CSE331 Autumn 2011
Software Design and Implementation

Worksheet A (?%): Due Monday December 5, 2011 at 11:29AM

This is the first worksheet assignment of two. It covers formal reasoning about programs. It is due at lecture this coming Monday -- we will use that time to exchange assignments and grade them together (under my direction). The intent of this is to get feedback to you quickly, and to also goto see the reasoning for the solutions.

• You are allowed to use late days, and you are allowed to miss lecture. However, everybody who attends Monday's lecture and contributes to the grading will get 5% extra-credit on the worksheet. (Note: extra-credit will be considered during assignment of final grades only after all the base grades are assigned. That is, you can not get a lower grade in the course because you did not do any extra credit, but you may get a higher grade.)
• We will collect the graded assignments after lecture to record the grades (and the extra-credit); we will have them at the CSE main desk by 3:30PM that afternoon. If you have concerns about how your assignment was graded, bring that to my attention as soon as possible.
• The solutions can be formatted or hand-written; regardless, they should be legible for the graders.
• Although we clearly will discuss the solutions in Monday's lecture, I will not be handing out a solution key at least until all students not in lecture turn in their assignments.

---

(2 points each, 20 points total) For each of the following Hoare triples, determine if it is true or false. Unless otherwise indicated, assume all variables are integers.

1. y ≤ 3 {x = y + 1} 2*x + y ≤ 11
2. n is even ∧n ≤ 100{n = n + 2}n is even ∧n ≤ 101
3. true {x = 5; y = 0}x= 5
4. x = 2 ∧ x = 3 {x = 5}x = 0
5. true {System.out.println("Hello world")}false
6. false {System.out.println("Hello world")} true
7. x = 0 {while x == 0 do x = x+1}x = 1
8. x = 1 {while x != 0 do x = x+1}x = 100
9. 2x = 3y {x = 2x} x = 3y
10. x > 2 {if x>2 then y=1 else y=-1} y > 0

---

(15 points) Prove the correctness of the following program (the precondition and the postcondition are shown in bold at the top and the bottom, respectively). All variables are integers, and the program is computing the quotient (q) and the remainder (r) of x/y. Your primary focus will be on the loop: you will need to prove all three parts of the Hoare axiom for loops, which also requires that you explicitly find a proper loop invariant.

true

q = 0;
while (y <= r) {
   r = r − y;
   q = 1 + q;
}

x = r + y × q ∧ y > r

---

(15 points) Consider the follow pair of very similar programs; prove them both correct (as in the previous question) and ensure that the proofs are about as similar to each other as the programs.

n > 0                                                                                             n > 0                                       
k = 0;                                                   k = 0;
j = 1;                                                   j = 1;
while (k != n) {                                         while (k != n) {
    k = k + 1;                                              k = k + 1;
    j = 2*j;                                                j = 2 + j;
}                                                        }
j = 2^n                                                   j = 2n+1

---