CSci 550: Program Semantics and Derivation
Spring Semester 1998

Assignment #7
Due 9:30 A.M., Tuesday, 14 April

1. Derive a program fragment S that does not contain the multiplication operator. Show the derivation and a proof of the correctness of your solution.

       |[ con X, Y : int { X >= 0 & Y >= 0 } ;
          var z : int ; 
               S 
          { z : z = X * Y } 
       ]|
   

2. Derive a program fragment S that does not contain an exponentiation. Show the derivation and the proof obligations.

       |[ con  N : int { N >= 0 } ; 
          var  b[0..N) : array of int ; 
              S 
          { z : z = (+ i : 0 <= i < N : (-1)**i * b.i ) }
       ]|
   

UP to CSCI 550 Assignments document?