7h4um

Some exercise solutions for

Verification of Sequential and Concurrent Programs. Krzysztof R. Apt, Frank S. de Boer, Ernst-R ¨udiger Olderog. Series: Texts in Computer Science. Springer. 3rd ed. 2nd Printing. ISBN: 978-1-84882-744-8

2.9 Exercises

2.1

i

\begin{aligned} (p \lor (q \lor r)) \land (q \to (r \to p)) \\ \equiv & (p \lor (q \lor r)) \land (q \to (\neg r \lor p)) \\ \equiv & (p \lor (q \lor r)) \land (\neg q \lor (\neg r \lor p)) \\ \equiv & (p \lor (q \lor r)) \land (\neg q \lor \neg r \lor p) \\ \equiv & (p \lor (q \lor r)) \land (p \lor (\neg q \lor \neg r)) \\ \equiv & p \lor ((q \lor r) \land (\neg q \lor \neg r)) \end{aligned}

ii

\begin{aligned} (s < t \lor s = t) \land t < u \\ \equiv & s \leq t \land t < u \end{aligned}

iii

\begin{aligned} \exists x : (x < t \land (p \land (q \land r))) \lor s = u \\ \equiv & (\exists x : x < t \land (p \land (q \land r))) \lor s = u \\ \equiv & ((\exists x : x < t) \land (p \land (q \land r))) \lor s = u \\ \equiv & ((\exists x : x < t) \land p \land q \land r) \lor s = u \end{aligned}

2.2

i

\begin{aligned} (x + y) [x := z] [z := y] \\ \equiv & (z + y) [z := y] \\ \equiv & y + y \end{aligned}

ii

\begin{aligned} (a [x] + y) [x := z] [a [2] := 1] \\ \equiv & (a [z] + y) [a [2] := 1] \\ \equiv & if z [a [2] := 1] = 2 then 1 else a [z [a [2] := 1]] fi + y \\ \equiv & if z = 2 then 1 else a [z] fi + y \end{aligned}

iii

\begin{aligned} a [a [2]] [a [2] := 2] \\ \equiv & 2 \end{aligned}

2.3

i

\begin{aligned} σ [x := 0] (a [x]) \\ = & (σ [x := 0] (a)) (σ [x := 0] (x)) \\ = & σ (a) (0) \\ = & σ (a [0]) \end{aligned}

ii

\begin{aligned} σ [y := 0] (a [x]) \\ = & (σ [y := 0] (a)) (σ [y := 0] (x)) \\ = & σ (a) (σ (x)) \\ = & σ (a [x]) \end{aligned}

iii

