Merge function proof of correctness
Let $A'[p \ldots r]$ be a copy of the array $A[p\ldots r]$ right after entering the Merge function.
Precondition
$0 \leq p \leq q \lt r$
$\forall p\leq x\leq r: A'[x] \neq \infty$
$A'[p\ldots q]$ and $A'[q+1\ldots r]$ are sorted in ascending order.
Postcondition
Permutations can be formalized by using the concept of bijection. We say that $A[p \ldots r]$ is a permutation of $A'[p \ldots r]$ (or vice versa) if and only if:
There exists a bijection $F : \{p \ldots r\} \rightarrow \{p \ldots r\}$ such that $\forall p \le x \le r : A[x] = A'[F(x)]$
Furthermore, if we want to verify that $A[p \ldots r]$ is sorted in ascending order, we just need to add another constraint:
$\forall p\leq x \lt r : A[x] \leq A[x + 1]$
These two expressions will be the Postcondition of the Merge function.
Loop invariant
We can craft an invariant by weakening the postcondition:
$\varphi:$ There exists a bijection $F : \{p\ldots k-1\} \rightarrow \{p \ldots p+i-2\} \cup \{q+1\ldots q+j-1\}$ such that
$\forall p \leq x \leq k-1 : A[x] = A'[F(x)]$. Furthermore $\forall p\leq x \lt k-1 : A[x] \leq A[x + 1]$.
We still need to add some properties to the invariant. These are required for proving the termination step:
- $i \leq q-p+2$
- $j \leq r-q+1$
- $k = p+j+i-2$
- $p \leq k \leq r + 1$
and these are required for proving the maintenance step:
- $\forall 1 \leq x \leq q-p+1 : L[x] = A'[p+x-1]$
- $\forall 1 \leq x \leq r-q : R[x] = A'[q+x]$
- $\Psi: \forall p \leq x \leq k-1 : A[x] \leq min(L[i],R[j])$
- $L[q-p+2] = R[r-q+1] = \infty$
- $A'[p\ldots q]$ and $A'[q+1\ldots r]$ are already sorted. This is part of Merge's precondition.
Now, let us calculate the continuation condition $B$ and exit condition $\neg B$ of the loop (line 12). We know from the pseudocode that $B$ is $k \leq r$. We can see this more clearly if we translate the for k = p to r
loop into a normal for loop: for(k = p; k <= r; k++){ ... }
. As we can see, the loop will continue provided that $k \leq r$. Therefore, the exit condition will be $\neg B$, that is $k \gt r$. However, since the invariant asserts that $k \leq r + 1$, we can simply consider that the exit condition is $k = r + 1$.
Initialization step
$Pre \wedge (k = p) \wedge (i = 1) \wedge (j = 1) \implies Inv$
$k = p$ leads to the empty domain $\{p\ldots p-1\}$. Universal quantification over an empty domain is trivially true. The rest of the properties of the invariant are easy to prove by just substituting the values of the variables in the first iteration ($k = p$, $i = 1$, $j = 1$).
Maintenance step
The general rule for proving maintenance is: $\{Inv \wedge B\}$ $S$ $\{Inv\}$, being $S$ the set of instructions in the loop body.
The maintenance of the following invariant properties need not be proved:
$\forall 1 \leq x \leq q-p+1 : L[x] = A'[p+x-1]$
$\forall 1 \leq x \leq r-q : R[x] = A'[q+x]$
$L[q-p+2] = R[r-q+1] = \infty$
$A'[p\ldots q]$ and $A_1[q+1\ldots r]$ are already sorted.
since $A'$, $L$, $R$, $p$, $q$ and $r$ are not modified during the execution of the loop.
For the rest of the properties, we are going to prove their maintenance by considering the two possible cases that can occur (either $L[i] \leq R[j]$ or $L[i] \gt R[j]$):
(a) $Inv \wedge B \wedge (L[i] \leq R[j]) \wedge (A[k] = L[i]) \implies ((Inv)_{i+1}^{i})_{k+1}^{k}$
- Maintenance of $p \leq k \leq r + 1$
$p \leq k \leq r + 1 \wedge B \implies (p \leq k \leq r + 1)^{k}_{k+1}$
$p \leq k \leq r + 1 \wedge k\leq r \implies p \leq k+1 \leq r + 1$
$p \leq k \leq r \implies p \leq k+1 \leq r + 1$
- Maintenance of $k = p+j+i-2$
At the end of the iteration, both $k$ and $i$ will have incremented by one with respect to their previous value, and $j$ will remain unchanged. Hence, the equality $k = p+j+i-2$ will be preserved.
- Maintenance of $i \leq q-p+2$ and $j \leq r-q+1$.
The variable $j$ remains unchanged so $j \leq r-q+1$ is maintained.
The variable $i$ cannot grow larger than $q-p+2$ because if $i = q-p+2$, then $L[i] = \infty$, and the condition $L[i] \leq R[j]$ (line 13) will fail provided that $R[j] \neq \infty$, or equivalently, $j \neq r-q+1$. Now, suppose $i = q-p+2$ and $j = r-q+1$ occur at the same time:
$Inv \wedge \color{red}{B} \wedge (i = q-p+2) \wedge (j = r-q+1)\implies$
$(k = p+j+i-2) \wedge (i = q-p+2) \wedge (j = r-q+1) \implies k = r + 1 \implies \color{red}{\lnot B}$
This is a contradiction, therefore, $i = q-p+2$ and $j = r-q+1$ cannot occur at the same time provided $Inv \wedge B$.
- Maintenance of $\varphi$
$Inv \wedge B \wedge (L[i] \leq R[j]) \wedge (A[k] = L[i]) \implies ((\varphi)^{i}_{i+1})^{k}_{k+1}$
We want to prove that $((\varphi)^{i}_{i+1})^{k}_{k+1}$, that is:
There exists a bijection $F : \{p\ldots k\} \rightarrow \{p \ldots p+i-1\} \cup \{q+1\ldots q+j-1\}$ such that
$\forall p \leq x \leq k : A[x] = A'[F(x)]$. Furthermore $\forall p\leq x \lt k : A[x] \leq A[x + 1]$.
We will do this in two steps. First we are going to prove $\forall p\leq x \lt k : A[x] \leq A[x + 1]$.
We know from $\Psi$ that $\forall p \leq x \leq k-1 : A[x] \leq min(L[i],R[j])$.
Since $L[i] \leq R[j]$, then $\forall p \leq x \leq k-1 : A[x] \leq L[i]$. Since $A[k] = L[i]$, then $\forall p \leq x \leq k-1 : A[x] \leq A[k]$.
We know from $\varphi$ that $\forall p\leq x \lt k-1 : A[x] \leq A[x + 1]$. We can conclude that:
$$(\forall p\leq x \lt k-1 : A[x] \leq A[x + 1]) \wedge (\forall p \leq x \leq k-1 : A[x] \leq A[k]) \implies$$ $$\forall p\leq x \lt k : A[x] \leq A[x + 1]$$
Let's continue with the second part.
Let there be a bijection $F : \{p\ldots k-1\} \rightarrow \{p \ldots p+i-2\} \cup \{q+1\ldots q+j-1\}$ such that
$\forall p \leq x \leq k-1 : A[x] = A'[F(x)]$.
Since $A[k] = L[i] = A'[p+i-1]$, we can construct another bijection $F' : \{p\ldots k\} \rightarrow \{p \ldots p+i-1\} \cup \{q+1\ldots q+j-1\}$ such that
$\forall p \leq x \leq k : A[x] = A'[F'(x)]$.
- Maintenance of $\Psi$
$Inv \wedge B \wedge (L[i] \leq R[j]) \wedge (A[k] = L[i]) \implies ((\Psi)^{i}_{i+1})^{k}_{k+1}$
$\Psi: \forall p \leq x \leq k-1 : A[x] \leq min(L[i],R[j])$
Since $A[k] = L[i]$ and $L[i] \leq R[j]$, then $A[k] \leq min(L[i],R[j])$
Since $L[i] \leq L[i+1]$, then $min(L[i],R[j]) \leq min(L[i+1],R[j])$
Therefore, $\forall p \leq x \leq k : A[x] \leq min(L[i+1],R[j])$
(b) $Inv \wedge B \wedge (L[i] \gt R[j]) \wedge (A[k] = R[j]) \implies ((Inv)_{j+1}^{j})_{k+1}^{k}$
The proof of (b) is analogous to (a).
Termination step
First, we can derive that $Inv \wedge (k = r + 1)$ implies $(i = q-p+2)\wedge(j=r-q+1)$.
Proof:
$(k = r+1) \wedge (k = p+j+i-2) \implies r+1=p+j+i-2$
The system of equations
$$r+1=p+j+i-2$$
$$i \leq q-p+2$$
$$j \leq r-q+1$$
has only one solution for $(i,j)$: $i = q-p+2$ and $j = r-q+1$. If there was another solution for $(i,j)$, then $p+j+i-2 \lt r+1$, which contradicts $r+1=p+j+i-2$.
The above makes proving $Inv \wedge \lnot B \implies Post$ much easier:
$Inv \wedge (k=r+1) \implies Inv \wedge (k=r+1) \wedge (i=q-p+2) \wedge (j=r-q+1) \implies Post$
Merge's proof of terminality
By the invariant we know that $k \leq r + 1$. Also, we know that the exit condition of the loop is $k = r + 1$. Since the $k$ variable is always incremented by one on each iteration, we can be sure that $k$ will eventually reach $r + 1$, causing the loop to exit. This can be reflected via the following bound function:
$\tau(k) = r + 1 - k$
We can verify that $\tau(k)$ holds the following properties:
- $Inv \wedge B \implies \tau(k) \gt 0$
Proof: $Inv \wedge B \implies B \implies k \leq r \implies r - k \geq 0 \implies r + 1 - k \gt 0$
- $\tau(k) = V \implies \tau(k + 1) \lt V$
Proof: $\tau(k + 1) = r - k = \tau(k) - 1 = V - 1 \lt V$
The first property ensures that when $\tau(k)$ reaches a value less than or equal to $0$, the loop will exit.
The second property ensures that $\tau(k)$ decreases strictly upon each iteration.
Therefore, the loop will always halt.
Definition is_a_sorting_algorithm
in softwarefoundations.cis.upenn.edu/vfa-current/Sort.html) $\endgroup$