CS 536: Science of Programming - HW 4: Sequential Nondeterminism // Hoare Triples 1 & 2
Sequential Nondeterminism, Hoare Triples 1 & 2 CS 536: Science of Programming, Spring 2023
Due Thu Feb 16, 11:59 pm [not Sep 16] 2023-02-13: p.1; 2023-02-15: p.2
A. Problems [60 points total] Class 7: Sequential Nondeterminism
1. [12 = 2 * 6 points] Let D O be the nondeterministic loop [2023-02-13 do/od keywords] do x≠0 ➞ x:=x-1; y:=y+1 ☐ x≠0 ➞ x:=x-1; y:=y+2 od
- First, let's work on what what a typical loop iteration does over an arbitrary state σ={x=β,y=δ}. Assume β≥2 and calculate the two states we can be in after a single iter- ationoftheloop. I.e.,whataretheτ where〈DO,σ〉→3〈DO,τ〉?
- Extend part (a) to do κ iterations where 1 < κ ≤ β . What is the set of final states Σ′ we can reachin3κiterations? I.e.,whatisΣ′={τ∈Σ|〈DO,σ〉→3κ〈DO,τ〉}?
Classes 8 & 9: Hoare Triples, pt 1 & 2
2. [16=4*4 points]
- Using backward assignment, what can we use for precondition p1 in the triple
{p1} b:=b+b{b*c≤d–b}? (Mild hint: Be careful with parenthesization)
- Using backward assignment, what can we use for p2 in {p2}x:=m{1≤x*y≤n*m} ?
- Using backward assignment, what can we use for p3 in { p3 } y := n { p2} ?
- Joining parts (b) and (c), what can we use for p4 in {p4}y:=n; x:=m{1≤x*y≤n*m} ?
3. [6=2*3 points] Letp0→p,p→p1,q0→q,andq→q1 allbevalid. From{p}S{q},thereare four triples of the form {pi}S{qj}that get by replacing p by p0 or p1 and q by q0 or q1.
- Ifσ⊨{p}S{q},whichofthefourtriplesσ⊨{pi }S{qj } is/arealsosatisfiedbyσunder⊨? Briefly justify.
- Repeat part (a) but under total correctness.
4. [8=2*4 points] Say σ⊨{p1}S{q1} and σ⊨{p2}S{q2}. a. Doesσ⊨{p1∧p2}S{q1∨q2}? Justifybriefly.
b. Doesσ⊨{p1∨p2}S{q1∧q2}? Justifybriefly.
tions of correctness triples. Assume σ ≠ ⊥ and S is deterministic.
For (a) and (b), the four statements are σ ⊨ {p}S{q}, σ ⊨ {p}S{¬q}, σ ⊭ {p}S{q}, σ ⊭ {p}S{¬q}
- [4points] Therearefourstatementsoftheformσ(⊨or⊭){p}S {qor¬q}. Which(if any) of them are implied by σ⊨tot {p}S{q}?
- [4points] Thereare[2023-02-15]fourstatementsoftheformσ (⊨or⊭){p}S {qor¬q}. Which (if any) of them are implied by σ⊨tot {T}S{q}?
For (a) and (c), the four statements are σ ⊨ {p}S{q}, σ ⊨ {p}S{¬q}, σ ⊨ {¬p}S{q}, σ ⊨ {¬p}S{¬q}
c. [2 points] There are four statements of the form σ⊨{p or ¬p} S {q or ¬q}. When can all
four of them be satisfied at the same time, or is it impossible?
Definitions
"Σ0partly⊨p" meansthereisaτ∈Σ0withτ⊨p. "Σ0partly⊭p" meansthereisaτ∈Σ0withτ⊨¬p.
6. [8 = 2 * 4 points] Now assume that σ ≠ ⊥ and S is nondeterministic and answer the following questions.
- Therearefourstatementsoftheformσpartly(⊨or⊭){p}S{qor¬q}. If⊥∉M(S,σ), then which (if any) of them are implied by σ⊭{p}S{q}?
- Continuing, which (if any) of the remaining statements can occur (but might not) when σ⊭{p}S{q}?