\begin{aligned} σ [a [0] := 2] (a [x]) \\ = & σ [a [0] := 2] (a) (σ [a [0] := 2] (x)) \\ = & σ [a [0] := 2] (a) (σ (x)) \\ = & {\begin{cases} 2 & if σ (x) = 0, \\ σ (a [x]) & otherwise . \end{cases} \end{aligned}

iv

\begin{aligned} τ [a [x] := τ (x)] (a [1]) \\ = & σ [x := 1] [a [1] := 2] [a [x] := 1] (a) (1) \\ = & 1 \end{aligned}

2.4

i

\begin{aligned} σ ⊨ p \land (q \land r) \\ ⟺ & (σ ⊨ p) \land (σ ⊨ (q \land r)) \\ ⟺ & (σ ⊨ p) \land ((σ ⊨ q) \land (σ ⊨ r)) \\ ⟺ & (σ ⊨ p) \land (σ ⊨ q) \land (σ ⊨ r) \\ ⟺ & (σ ⊨ p \land q) \land (σ ⊨ r) \\ ⟺ & σ ⊨ (p \land q) \land r \end{aligned}

ii

\begin{aligned} σ ⊨ p \lor (q \lor r) \\ ⟺ & (σ ⊨ p) \lor (σ ⊨ q) \lor (σ ⊨ r) \\ ⟺ & (σ ⊨ p \lor q) \lor (σ ⊨ r) \\ ⟺ & σ ⊨ (p \lor q) \lor r \end{aligned}

iii

\begin{aligned} σ ⊨ p \lor (q \land r) \\ ⟺ & (σ ⊨ p) \lor (σ ⊨ (q \land r)) \\ ⟺ & (σ ⊨ p) \lor ((σ ⊨ q) \land (σ ⊨ r)) \\ ⟺ & ((σ ⊨ p) \lor (σ ⊨ q)) \land ((σ ⊨ p) \lor (σ ⊨ r)) \\ ⟺ & σ ⊨ (p \lor q) \land (p \lor r) \end{aligned}

iv

Similar to the above.

v

\begin{aligned} σ ⊨ \exists x : (p \lor q) \\ ⟺ & σ [x := d] ⊨ p \lor q \\ ⟺ & (σ [x := d] ⊨ p) \lor (σ [x := d] ⊨ q) \\ ⟺ & σ ⊨ \exists x : p \lor \exists x : q \end{aligned}

vi

Similar to the above.

2.5

i

No. e.g. $p (x) \equiv (x = 0), q (x) \equiv (x = 1)$

L.H.S is always false, since $x$ has to be $0$ and $1$ at the same time.

R.H.S is true, since $p$ and $q$ can use different $x$ .

ii

Similar to the above.

iii

\begin{aligned} (\exists x : z = x + 1) [z := x + 2] \\ \equiv & (\exists x : z = x + 1) [x := y] [z := x + 2] \\ \equiv & (\exists y : z = y + 1) [z := x + 2] \\ \equiv & \exists y : x + 2 = y + 1 \end{aligned}

iv

\begin{aligned} (\exists x : a [s] = x + 1) [a [s] := x + 2] \\ \equiv & (\exists y : a [s] = y + 1) [a [s] := x + 2] \\ \equiv & \exists y : x + 2 = y + 1 \end{aligned}

2.6

i

\begin{aligned} σ ⊨ \forall x : p \\ ⟹ & { definition of \forall} \\ \forall τ : σ = τ mod x ⟹ τ ⊨ p \\ ⟹ & { let τ = σ [x := d], where d \in D_{T}} \\ \forall d \in D_{T} : σ [x := d] ⊨ p \end{aligned}

\begin{aligned} \forall d \in D_{T} : σ [x := d] ⊨ p \\ ⟹ & { suppose for any τ such that σ = τ mod x} \\ \forall τ : σ = τ mod x ⟹ τ ⊨ p \\ ⟹ & {definition of \forall} \\ σ ⊨ \forall x : p \end{aligned}

ii

Similar to the above.

2.7

i

\begin{aligned} \llbracket \neg p \rrbracket \\ = & {meaning of an assertion} \\ {σ \in Σ ∣ σ ⊨ \neg p} \\ = & {definition of negation} \\ {σ \in Σ ∣ σ ⊨ p}^{c} \\ = & {meaning of an assertion} \\ Σ - {σ \in Σ ∣ σ ⊨ p} \end{aligned}

ii

\begin{aligned} \llbracket p \lor q \rrbracket \\ = & {meaning of an assertion} \\ {σ ∣ σ ⊨ p \lor q} \\ = & {definition of disjunction} \\ {σ ∣ (σ ⊨ p) \lor (σ ⊨ q)} \\ = & {for any τ in the set above, (τ ⊨ p) \lor (τ ⊨ q)} \\ {σ ∣ σ ⊨ p} \cup {σ ∣ σ ⊨ q} \\ = & {meaning of an assertion} \\ \llbracket p \rrbracket \cup \llbracket q \rrbracket \end{aligned}

iii

Similar to the above.

iv

\begin{aligned} p \to q \\ ⟹ & {for any τ ⊨ p, apply p \to q} \\ (τ ⊨ p) \to (τ ⊨ q) \\ ⟹ & {definition of implication} \\ τ ⊨ p \to q \\ ⟹ & {summarize} \\ τ \in {σ ∣ σ ⊨ p} \to τ \in {σ ∣ σ ⊨ p \to q} \\ ⟹ & {definition of subset} \\ {σ ∣ σ ⊨ p} \subseteq {σ ∣ σ ⊨ p \to q} \\ ⟹ & {meaning of an assertion} \\ \llbracket p \rrbracket \subseteq \llbracket q \rrbracket \end{aligned}

v

Similar to the above.

2.8

i

Since both $σ$ and $τ$ agree on all variables in the expression $s$ , the evaluated result must be the same.

ii

Since both $σ$ and $τ$ agree on all free variables of $p$ , the truth value of $p$ under $σ$ and $τ$ must be the same. Therefore, $σ ⊨ p$ if and only if $τ ⊨ p$ .

2.9 Exercises ​

2.1 ​

i ​

ii ​

iii ​

2.2 ​

i ​

ii ​

iii ​

2.3 ​

i ​

ii ​

iii ​

iv ​

2.4 ​

i ​

ii ​

iii ​

iv ​

v ​

vi ​

2.5 ​

i ​

ii ​

iii ​

iv ​

2.6 ​

i ​

ii ​

2.7 ​

i ​

ii ​

iii ​

iv ​

v ​

2.8 ​

i ​

ii ​

2.9 Exercises

2.1

i

ii

iii

2.2

i

ii

iii

2.3

i

ii

iii

iv

2.4

i

ii

iii

iv

v

vi

2.5

i

ii

iii

iv

2.6

i

ii

2.7

i

ii

iii

iv

v

2.8

i

ii