MergeSort's merge function loop invariant

Question

I am reading a proof of correctness for the MergeSort Algorithm. This is the code for the MergeSort and the Merge function:

The correctness of the MergeSort function is easy to prove since the two MergeSort recursive calls decrease the size of the problem by half, which guarantees the convergence to the base case ($p = r$). Furthermore, assuming the first recursive call to MergeSort leaves the array A[p..q] sorted and the second recursive call leaves A[q+1..r] sorted, it is clear that merging the subarrays A[p..q] and A[q+1..r] will leave the array A[p..r] sorted. However, the key thing here is proving the correctness of the Merge function.

Cormen's book suggests the following invariant for the main loop in the Merge function (lines from 12 to 17):

1. The subarray $A[p\ldots(k−1)]$ consists of the $k−p$ smallest elements of $L[1\ldots(n_1 + 1)]$ and $R[1\ldots(n_2 + 1)]$, in sorted order.

2. The elements $L[i]$ and $R[j]$ are the smallest elements of their arrays that have not been copied back to $A$.

I understand this invariant and the full proof (Initialization, Maintenance, and Termination). However, the above invariant is mostly written in natural language, and I wonder if there is a more formal way to state it. This is because I need a more rigorous proof that need not rely on natural language. For example, to verify the program with a theorem prover I can't use natural language at all.

Update

@Dmitry suggested a different invariant that requires using the concept of permutation. However, Coq's axioms of permutation look really complicated. Is there a simpler way to formally prove the Merge function without resorting to Coq's axioms or other external libraries?

Answer 1

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}$

1. 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$

2. 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.

3. 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$.

4. 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)]$.

5. 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.