SE 504   Spring 2025
HW #3: Loops, Selection, and Sequential Composition
Due: 4:00pm, Friday, March 7

In each of the problems, you are given a Hoare triple of the form {P} Sinit; do B ---> S od {Q} (possibly with some missing pieces) in which Sinit is an assignment command (used for initialization), B is a loop guard, and S is a loop body. The Hoare triple is annotated with a loop invariant I and bound function t.

Prove it by showing each of the five items on the loop checklist:

  1. {P} Sinit {I}, which guarantees that the initialization truthifies the loop invariant (just before the loop's first iteration).
  2. {I ∧ B} S {I} which guarantees that each iteration of the loop preserves the truth of the loop invariant.
  3. I ∧ ¬B  ⟹  Q, which guarantees that, if the loop terminates, the postcondition will hold at that time.
  4. I ∧ B  ⟹  t > 0 which guarantees that, as long as more iterations are to occur, the bound function has not yet descended to its threshold of zero.
  5. {I ∧ B ∧ t=C} S {t < C} which guarantees that each iteration of the loop causes the value of the bound function to decrease.

Items 1 and 2 together show that I is, as claimed, an invariant of the loop. Item 3 shows that, if and when the loop terminates, the postcondition Q holds. Items 4 and 5 together show that the loop terminates after finitely many iterations.

Note that any precondition regarding only constants (e.g., N≥0) can be considered as an implicit part of the loop invariant.

1. Consider the recursive function f, defined as follows:

f(k) = { 1   if k = 0
2   if k = 1
5·f.(k−1) − 6·f.(k−2)   otherwise (i.e., k ≥ 2)

The program below computes f.N, placing the result in the variable current. Prove the program's correctness. 


|[ con N : int;   // N is the input value
   var i,current,next : int;
   {P: N ≥ 0}
   i, current, next := 0, 1, 2;
   {loop invariant I: 0≤i≤N  ∧  current = f.i  ∧  next = f.(i+1)}
   {bound function t: N-i}
   do i ≠ N  --->  
      current, next := next, 5*next - 6*current;
      i := i+1;
   od
   {Q: current = f.N}
]|

2. Prove the correctness of this program, which calculates (+k | 0≤k≤Y : k) in a very roundabout way. 

|[ con Y : int;       // input variable
   var x,y,z : int;   // z is the output variable      
   {P: Y ≥ 0}
   x,y,z := Y,Y,0;
   {loop invariant I: z+x = (+k | y≤k≤Y : k) ∧ 0≤x≤y ∧ z≥0 }
   {bound function t: Y2 + y - z}
   do x ≠ 0 ∨ y ≠ 0 --->
      if x ≠ 0 then  
         x,z := x-1,z+1
      else  // x = 0 ∧ y ≠ 0
         y := y-1; x := y
      fi
   od
   {Q: z = (+k | 0≤k≤Y : k) }
]|

3. Apply the replace a constant by a variable heurisic to rewrite the postcondition Q in the program below. Specifically, replace 0 by the variable k and add the new conjunct k=0 to obtain a stronger postcondition Q'. (Repeating: Replace 0 by k; do not replace #B by k.)

Then take one of the conjuncts of Q' to be a loop invariant and the negation of the other conjunct to be the loop guard. (That is, apply the "delete a conjunct" heuristic.)

Complete the pre-loop assignment command so that k and biggest are initialized in such a way as to truthify the loop invariant. Then complete the assignment command forming the loop body so that its execution preserves the truth of the invariant. (You should derive the right-hand side of the assignment to biggest via calculation. Assume that max is an infix binary operator in our programming language, analogous to +, so that the expression x max y for example, evaluates to the larger of the values of x and y.)

You must also show that the loop body "makes progress towards termination", which is to say that its execution reduces the value of some bound function whose value cannot go below zero unless the loop guard has become false. (To do this you will need to include in the loop invariant a conjunct that imposes lower and upper bounds upon k.)

Show your completed program and a proof of its correctness. 


|[ con b : array of int;  {#b > 0}
   var biggest: int;
   var k : int;

   k,biggest:= ?,?;
   {loop invariant I: ?}
   {bound function t: ?}
   do ? --->
      k,biggest:= ?,?;
   od
   { Q:  biggest = (max j | 0≤j<#b : b[j]) }
]|

4. Prove the correctness of the following program, which finds a minimum element in the integer array b[]. Note that the 2nd conjunct of the loop invariant corresponds to the statement that either b[p] or b[q] is the minimum among the values occurring anywhere in b[0..p] or b[q..#b). 

|[ con b : array of int;
   var p,q : int;
   {P: #b > 0}
   p,q := 0, #b-1;
   {loop invariant I:
      0≤p≤q<#b  ∧
      b[p] min b[q] =  (MIN i | 0≤i≤p ∨ q≤i<#b : b[i]) }
   {bound t: q-p}
   do p ≠ q --->
      if b[p] > b[q] then 
         p := p+1;
      else  // b[p] ≤ b[q]
         q := q-1;
      fi
   od
   {Q: 0≤p<#b  ∧  b[p] = (MIN i | 0≤i<#b : b[i]) }
]|

In doing the proof, you may find useful this following definition of, and theorems pertaining to, the min operator:

  1. Definition of min: (x = x min y) ≡ (x ≤ y)
  2. Theorem Min.1: (x = x min y) ∨ (y = x min y)
  3. Theorem Min.2: x = x min x