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{array}{rl}& (p\vee (q\vee r))\wedge (q\to (r\to p))\\ \equiv & (p\vee (q\vee r))\wedge (q\to (\mathrm{\neg }r\vee p))\\ \equiv & (p\vee (q\vee r))\wedge (\mathrm{\neg }q\vee (\mathrm{\neg }r\vee p))\\ \equiv & (p\vee (q\vee r))\wedge (\mathrm{\neg }q\vee \mathrm{\neg }r\vee p)\\ \equiv & (p\vee (q\vee r))\wedge (p\vee (\mathrm{\neg }q\vee \mathrm{\neg }r))\\ \equiv & p\vee ((q\vee r)\wedge (\mathrm{\neg }q\vee \mathrm{\neg }r))\end{array}$$

ii

$$\begin{array}{rl}& (s<t\vee s=t)\wedge t<u\\ \equiv & s\le t\wedge t<u\end{array}$$

iii

$$\begin{array}{rl}& \text{exist}x:(x<t\wedge (p\wedge (q\wedge r)))\vee s=u\\ \equiv & (\text{exist}x:x<t\wedge (p\wedge (q\wedge r)))\vee s=u\\ \equiv & ((\text{exist}x:x<t)\wedge (p\wedge (q\wedge r)))\vee s=u\\ \equiv & ((\text{exist}x:x<t)\wedge p\wedge q\wedge r)\vee s=u\end{array}$$

2.2

i

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

ii

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

iii

$$\begin{array}{rl}& a[a[2]][a[2]:=2]\\ \equiv & 2\end{array}$$

2.3

i

$$\begin{array}{rl}& \sigma [x:=0](a[x])\\ =& (\sigma [x:=0](a))(\sigma [x:=0](x))\\ =& \sigma (a)(0)\\ =& \sigma (a[0])\end{array}$$

ii

$$\begin{array}{rl}& \sigma [y:=0](a[x])\\ =& (\sigma [y:=0](a))(\sigma [y:=0](x))\\ =& \sigma (a)(\sigma (x))\\ =& \sigma (a[x])\end{array}$$

iii

