CSci 550: Program Semantics and Derivation
Fall Semester 1996
Assignments

1. Assignment #1

2. Assignment #2

3. Assignment #3

4. Assignment #4

5. Assignment #5

6. Assignment #6

7. Assignment #7

8. Assignment #8

UP to CSCI 550 root document?

Assignment #1: Due Tuesday, 10 September, 9:30 a.m.

Note: I changed the due date on this homework from Thursday, 5 September, to Tuesday, 10 September.

Prove the following theorems from A Programmer's Introduction to Predicate Logic. In a proof of a theorem you may use any axiom or theorem appearing above the theorem (i.e., smaller number) in the list and any of the applicable proof techniques we discussed in class.

• Theorems 13, 21, and 22 about conjunction.
• Theorems 26, 29, and 34 about implication.
• Theorem 46, 55, and 57 about negation.

You may want to do several other theorems for your own study.

UP to CSCI 550 root document?

Assignment #2: Due Tuesday, 17 September, 9:30 a.m.

Do the following exercises.

• Exercise 2.3 (a) (c) from the Cohen textbook.
• Exercise 2.4 (b) (f) from the Cohen textbook.
• Theorems 78 and 94 from the Logic handout.
• Exercise 3.10, 3.11, 3.12 from the Cohen textbook.

UP to CSCI 550 root document?

Assignment #3: Due Thursday, 26 September, 9:30 a.m.

1. Formalize the following sentences. Suppose an array X[0..N) is given, where N >= 1.
   1. Array X is increasing.
   2. All values in X are distinct.
   3. All values in X are equal.
   4. If X contains a 1, then X contains a 0 as well.
   5. No two neighbors in X are equal.
   6. The maximum of X occurs only once in X.
   7. r is the length of a longest constant section of X.
   8. All elements of X are prime numbers.
   9. The number of odd-valued elements in X equals the number of even-valued elements.
   10. r is the product of the positive elements of X.
   11. r is the maximum of the sums of the sections of X.
   12. X contains a square.

2. Do exercise 4.2 (b) (d) (f) in the Cohen textbook

3. Do exercise 4.5 (b) (d) (e) in the Cohen textbook

UP to CSCI 550 root document?

Assignment #4: Due Thursday, 17 October, 9:30 a.m.

The notation in this online version of the assignment differs from the printed handout. Below OR, AND, and EQUIV represent logical disjunction, conjunction, and equivalence, respectively; ** denotes exponentiation; !=, <=, and >= denote not-equal, less-or-equal, and greater-or-equal, respectively; [] denotes the guard separator box.

1. Let div denote integer division and mod denote the modulo operation. For any integers a, b, q, and r such that b != 0:

       a div b = q OR a mod b = r EQUIV  a = q * b + r OR 0 <= r < |b|.
   

   Determine the weakest predicate Q for each of the following expressions:
   1. |[ var x : int { Q } ;
x := x + 1 { x > 0 } ]|
   2. |[ var x : int { Q } ;
x := x * x { x > 0 } ]|
   3. |[ var x : int { Q } ;
x := x * x * x - 2 * x + 4 { x > 0 } ]|
   4. |[ var x : int { Q } ;
x := x + 1 { x**3 - 5 * x**2 + 2 * x > 0 } ]|
   5. |[ var x : int { Q } ;
x := x * x * x - 2 * x + 4 { x**3 - 5 * x**2 + 2 * x > 0 } ]|
   6. |[ var x : int { Q } ;
x := x + 1 { x = x + 1 } ]|
   7. |[ var x : int { Q } ;
x := E { x = E } ]|
   8. |[ var x : int { Q } ;
x := x mod 2 { x = x mod 2 } ]|
   9. |[ var x,y : int { Q } ;
x,y := x+1, y-1 { x + y > 0 } ]|
   10. |[ var x,y : int { Q } ;
x,y := y+1, x-1 { x > 0 } ]|
   11. |[ var x,y : int { Q } ;
x,y := y * x, x*y { x + y > 0 } ]|
   12. |[ var x, y : bool { Q } ;
x := x EQUIV y { x } ]|
   13. |[ var x : int { Q } ;
x := x * x; x := x+1 { x > 0 } ]|
   14. |[ var x, y : int { Q } ;
x := y ; y := x { x = A AND y = B } ]|
   15. |[ var i : int ; var b[0..12) : array of int
{ 0 <= i < 12 OR Q } ; b.i, b.(i+1) := 3, 4 { b.i = 3 } ]|
2. Prove that the following holds:

   |[  var x, y : int 
       { true } ;  
       if  x >= y  --> skip
       []  y >= x  --> x,y := y,x  
       fi
       { x >= y }  
   ]|
   

UP to CSCI 550 root document?

Assignment #5: Due Tuesday, 29 October, 9:30 a.m.

1. Do exercise 5.1 (a) and (b) in the Cohen textbook (p. 89).
2. Do exercise 5.7 in the Cohen textbook (p. 96).
3. Prove that the following program is correct. Find appropriate loop invariants and bound functions for each loop. Identify the proof obligations and show that they hold.

   |[  con N : int { N >= 0 } ;  var f[0..N) : array of int ; 
       var b : bool ;  var n : int ; 
       b, n := false, 0 ; 
       do n != N --> 
           b := b OR (f.n = 0) ; 
           n := n + 1 
       od 
       { b = (EXISTS i : 0 <= i < N : f.i = 0) }
   ]|
   

4. Prove that the following program is correct. Find appropriate loop invariants and bound functions for each loop. Identify the proof obligations and show that they hold.

   |[  con N : int { N >= 0 } ;  var f[0..N) : array of int ; 
       var b : bool ;  var n : int ; 
       b, n := false, 0 ; 
       do n != N & NOT b  --> 
           b := b OR (f.n = 0) ; 
           n := n + 1 
       od 
       { b = (EXISTS i : 0 <= i < N : f.i = 0) }  
   ]|
   

5. What is an appropriate bound function for the following loop?

   |[  var x, y, z : int { true } ; 
       do  x < y  -->  x, y := y, x 
       []  y < z  -->  y, z := z, y 
       od 
       { x >= y & y >= z }    
   ]| 
   

UP to CSCI 550 root document?

Assignment #6: Due Thursday, 7 November, 9:30 a.m.

Note that I have postponed the due date from that printed on the handout sheet.

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

   |[  con N : int { N >= 1 }; f[0..N): array of int;
       var x, y : int;
           x, y := 0, N - 1;
           do x != y -->
   	    if f.x <= f.y --> x := x + 1
               [] f.y <= f.x --> y := y - 1
   	    fi
           od
       { f.x = (MAX i : 0 <= i < N : f.i) }
   |]
   

   Hint: What is always found in the subarray f[x..y]?

UP to CSCI 550 root document?

Assignment #7: Due Tuesday, 19 November, 9:30 a.m.

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 = (SUM i : 0 <= i < N : (-1)**i * b.i ) } 
       ]|
   

UP to CSCI 550 root document?

Assignment #8: Due Tuesday, 26 November, 9:30 a.m.

1. Derive a program fragment S satisfying the following specification. Show the derivation and the proof obligations.

       |[ con N : int { N >= 1 } ; 
          var b[0..N) : array of int ; 
          var r : int ;  
              S 
          { r : r = (# i,j : 0 <= i < j < N : b.i*b.j >= 0 ) } 
        ]|
   

   Hint: Consider the cases for x andy y in which x*y >= 0.

UP to CSCI 550 root document?