HW 5:  Weakest Preconditions 1 & 2; Domain Predicates

CS 536: Science of Programming HW 5: 
Weakest Preconditions 1 & 2; Domain Predicates
CS 536: Science of Programming

Problems [60 points total]
Class 10: Weakest Preconditions part 1 [22 points]
1. [3 points] Let IFN ≡ if B₁ ➞ S₁ ☐ B₂ ➞ S₂ fi be a nondeterministic if-fi and let w₁ and w₂ be
wlp(S₁, q) and wlp(S₂, q) respectively. Let p be (B₁ → w₁) ∧ (B₂ → w₂) and let p′ be (B₁ ∧ w₁) ∨
(B₂ ∧ w₂). Question: Why is wlp(IFN, q) 㱻 p but not p′ ′?
2. [4 points] Which of the following (four) statements behave differently depending on whether S
is deterministic or nondeterministic? Explain briefly.
• wp(S, p ∨ q) → and ← wp(S, p) ∨ wp(S, q)
• wp(S, p ∧ q) → and ← wp(S, p) ∧ wp(S, q)
3. [15 = 3*5 points] Let w 㱻 wp(S, q) and let b → w and w → c. Characterize each satisfiability /
validity statement below as Always true, Always false, or Might be true (and might be false).
Explain briefly.
a. if S is deterministic, then ⊨tot {b} S {q }.
b. If S is nondeterministic, then there exists σ such that σ ⊨ {¬c} S {¬q }.
c. If S is nondeterministic, then there exist σ ⊨ ¬c and τ ∈ M(S, σ) such that τ ⊨ q.
Class 11: Weakest Preconditions part 2 [20 points]
Calculate the wlp for each of the following. You can omit intermediate calculations but they might
be worth partial credit. Do only the syntactic calculations; don't simplify the result. E.g., wlp(x := 2,
x*x = 4) ≡ 2*2 = 4, not T.
4. [10 points] wlp(u := u*k; k := u, u > h(k)).
5. [10 points] wlp(if x < 0 then x := –x fi, x² ≥ x). (Don't forget the implicit "else skip" clause.)
CS Dept., Illinois Institute of Technology – 1 – © James Sasaki, 2022
CS 536: Science of Programming Thu 2022-09-29, 17:22 HW 5: Classes 10 - 11
Class 11: Domain Predicates [18 points]
Calculate the wp's below. Show your intermediate calculations. You can simplify your answer as
you go and/or at the end or not at all (your preference). Suggestion: Define S, q, and w and
separately calculate D(S), w ≡ wlp(S, q), and D(w). Combine and give wp(S, q) 㱻 D(S) ∧ w ∧ D(w).
6. [6 points] wp(y := y/x, sqrt(y) < x).
7. [12 points] wp(if y ≥ 0 then x := y / x else x := –x / y fi, r < x ≤ y).
CS Dept., Illinois Institute of Technology – 2 – © James Sasaki, 2022