$$\begin{array}{rl}& \sigma [a[0]:=2](a[x])\\ =& \sigma [a[0]:=2](a)(\sigma [a[0]:=2](x))\\ =& \sigma [a[0]:=2](a)(\sigma (x))\\ =& \{\begin{array}{ll}2& \text{if }\sigma (x)=0,\\ \sigma (a[x])& \text{otherwise}.\end{array}\end{array}$$

iv

$$\begin{array}{rl}& \tau [a[x]:=\tau (x)](a[1])\\ =& \sigma [x:=1][a[1]:=2][a[x]:=1](a)(1)\\ =& 1\end{array}$$

2.4

i

$$\begin{array}{rl}& \sigma \models p\wedge (q\wedge r)\\ ⟺& (\sigma \models p)\wedge (\sigma \models (q\wedge r))\\ ⟺& (\sigma \models p)\wedge ((\sigma \models q)\wedge (\sigma \models r))\\ ⟺& (\sigma \models p)\wedge (\sigma \models q)\wedge (\sigma \models r)\\ ⟺& (\sigma \models p\wedge q)\wedge (\sigma \models r)\\ ⟺& \sigma \models (p\wedge q)\wedge r\end{array}$$

ii

$$\begin{array}{rl}& \sigma \models p\vee (q\vee r)\\ ⟺& (\sigma \models p)\vee (\sigma \models q)\vee (\sigma \models r)\\ ⟺& (\sigma \models p\vee q)\vee (\sigma \models r)\\ ⟺& \sigma \models (p\vee q)\vee r\end{array}$$

iii

$$\begin{array}{rl}& \sigma \models p\vee (q\wedge r)\\ ⟺& (\sigma \models p)\vee (\sigma \models (q\wedge r))\\ ⟺& (\sigma \models p)\vee ((\sigma \models q)\wedge (\sigma \models r))\\ ⟺& ((\sigma \models p)\vee (\sigma \models q))\wedge ((\sigma \models p)\vee (\sigma \models r))\\ ⟺& \sigma \models (p\vee q)\wedge (p\vee r)\end{array}$$

iv

Similar to the above.

v

$$\begin{array}{rl}& \sigma \models \text{exist}x:(p\vee q)\\ ⟺& \sigma [x:=d]\models p\vee q\\ ⟺& (\sigma [x:=d]\models p)\vee (\sigma [x:=d]\models q)\\ ⟺& \sigma \models \text{exist}x:p\vee \text{exist}x:q\end{array}$$

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{array}{rl}& (\text{exist}x:z=x+1)[z:=x+2]\\ \equiv & (\text{exist}x:z=x+1)[x:=y][z:=x+2]\\ \equiv & (\text{exist}y:z=y+1)[z:=x+2]\\ \equiv & \text{exist}y:x+2=y+1\end{array}$$

iv

$$\begin{array}{rl}& (\text{exist}x:a[s]=x+1)[a[s]:=x+2]\\ \equiv & (\text{exist}y:a[s]=y+1)[a[s]:=x+2]\\ \equiv & \text{exist}y:x+2=y+1\end{array}$$

2.6

i

$$\begin{array}{rl}& \sigma \models \mathrm{\forall }x:p\\ ⟹& \text{{ definition of }\mathrm{\forall }\text{ }}\\ & \mathrm{\forall }\tau :\sigma =\tau \text{ mod }x⟹\tau \models p\\ ⟹& \text{{ let }\tau =\sigma [x:=d]\text{, where }d\in {\mathcal{D}}_T\text{ }}\\ & \mathrm{\forall }d\in {\mathcal{D}}_T:\sigma [x:=d]\models p\end{array}$$$$\begin{array}{rl}& \mathrm{\forall }d\in {\mathcal{D}}_T:\sigma [x:=d]\models p\\ ⟹& \text{{ suppose for any }\tau \text{ such that }\sigma =\tau \mathbf{\text{ mod }}x\text{ }}\\ & \mathrm{\forall }\tau :\sigma =\tau \text{ mod }x⟹\tau \models p\\ ⟹& \text{{definition of }\mathrm{\forall }\text{}}\\ & \sigma \models \mathrm{\forall }x:p\end{array}$$

ii

Similar to the above.

2.7

i

$$\begin{array}{rl}& \text{llbracket}\mathrm{\neg }p\text{rrbracket}\\ =& \text{{meaning of an assertion}}\\ & \{\sigma \in \mathrm{\Sigma }\mid \sigma \models \mathrm{\neg }p\}\\ =& \text{{definition of negation}}\\ & \{\sigma \in \mathrm{\Sigma }\mid \sigma \models p{\}}^c\\ =& \text{{meaning of an assertion}}\\ & \mathrm{\Sigma }-\{\sigma \in \mathrm{\Sigma }\mid \sigma \models p\}\end{array}$$

ii

$$\begin{array}{rl}& \text{llbracket}p\vee q\text{rrbracket}\\ =& \text{{meaning of an assertion}}\\ & \{\sigma \mid \sigma \models p\vee q\}\\ =& \text{{definition of disjunction}}\\ & \{\sigma \mid (\sigma \models p)\vee (\sigma \models q)\}\\ =& \text{{for any }\tau \text{ in the set above, }(\tau \models p)\vee (\tau \models q)\text{}}\\ & \{\sigma \mid \sigma \models p\}\cup \{\sigma \mid \sigma \models q\}\\ =& \text{{meaning of an assertion}}\\ & \text{llbracket}p\text{rrbracket}\cup \text{llbracket}q\text{rrbracket}\end{array}$$

iii

Similar to the above.

iv

$$\begin{array}{rl}& p\to q\\ ⟹& \text{{for any }\tau \models p\text{, apply }p\to q\text{}}\\ & (\tau \models p)\to (\tau \models q)\\ ⟹& \text{{definition of implication}}\\ & \tau \models p\to q\\ ⟹& \text{{summarize}}\\ & \tau \in \{\sigma \mid \sigma \models p\}\to \tau \in \{\sigma \mid \sigma \models p\to q\}\\ ⟹& \text{{definition of subset}}\\ & \{\sigma \mid \sigma \models p\}\subseteq \{\sigma \mid \sigma \models p\to q\}\\ ⟹& \text{{meaning of an assertion}}\\ & \text{llbracket}p\text{rrbracket}\subseteq \text{llbracket}q\text{rrbracket}\end{array}$$

v

Similar to the above.

2.8

i

Since both $\sigma$ and $\tau$ agree on all variables in the expression $s$, the evaluated result must be the same.

ii

Since both $\sigma$ and $\tau$ agree on all free variables of $p$, the truth value of $p$ under $\sigma$ and $\tau$ must be the same. Therefore, $\sigma \models p$ if and only if $\tau \models p$.