CS 536: Science of Programming - HW5 : Weakest Preconditions 1 & 2; Domain Predicates
Weakest Preconditions 1 & 2; Domain Predicates
CS 536: Science of Programming, Spring 2023 Due Mon Feb 27, 11:59 pm
Problems [60 points total]
Class 10: Weakest Preconditions part 1 [27 points]
1. [3points]LetIF ≡ ifB1 ➞ S1 ☐ B2 ➞ S2 fi andletw1⇔wlp(S1,q)andw2⇔wlp(S2,q). Question: Whyiswlp(IF,q)⇔(B1→w1)∧(B2→w2) butnot(B1∧w1)∨(B2∧w2).
2. [4 points] Which of the following statements behave differently depending on whether S is deterministic or nondeterministic? Explain briefly.
• wp(S,p∨q)→wp(S,p)∨wp(S,q) • wp(S,p)∨wp(S,q)→wp(S,p∨q) • wp(S,p∧q)→wp(S,p)∧wp(S,q) • wp(S,p)∧wp(S,q)→wp(S,p∧q)
3. [20=5*4 points] Consider the statement σ⊨{wlp(S,q)}S{q}. If σ satisfies the precondi- tion, then σ⊨{wlp(S,q)}S{q} is satisfied when
· M ( S , σ ) – ⊥ ⊨ q (description using meaning functions)
· For all τ ∈ M ( S , σ ), τ = ⊥ or τ ⊨ q (equivalent description using states/logic) (Note the description is correct whether S is deterministic or nondeterministic.)
For each of the statements below, assume σ satisfies the precondition and give the mean- ing function requirement and the equivalent logical description. If not specified, S could be deterministic or nondeterministic. If S is deterministic, it could be helpful to use the phrase M(S,σ)={τ}.
1. σ⊭{wlp(S,q)}S{q}
2. σ⊨tot {¬wlp(S,q)}S{¬q}, if S is deterministic
3. σ⊨tot {wp(S,q)}S{q}
4. σ⊭tot {wp(S,q)}S{q}
5. σ⊨{¬wp(S,q)}S{¬q}, if S is deterministic
CS Dept, Illinois Institute of Technology – 1 – © James Sasaki, 2023
CS 536: Science of Programming Wed 2023-02-15, 19:50 HW 5: Classes 10 - 11 Class 11: Weakest Preconditions part 2 [9 points]
4. [9 points] Calculate wlp ( if x < 0 then x := – x fi, x2 ≥ x ). (Don't forget the implicit "else skip" clause.) You can omit intermediate calculations but they might be worth partial credit. After syntactically calculating the wlp, logically simplify the result. (Textual simplifications like
p ∧ p ≡ p are always allowed.)
1. [3 points] Calculate the wlp of the true branch
2. [2 points] Calculate the wlp of the false branch
3. [2 points] Calculate the overall wlp.
4. [2 points] Give the result after logical/arithmetic simplification.
Class 11: Domain Predicates [24 points]
Calculate the wp 's below. Show your intermediate calculations. You can logically simplify your answer as you go and/or at the end or not at all (your preference). (Textual simplifications like p ∧ p ≡ p are always allowed.)
5. [12=4*3 points] wp(S,q) where S≡ y:=y/x and q≡sqrt(y)<x.
1. Calculate D ( S ).
2. Calculate w≡wlp(S,q).
3. Calculate D ( w ).
4. Calculatewp(S,q) (it's⇔D(S)∧w∧D(w)).
6. [12=4*3 points] wp(S,q) where S≡if y≥0 then x:=y/x else x:=–x/y fi and q≡r<x≤y.
1. Calculate D ( S ).
2. Calculate w≡wlp(S,q).
3. Calculate D ( w ).
4. Calculate wp(S,q).
