CSci 550: Program Semantics and Derivation
Spring Semester 1998

Assignment #5
Due 9:30 A.M., Thursday, 19 March

1. Prove that the following program is correct. Identify the proof obligations and show that they hold.

   |[  var c, n : int ;  var b[0..N) : int  
       { 0 < n <= N & c = (# i : n <= i < N : b.i < 0) }; 
           if b.(n-1) <  0 --> c,n := c+1, n-1 
           [] b.(n-1) >= 0 --> n := n-1 
           fi 
       { c = (# i : n <= i < N : b.i < 0) }
   ]|
   

2. Now prove that the following program is correct. Find a loop invariant and bound function for the loop. Identify the proof obligations and show that they hold.

   |[  var c,n : int ;  var b[0..N) : int { N >= 0 } ; 
           c, n := 0, N; 
           do n != 0 --> 
               if b.(n-1) <  0 --> c,n := c+1, n-1 
               [] b.(n-1) >= 0 --> n := n-1 
               fi 
           od
       { c = (# i : 0 <= i < N : b.i < 0 )  }
   ]|
   

3. How would the invariant and bound function differ for this program? It is not necessary to prove this program, just identify a suitable invariant and bound function.

   |[  var c,n : int ;  var b[0..N) : int { N >= 0 } ; 
           c, n := 0, 0; 
           do n != N --> 
               if b.n <  0 --> c,n := c+1, n+1 
               [] b.n >= 0 --> n := n+1 
               fi 
           od 
       { c = (# i : 0 <= i < N : b.i < 0 )  }
   ]|
   

4. Prove that the following program is correct. Find a loop invariant and bound function for the loop. Identify the proof obligations and show that they hold.

   |[  con N : int { N >= 1 } ; var n : int ;   
           n := 1 ; 
           do 2 * n <= N --> 
               n := 2 * n  *
           od  
       { 1 <= n <= N < 2 * n & (EXISTS p : p >= 0 :  n = 2^p)  }
   ]| 
   

UP to CSCI 550 Assignments document?