HW 4 Sequential Nondeterminism, Hoare Triples 1 & 2

CS 536: Science of Programming HW 4
Sequential Nondeterminism, Hoare Triples 1 & 2
CS 536: Science of Programming

A. Problems [60 points total]
Class 7: Sequential Nondeterminism
1. [13 = 3 + 3 + 7 points] Let DO be the nondeterministic loop
do x ≠ 0 ➞ x := x-1; y := y+1 ☐ x ≠ 0 ➞ x := x-1; y := y+2 od
a. 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
iteration of the loop. I.e., what are the τ where ⟨DO, σ⟩ →³ ⟨DO, τ⟩?
b. Repeat part (a) but for two iterations to get three possible final states.
c. Generalize parts (a) and (b) to κ iterations where 1 < κ ≤ β. I.e., what is Σ′ such that
⟨ DO, σ ⟩ →3*κ ⟨ DO, τ ⟩ iff τ ∈ Σ′?
Class 8: Hoare Triples, pt 1
The questions below have the form “If X, then Y __________ occur”. To answer them, fill in the blank
with “must”, “can't”, or “may or may not”.
• Must occur means X implies Y. (E.g., if x > 1, then x > 0 must occur.)
• Can't occur means X implies ¬Y. (E.g., if x > 1, then x < -3 can't occur.)
• May or may not occur means that either X ∧ Y or X ∧ ¬Y can happen. (E.g., if x > 1, then y = 0
may or may not occur.)
You're not required to justify your answer, though you can if you want to (and you should be able to
if asked in to in an exam).
2. [30 = 15 * 2 points] Below, unless specified, assume that σ ≠ ⊥ and S may or may not be
deterministic.
a. If σ ⊨ {p} S {q} and σ ⊭ p, then ⊥ ∈ M(S, σ) __________ occur.
b. If σ ⊨ {p} S {q} and σ ⊭ p, then M(S, σ) - {⊥} ⊨ q __________ occur.
c. If σ ⊨ {p} S {q} and σ ⊨ p, then ⊥ ∈ M(S, σ) __________ occur.
d. If σ ⊨ {p} S {q} and σ ⊨ p, then M(S, σ) - {⊥} ⊨ q __________ occur.
e. If ⊨tot {p} S {q} then ⊨tot {p} S {T} __________ occur.
f. If ⊨tot {p} S {T} then ⊨tot {p} S {q} __________ occur.
CS Dept., Illinois Institute of Technology – 1 – © James Sasaki, 2022
CS 536: Science of Programming Thu 2022-10-20, 20:21 HW 4: Classes 7 - 9
g. If σ ⊭ {p} S {q} and S is deterministic, then σ ⊨ p, ⊥ ∉ M(S, σ), and M(S, σ) ⊨ ¬q __________ all
occur simultaneously.
h. If ⊥ ∉ M(S, σ), M(S, σ) ⊭ q, and S is deterministic, then M(S, σ) ⊨ ¬q __________ occur.
i. If ⊥ ∉ M(S, σ), M(S, σ) ⊭ q, and S is nondeterministic, then M(S, σ) ⊨ ¬q __________ occur.
j. If M(S, σ) ⊭ q, τ ∈ M(S, σ), and S is nondeterministic, then τ ⊨ q __________ occur.
k. If S is deterministic and σ ⊨ {p} S {q}, then σ ⊨ {p} S {¬q} __________ occur.
l. If σ ⊭tot {p} S {q} and S is deterministic, then σ ⊨ {p} S {¬q} __________ occur.
m. If σ ⊭tot {p} S {q} and S is nondeterministic, then σ ⊨ {p} S {¬q} __________ occur.
n. If σ ⊭ {p} S {q} and S is deterministic, then σ ⊨tot {p} S {¬q} __________ occur.
o. If σ ⊭ {p} S {q} and S is non-deterministic, then σ ⊨tot {p} S {¬q} __________ occur.
Class 9: Hoare Triples, pt 2
3. [2 points] Study the triple {???} b := b+b {b*c ≤ d–b}. Using backward assignment, what can
we use for the precondition of the triple? (Hint: Be careful with parenthesization)
4. [3 points]
a. Using backward assignment, what is u in { u } x := m {1 ≤ x*y ≤ n*m} ?
b. Using backward assignment, what is v in { v } y := n { u } ?
c. Joining parts (a) and (b), what is w in { w } y := n ; x := m {1 ≤ x*y ≤ n*m} ?
5. [4 = 2*2 points] Let p₀ → p, p → p₁, q₀ → q, and q → q₁ all be valid. From {p} S {q}, there are
four triples of the form { pi } S { qj } that get by replacing p by p₀ or p₁ and q by q₀ or q₁.
a. If σ ⊨ {p} S {q}, which of the four triples σ ⊨ { pi } S { qj } is/are also satisfied by σ (under ⊨)?
Briefly justify.
b. If σ ⊨tot {p} S {q}, which of the four triples σ ⊨ {pi} S {qj} is/are also satisfied by σ (under
⊨tot )? Briefly justify.
6. [8 = 4*2 points] Say σ ⊨ {p₁} S {q₁} and σ ⊨ {p₂} S {q₂}.⊥⟨
a. Does σ ⊨ {p₁ ∧ p₂} S {q₁ ∧ q₂}? Justify briefly.
b. Does σ ⊨ {p₁ ∨ p₂} S {q₁ ∨ q₂}? Justify briefly.
c. Does σ ⊨ {p₁ ∧ p₂} S {q₁ ∨ q₂}? Justify briefly.
d. Does σ ⊨ {p₁ ∨ p₂} S {q₁ ∧ q₂}? Justify briefly.
CS Dept., Illinois Institute of Technology – 2 – © James Sasaki, 2022
CS 536: Science of Programming Thu 2022-10-20, 20:21 HW 4: Classes 7 - 9
Sequential Nondeterminism, Hoare Triples 1 & 2
Solutions
2022-10-20 p.1
1. (Nondeterministic loop)
a. {x = β – 1, y = δ+1}, {x = β – 1, y = δ + 2}
b. {x = β – 2, y = δ′ } where δ′ is 2, 3, or 4.
2 times, we add 1 or 2 to δ, so we add a minimum of 2 and a maximum of 4 to δ.
c. {x = β – κ, y = δ″ } where κ ≤ δ″ ≤ 2κ.
κ times, we add 1 or 2 to δ, so we add a minimum of κ and a maximum of 2κ to δ.
2. (wp and wlp properties and relationships)
Must happen: d, e, g, h, i , l, n, o . [2022-10-20] drop i, o
Can't happen: k . [2022-10-20] drop k
May or may not happen: a, b, c, f, j, m. [2022-10-20] add i, k, o
3. (Backward assignment)
(b+b)*c ≤ d–(b+b)
4. (Sequence of assignments)
a. u ≡ 1 ≤ m*y ≤ n*m
b. v ≡ 1 ≤ m*n ≤ n*m
c. w ≡ v ≡ 1 ≤ m*n ≤ n*m
5. (Weakening and strengthening conditions)
a. {p₀} S {q₁} by pre. str. and post. weak.
b. Same: {p₀} S {q₁} by pre. str. and post. weak.
6. (Conjunctions and disjunctions of conditions)
a. Yes. If p₁ ∧ p₂ holds then postcondition q₁ holds because of p₁ and q₂ holds because of p₂,
so postcondition q₁ ∧ q₂ holds.
b. Yes. Say p₁ ∨ p₂ holds. If p₁ holds then q₁ (and therefore q₁ ∨ q₂) holds; alternatively if p₂
holds then q₂ (and therefore q₁ ∨ q₂) holds, and q₁ ∨ q₂ either way.
c. Yes. From part (a), we know q₁ ∧ q₂ holds, which implies that q₁ ∨ q₂ holds.
d. No. From part (b) we know that either q₁ or q₂ (or both) hold, but just knowing q₁ ∨ q₂
doesn't imply that q₁ ∧ q₂ holds.
CS Dept., Illinois Institute of Technology – 3 – © James Sasaki, 2022