Homework 7 Proof Rules and Proofs

CS 536: Science of Programming  Homework 7
Proof Rules and Proofs
CS 536: Science of Programming

A. Why?
• To prove validity of correctness triples, we use a proof system with axioms for atomic statements
and rules of inference for compound statements.
B. Outcomes
After this homework, you should be able to
• Verify and generate instances of the partial correctness proof rules.
C. Problems [60 points total]
Lectures 14 - 15: Proof Rules and Proofs, parts 1 & 2
For all the problems, if you define something using substitution notation (e.g., defining p′ using
“where p′ ≡ q′ [e/v]”), be sure to show the result of the substitution somewhere. Intermediate
calculations that you write out might be worth partial credit.
Note the names used in one problem have no connection to the same names in other
problems. (E.g., p₁ in Problem 1 is unrelated to p₁ in Problem 2.) Exception: Explicit connection can
be made but they refer only to the given names. (E.g., if Problem 2 said "Let p₁ be as in Problem 1",
then p₂ in Problems 1 and 2 are unrelated.)
You can use the looser sense of ≡ from lecture.
1. [12 = 4 * 3 points] Let p ≡ x = 2^k ∧ k ≤ n. Calculate p₁ and p₂, and the rule references R₁
and R₂.
1. { p₁ } k := k+1 { p ≡ x = 2^k ∧ k ≤ n } assignment (backward)
2. { p₂ } x := x*2 { p₁ } assignment (backward)
3. { p₂ } x := x*2; k := k+1 { p } sequence 2, 1
4. p ∧ k < n → p₂ predicate logic
5. {p ∧ k < n } x := x*2; k := k+1 { p } R₁

6. { inv p } while k < n do x := x*2; k := k+1 od {p ∧ k ≥ n} [2022-10-20] R₂
Hint: p₁ ≡ wp(k := k+1, p) ≡ …
CS Dept., Illinois Institute of Technology - 1 - © J. Sasaki 2022
CS 536: Science of Programming Sun 2022-11-06, 16:14 Homework 7: Classes 14 – 15
2. [15 = 5 * 3 points] Let p ≡ x = 2^k ∧ k ≤ n. Calculate p₁, p₂, and p₃ and the rule references R₁
and R₂.
1. { p₁ ≡ p ∧ k < n } x := x*2 { p₂ } assignment (forward)
2. { p₂ } k := k+1 { p₃ } assignment (forward)
3. { p₁ } x := x*2; k := k+1 { p₃ } sequence 2, 1
4. p₃ → p predicate logic
5. { p₁ } x := x*2; k := k+1 { p } R₁

6. { inv p } while k < n do x := x*2; k := k+1 od {p ∧ k ≥ n} [2022-10-20] R₂
Hints: p₁ ≡ p ∧ k < n ≡ ... ?. p₂ ≡ sp(p₁, x := x*2) ≡ … ?
3. [33 = 11 * 3 points] Let
• q ≡ r = X*Y - x*y
• IF ≡ if even(x) then y := 2*y; x := x/2 else r := r+y; x := x-1 fi
• even(x) ≡ x % 2 = 0, and odd(x) ≡ x % 2 ≠ 0
Calculate q₁ – q₆ and R₁ – R₅, so that the proof of correctness below is correct. (For R₁ – R₄, say
what kind of assignment is being used: assignment (backward) or assignment (forward).)
1. {q₁} x := x/2 {q} R₁ ≡ assignment (???)
2. {q₂} y := 2*y {q₁} R₂ ≡ assignment (???)
3. q₃ → q₂ predicate logic
4. {q₃} y := 2*y {q₁} precondition strengthening 3, 2
5. {q₃} y := 2*y; x := x/2 {q} sequence 4, 1
6. {q₄ ∧ r = r₀ ∧ x = x₀} r := r+y {q₅} R₃ ≡ assignment (???) *
7. {q₅} x := x-1 {q₆} R₄ ≡ assignment (???)
8. q₆ → q predicate logic
9. {q₅} x := x-1 {q} postcondition weakening 7, 8
10. {q₄} r := r+y; x := x-1 {q} sequence 6, 9
11. {q} IF {q} R₅
 We only use r₀ and x₀ in the false branch, and we drop them (in line 10) before forming the if-else (in line 11), *
so we don't have to add them to the true branch code or to the precondition of the if-else.
CS Dept., Illinois Institute of Technology - 2 - © J. Sasaki 2022
CS 536: Science of Programming Sun 2022-11-06, 16:14 Homework 7: Classes 14 – 15
Solution to Homework 7
1. p₁ ≡ p[k+1⧸k] ≡ x = 2^(k+1) ∧ k+1 ≤ n
p₂ ≡ p₁[x*2⧸x] ≡ x*2 = 2^(k+1) ∧ k+1 ≤ n [2022-11-02]
R₁ ≡ precondition strengthening 4, 3
R₂ ≡ while loop, 5 †
2. p₂ ≡ sp(p₁, x := x*2) ≡ (p ∧ k < n) [ x₀ ⧸ x ] ∧ x = x₀*2
≡ ((x = 2^k ∧ k ≤ n) ∧ k < n)[x₀ ⧸x] ∧ x = x₀*2 [fixes 2022-11-06]
≡ (x₀ = 2^k ∧ k ≤ n ∧ k < n ∧ x = x₀*2)
p₃ ≡ sp(p₂, k := k+1 ) ≡ p₂ [ k₀ ⧸ k ] ∧ k = k₀+1
≡ (x₀ = 2^k ∧ k ≤ n ∧ k < n ∧ x = x₀*2) [ k₀ ⧸ k ] ∧ k = k₀+1
≡ (x₀ = 2^k₀ ∧ k₀ ≤ n ∧ k₀ < n ∧ x = x₀*2 ∧ k = k₀+1 )
R₁ ≡ postcondition weakening 3, 4
R₂ ≡ while loop, 5
[2022-11-06] Quick sanity check: p₃ → p?
p₃ ≡ (x₀ = 2^k₀ ∧ k₀ ≤ n ∧ k₀ < n ∧ x = x₀*2 ∧ k = k₀+1)
㱺 x₀*2 = 2^(k₀+1) ∧ k₀ +1< n+1 ∧ (x = x₀*2 ∧ k = k₀+1)
㱺 x = 2^k ∧ k < n+1
㱺 x = 2^k ∧ k ≤ n
≡ p
3. q ≡ r = X*Y - x*y
q₁ ≡ wp(x := x/2, q) ≡ (r = X*Y - x*y)[x/2 / x] ≡ r = X*Y - (x/2)*y
q₂ = wp(r := r+y, q₁) ≡ (r = X*Y - (x/2)*y)[2*y/y] ≡ r = X*Y - (x/2)*(2*y)
q₃ ≡ q ∧ even(x) ≡ r = X*Y - x*y ∧ even(x)
q₄ ≡ q ∧ odd(x) ≡ r = X*Y - x*y ∧ odd(x)
q₅ ≡ sp(q₄, r := r+y) ≡ r₀ = X*Y - x*y ∧ odd(x) ∧ r = r₀+y
q₆ ≡ sp(q₅, x := x-1) ≡ r₀ = X*Y - x₀*y ∧ odd(x₀) ∧ r = r₀+y ∧ x = x₀-1
R₁, R₂ ≡ assignment (backward)
R₃, R₄ ≡ assignment (forward)
R₅ ≡ conditional / if-else 5,10
 We can be a little flexible with rule names: while loop and loop are ok; similarly conditional and if-else are ok. †
CS Dept., Illinois Institute of Technology - 3 - © J. Sasaki 2022