1. Calculate (and simplify as much as possible).
(a) wp.(b[j] := k).(b[j] ≠ b[k])
(b) wp.(b[b[k]] := b[j]).(b[j] = b[k])
2. Derive a solution (and provide an accompanying narrative) to the following problem:
|[ con B : array of int; { #B>0 }
var r : int;
r := ?
{Q: r = (#k | 1≤k<#B : B[k] ≥ M.k)}
]|
|
where M.k = (MAX i | 0≤i<k : B[i]) is the maximum value in the array segment B[0..k). In words, the program computes the number of elements in the array —not including the one at location zero— that are greater than or equal to all those that precede it.
It should not need to be said that your solution/narrative is expected to explicitly identify the loop invariant (and how you chose it) and bound function. All but item (ii) on the loop checklist should obviously be true, and your derivation of the loop body and guard should serve as a proof of item (ii).
You should expect to have to strengthen the loop invariant by introducing a fresh variable and including a new conjunct that relates that variable's value to M.
3. Complete the development of the program below and show a proof of (ii) from the loop checklist. (The four other items on the list are clearly true.) Of course, E refers to an unknown expression. You will need to augment the loop invariant with a third conjunct in a way similar to what was done in solving the Prefix Sums problem. Don't forget that B is a rigid variable and therefore cannot be mentioned in any command. You can assume that min is an infix binary operator in our programming language (and can be applied as it appears within Q and Q')
|[ con N : int; {N≥0}
var b : array[0..N] of int; {b = B}
var k : int;
k := 0;
{loop invariant I: (∀i | 0≤i<k : b[i] = B[i] min B[i+1]) ∧ 0≤k≤N }
{bound function t: N - k}
do k ≠ N ⟶ k,b := k+1,b(k:E)
od
{Q': (∀i | 0≤i<k : b[i] = B[i] min B[i+1]) ∧ k=N ∧ b[N] = B[N]}
{Q: (∀i | 0≤i<N : b[i] = B[i] min B[i+1]) ∧ b[N] = B[N] }
]|
|
4. Complete the development of the program below and show a proof of (ii) from the loop checklist. (The four other items on the list are clearly true, with the exception of item (i) with respect to any fresh variables that you might introduce.) Of course, E refers to an unknown expression. You will need not only to augment the loop invariant as in the previous problem but also to strengthen it by introducing a fresh variable. You should find that using a multiple assignment command is very convenient. Don't forget that B is a rigid variable and therefore cannot be mentioned in any command.
|[ con N : int; {N>0}
var b : array[0..N) of int; {b = B}
var k : int;
k := 1;
{loop invariant I: (∀i | 1≤i<k : b[i] = B[i] - B[i-1]) ∧ 1≤k≤N }
{bound function t: N - k}
do k ≠ N ⟶ k,b := k+1,b(k:E)
od
{Q': (∀i | 1≤i<k : b[i] = B[i] - B[i-1]) ∧ k=N ∧ b[0] = B[0] }
{Q: (∀i | 1≤i<N : b[i] = B[i] - B[i-1]) ∧ b[0] = B[0] }
]|
|
5. Prove the correctness of the following program, which sorts an array. (Do you recognize which sorting algorithm it is based upon?) Because it is obvious that items (iii), (iv), and (v) on the loop checklist are satisfied, all you need to show are items (i) and (ii). (Regarding (ii), all you need to consider is the line of code that swaps two array elements, as is explained below.)
|[ con N : int { N>0 }
;var b : array[0..N) of T { b=B }
;var k, m : int
;m := N
{loop invariant I: inOrder.m.N ∧ boundary.m ∧ 0≤m≤N ∧ perm.b.B)}
{bound function t: m}
;do m ≠ 0 ⟶
{I ∧ m≠0}
k := locOfMax(b,0,m);
{I ∧ 0≠m ∧ 0≤k<m ∧ b[k] = (MAX i | 0≤i<m : b[i]) }
;swap(b,k,m-1);
{I(m:=m-1)}
;m := m-1
{I}
od
{Q: inOrder.0.N ∧ perm.b.B}
]|
whereinOrder.p.q : (∀i,j | p≤i≤j<q : b[i] ≤ b[j]) boundary.p : (∀i,j | 0≤i<p ∧ p≤j<N : b[i] ≤ b[j]) perm.f.g : arrays f and g are permutations of one another |
Notes/Hints:
The command swap(a,i,j) is, in effect, the assignment a := a(i,j : a.j,a.i) and therefore (in accord with the wp assignment law) has the following semantics:
where (provided that i=j implies E=F)
| a(i,j : E,F).r = | { | E | if i=r |
| F | if j=r | ||
| a.r | otherwise |
Using the if function, this can be written as follows:
Thus, if b'[i] occurs within a quantification in which i is a dummy that varies over a range that includes neither k nor m-1, you can cite the Irrelevant Array Element Axiom to justify replacing that occurrence of b'[i] by b[i].