Self Test: Sorting
This module is a test of proving a do-od loop that sorts an array,
\(X\), in place.
Specification
Let \(X^{init}\) be the initial value of \(X\) and \(X^{fini}\) be
its value when the loop terminates. The specification of the loop
is that execution of the loop terminates, and
-
\(X^{fini}\) is a permutation of \(X^{init}\), and
-
\(X^{fini}\) is in ascending order.
Iterations
Let \(X\) be an array of \(N\) numbers.
Prove that the following loop satisfies the specification.
for all i where 0 < i < N:
X[i-1] > X[i] -> X[i-1], X[i] = X[i], X[i-1]
The loop flips any adjacent pair that is out of order.
Self Test: Proof of Correctness
Test 1
Give and prove an invariant of the loop, i.e, show that (1) the
invariant holds initially and (2) if it holds before a command is
executed then it holds after the command has executed.
Test 2
Prove that the loop terminates by giving a variant function for
the loop. Show that (1) the function is bounded below, and (2)
the function value can decrease only a finite number of times
before the bound is reached, and (3) the execution of every guarded
command with a true guard reduces the function.
Test 3
Prove that the specification holds upon termination of the
loop, i.e. show that if the invariant holds and all the guards are
false then the specification holds.
Answers
Answer 1
The following is an invariant:
\(X\) is a permutation of \(X^{init}\).
The predicate holds initially and every state transition maintains
it.
Answer 2
Define a variant function \(f(x)\) as the number of out-of-order
pairs in \(x\):
\(
f(x) = |\{(i, j) | (i < j) \wedge (x[i] > x[j]\} |
\)
The function has the following properties
-
It is bounded below.
-
It can decrease only a finite number of times before the bound
is reached because the function value is integer.
-
The execution of any guarded command with a true guard decreases
the function.
Answer 3
Since the invariant holds
\(X^{fini}\) is a permutation of \(X^{init}\).
Since all the guards evaluate to False at termination
\(X^{fini}\) is in ascending order.
Therefore, if the invariant holds and all the guards evaluate
to False then specification holds.
K. Mani Chandy,
Emeritus Simon Ramo Professor,
California Institute of Technology