-------------------------------------------------- Part 1 -------------------------------------------------- I will only provide the answer; you should figure out yourself how to come to that answer. 1. (a) 2. (c) 3. (a) 4. (b) 5. (d) 6. (c) ; though (a) is also good. Both use "x" as the termination metric; but both do not indeed say that we have a lower bound. However, the loop's guard quite trivially implies that 0 is the lower bound. -------------------------------------------------- Part 1 -------------------------------------------------- 1. (a) {* N>=0 *} hasEqPair(READ a:[int], N:int) : bool {* return = (exists i,j: 0<=i,jj : a[i]=a[j]) *} (b) {* N>=0 /\ (forall i,j : 0<=i,j (i=j))*} mkPerm(READ a:[int], N:int) : [int] {* subset N return a /\ subset N a return *} where "subset" is defined as follows: subset N a b = (forall i : 0<=i=0 [A2:] Max>=0 [A3:] (forall k : 0=k=0) [G:] wp init I ------------------------------------------------------------- 1. { wp calculation } wp init I = (0 = SUM(a[0..0)) /\ 0<=0<=N /\ true = (0<=Max) 1. { see the subproof below } 0 = SUM(a[0..0) PROOF SUM(a[0..0)) = { empty enumeration } SUM [] = {def. SUM} 0 2. { follows from A1 } 0<=0<=N 3. { follows from A2 } true = (0<=Max) 4. { conjunction of 1,2,3 and using the equality in 1 } wp init I DONE ------------------------------------------------------------- PROOF PEC [A1:] s = SUM(a[0..i)) [A2:] 0<=i<=N [A3:] ok = (s<=Max) [A4:] i>=N [G:] wp (return := ok) (return = (SUM(a[0..N)) <= Max)) ------------------------------------------------------------- 1. { calculate wp } G = (ok = (SUM(a[0..N)) <= Max)) 1. { from A2 and A4 } i=N 2. { see subproof below } ok = (SUM(a[0..N)) <= Max PROOF SUM(a[0..N)) <= Max = { using 1 } SUM(a[0..i)) <= Max = { using A1 } s <= Max = { using A3 } ok DONE ------------------------------------------------------------- PROOF PIC [A1:] s = SUM(a[0..i)) [A2:] 0<=i<=N [A3:] ok = (s<=Max) [A4:] i0 *} {* (1) ? *} @x := k-1 ; {* (2) ? *} @y := k ; {* (3) ? *} r := P(@x,@y) ; {* (4) ? *} k := @y ; {* r+k>0 *} (4) --> r+@y>0 (3) --> @x>=0 /\ @y>0 /\ (r'+y' > @y+@x ==> r'+y'>0) // y' is a fresh variable (2) --> @x>=0 /\ k>0 /\ (r'+y' > k+@x ==> r'+y'>0) (1) --> k-1>=0 /\ k>0 /\ (r'+y' > k+k-1 ==> r'+y'>0) -- (b) Yes the specification is valid; the given pre-condition implies the calculated weakest pre-condition (1) above. (1) k>1 obviously implies k-1>=0 (2) since k-1>=0 and k>0, then k+k-1 must be >0. So r'+y' is also >0.