HW 6 Syntactic Substitution, Forward Assignment, & sp

CS 536: Science of Programming HW 6
Syntactic Substitution, Forward Assignment, & sp
CS 536: Science of Programming
Problems [60 points total]
Class 12: Syntactic Substitutions [30 points]
For Problems 1 – 4, Let p ≡ x*y < f(a) ∨∃x . x ≥ a*y → ∃y . f(x*y) > a-y+z and calculate the substitutions below. Show some detail if you want partial credit for a wrong answer. Just do the syntactic
calculations. Don't do any arithmetic or logical simplifications.
1. [4 points] p[y+z⧸x]
2. [6 points] p[a-y⧸y]
3. [9 points] p[a*y⧸a]
4. [11 points] p[x÷y⧸a][y-z⧸x]
Lecture 13: Forward Assignment; Strongest Postconditions [30 points]
5. [2 points] Give an example of an S such that ⊨ {T} S {sp(T, S)} but ⊭tot {T} S {sp(T, S)}.
6. [3 points] Syntactically calculate sp(x < y ∧ x+y ≤ n, x := f(x+y); y := g(x*y)). Don't simplify the
result.
For Problems 7 – 10, calculate each sp or wp result syntactically. If simplification is requested, do
the syntactic calculation first, then simplify, maintaining logical equivalence unless asked otherwise.
7. [3 points] Calculate and then logically simplify sp(x = 2^k, x := x/2).
8. [3 points] Calculate (but don't simplify) wp(x := x/2, x = 2^k).
9. [7 = 3+4 points]. Let S ≡ if even(x) then x := x+1 fi. (Let even(x) ≡ x%2 = 0 and odd(x) ≡ x%2 ≠ 0.)
a. Calculate and then logically simplify wp(S, odd(x)).
b. Calculate and then logically simplify sp(x = x₀, S). As part of simplification, drop x₀. (The
simplified result will be ⇐ but not 㱻 the unsimplified result.)
10. [12 = 7+5 points]. Let S ≡ if x < b[mid] then right := m else left := m fi and let p′ ≡ left = left₀ ∧
right = right₀.
a. Calculate (but don't simplify sp(p ∧ p′, S) where
p ≡ left< right–1 ∧ mid = (left + right)/2 ∧ b[left]≤ x < b[right].
b. Calculate (but don't simplify sp(p ∧ p′, S) where
p ≡ –1 ≤ left–1 ≤ right ∧ mid = (left + right)/2 ∧ (x ∈ b[0…n–1] 㲗 x ∈ b[left..right])
(Notation: x ∈ b[y..z] ≡ member(x, b, y, z))
CS Dept., Illinois Institute of Technology – 1 – © James Sasaki, 2022