0
$\begingroup$

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

MergeSort code

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?

$\endgroup$
5
  • 2
    $\begingroup$ I would state it like this: let $i$ and $j$ be the current indices (you can do induction on $i+j$). Then the statement could be along the lines "1) $A[...]$ is a permutation of $L_1, \ldots, L_{i-1}, R_1, \ldots, R_{j-1}$, 2) $A[...]$ is sorted, 3) All elements in $A[...]$ are at most $\min(L_i, R_j)$". You also know that $L_i$ is the smallest element in $L_i, L_{i+1}, \ldots$ (same for $R_j$). It should be enough for the induction. The above statements can be stated formally by their definitions (e.g. for 1), just use the definition of permutation) $\endgroup$
    – Dmitry
    Oct 30, 2022 at 22:40
  • $\begingroup$ @Dmitry why don't you answer the question instead of commenting? Are you afraid of upvotes? $\endgroup$
    – Nathaniel
    Oct 30, 2022 at 22:49
  • $\begingroup$ @Dmitry Thanks for your reply. I guess most of the theorem provers have built-in libraries including the definition of permutation, tuple, set etc., so I think I won't need to define myself all those concepts, right? If that is not the case, would it be difficult to do manually from scratch? $\endgroup$
    – mateleco
    Oct 31, 2022 at 1:38
  • 1
    $\begingroup$ @mateleco, Tuples and sets are probably defined, but I don't know about permutations. You can check how Coq does it, and it looks like a pain to work with: coq.inria.fr/library/Coq.Sorting.Permutation.html (but it might work out OK for merge sort). But it looks like they use exactly them (check Definition is_a_sorting_algorithm in softwarefoundations.cis.upenn.edu/vfa-current/Sort.html) $\endgroup$
    – Dmitry
    Oct 31, 2022 at 2:29
  • 1
    $\begingroup$ You could use Hoare logic to formalise a correctness proof of Merge (and MergeSort). Doing so would reveal that the suggested invariant is still too weak: it needs to state a.o. that $A[1..p-1]$ and $A[r+1..|A|]$ remain unchanged. You'd also make regular use of a sortedness predicate about subarrays. And that usually refers to permutations as @Dmitry indicated. $\endgroup$
    – Kai
    Nov 2, 2022 at 9:08

1 Answer 1

0
$\begingroup$

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$

  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.

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

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

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.