CS 536 Science Of Programming Course ________ 1. For x and y of type int, {y 0} x := y {x 1} if and only if a. (y) 1 b. (y) 0 c. (y) 2 d. (y) gt;...

CS 536 Science Of Programming Course

________ 1. For x and y of type int, σ ⊨ {y ≥ 0} x := y {x² ≥ 1} if and only if

a. σ(y) ≥ 1 b. σ(y) ≠ 0 c. σ(y) ≥ 2 d. σ(y) > σ(x)

________ 2. For nondeterministic S, if σ ⊨ {p} S {q} then

a. If σ ⊨ ¬p and τ ∈ M(S, σ), then τ = ⊥ or τ ⊨ ¬q

b. If σ ⊨ ¬p, then M(S, σ) = {⊥}

c. If σ ⊨ p, then ⊥ ∈ M(S, σ)

d. If σ ⊨ p and τ ∈ M(S, σ), then τ = ⊥ or τ ⊨ q

________ 3. If σ ⊭ {p} S {q}, then

a. σ ⊨ p, ⊥ ∉ M(S, σ) and M(S, σ) ⊭ q c. σ may or may not ⊨ p

b. σ ⊨ ¬p and M(S, σ) may or may not ⊨ q d. σ = ⊥

________ 4. If w ≡ wp(S, q) and S is deterministic, then

a. σ ⊨tot {w} S {q} but σ ⊭ {¬w} S {¬q} is possible

b. σ ⊭ {w} S {q} and σ ⊭ {¬w} S {¬q} are possible at the same time

c. σ ⊨tot {w} S {q} and σ ⊨ {¬w} S {¬q}

d. If w → w₁, then σ ⊨tot {w₁} S {q} and vice versa

For Problems 7 and 8, let p ≡ x ÷ y < z ∧ ∃x . x < a → ∀y . x ÷ y > y-a.

________ 7. Let v be a fresh variable. For p as above, p[y-z⧸x] ≡

a. (y-z) ÷ y < z ∧ ∃v . y-z < a → ∀y . (y-z) ÷ y > y-a

b. (y-z) ÷ y < z ∧ ∃x . x < a → ∀y . x ÷ y > y-a

c. x ÷ y < z ∧ ∃x . x < a → ∀y . x ÷ y > y-a (i.e., it's the same as p)

d. (y-z) ÷ y < z ∧ ∃x . x < a → ∀y . (y-z) ÷ y > y-a

________ 8. Let v and w be fresh variables. For p as above, p[x+y⧸a][y-a⧸x] ≡

a. (y-a) ÷ y < z ∧ ∃v . (y-a) < x+y → ∀w . (y-a) ÷ y > y-(x+y)

b. (x ÷ y < z ∧ ∃x . x < y-a → ∀y . x ÷ y > y-(y-a)) ((x+y) ÷ a) ((y-a) ÷ x)

c. (y-a) ÷ y < z ∧ ∃v . v < (y-a)+y → ∀w . v ÷ w > w-((y-a)+y)

d. (y-(x+y)) ÷ y < z ∧ ∃v . v < x+y → ∀y . (y-(x+y)) ÷ y > y-(x+y)