# Lösungsvorschlag Formal Methods Endterm 2011

## Assignment 1

Abbreviations:

• s:
 r := 1;
while j > 1 do
r := r * j;
j := j - 1;
end

• l:
 while j > 1 do
r := r * j;
j := j - 1;
end

• l' :
 r := r * j;
j := j - 1;

• [2,0] = $\sigma [j\mapsto 2,r\mapsto 0]$

Derivation Sequence:

1. 〈s, 〉→₁
2. 〈r := 1; l, 〉→₁
3. 〈l, [3, 1]〉→₁
4. 〈if j > 1 then l';l else skip end, [3, 1]〉→₁
5. 〈r := r * j; j := j - 1; l, [3, 1]〉→₁
6. 〈j := j -1; l, [3, 3]〉→₁
7. 〈l, [2, 3]〉→₁
8. 〈if j > 1 then l'; l else skip end, [2, 3]〉→₁
9. 〈r := r * j; j := j - 1; l, [2, 3]〉→₁
10. 〈j := j - 1; l, [2, 6]〉→₁
11. 〈l, [1, 6]〉→₁
12. 〈if j > 1 then l'; l else skip end, [1, 6]〉→₁
13. 〈skip. [1, 6]〉→₁
14. 〈[1, 6]〉

## Assignment 2

Invariant: $\{(i\geq 0)\land sum={\frac {N*(N+1)}{2}}-{\frac {i*(i+1)}{2}}\}$

Proof outline

$\{(n=N)\land (n\geq 0)\}$

$\{0=0\land n=n\land n=N\land n\geq 0\}$

 i := n


$\{0=0\land i=n\land n=N\land n\geq 0\}$

$\{0=0\land i=n\land i\geq 0\land n=N\land n\geq 0\}$

 sum := 0


$\{sum=0\land i=n\land n=N\land n\geq 0\}$

$\{(i\geq 0)\land sum={\frac {N*(N+1)}{2}}-{\frac {i*(i+1)}{2}}\}$

 while i # 0 do


$\{(i\neq 0)\land (i\geq 0)\land sum={\frac {N*(N+1)}{2}}-{\frac {i*(i+1)}{2}}\}$

$\{(i-1\geq 0)\land sum+i={\frac {N*(N+1)}{2}}-{\frac {(i-1)*((i-1)+1)}{2}}\}$

   sum := sum + i;


$\{(i-1\geq 0)\land sum={\frac {N*(N+1)}{2}}-{\frac {(i-1)*((i-1)+1)}{2}}\}$

   i := i - 1;


$\{(i\geq 0)\land sum={\frac {N*(N+1)}{2}}-{\frac {i*(i+1)}{2}}\}$

 end


$\{(i=0)\land (i\geq 0)\land sum={\frac {N*(N+1)}{2}}-{\frac {i*(i+1)}{2}}\}$

$sum={\frac {N*(N+1)}{2}}$

## Assignment 3

Claim: $\forall P,Q.\vdash \lbrace P\rbrace {\text{while b do skip end}}\lbrace Q\rbrace \iff (P\land \neg b\implies Q)$

Proof of "$\Rightarrow$"

• I'll do a proof by induction on the shape of the inference tree of $\vdash \lbrace P\rbrace {\text{while b do skip end}}\lbrace Q\rbrace$.
• Out of the six rules of axiomatic semantics, only WH_Ax or CONS_Ax can be at the root of the tree
• Case WH_Ax:
• The rule is as followed defined, $\lbrace P\rbrace {\text{while b do skip end}}\lbrace P\land \lnot b\rbrace$

hence: $Q=(\lnot b\land P)$, thus: $P\land \lnot b\implies Q$

• Case CONS_Ax:
• From CONS_Ax we know, there exists an inference tree for $\lbrace P'\,\rbrace {\text{while b do skip end}}\lbrace Q'\,\rbrace$, where $P\implies P'\land Q'\implies Q$
• By applying the induction hypothesis to $\lbrace P'\,\rbrace {\text{while b do skip end}}\lbrace Q'\,\rbrace$, we get $(P'\land \lnot b)\implies Q'$
• Because we have $P\implies P'$ and $Q'\implies Q$, we can build following chain of implications: $(P\land \lnot b)\implies (P'\land \lnot b)\implies Q'\implies Q$. And we are done.
• Old Version: by applying the induction hypothesis to $\lbrace P'\rbrace {\text{while b do skip end}}\lbrace Q'\rbrace$, we get $P'\implies Q'$
• Old Version: Now we have $(P\implies P')\land (P'\implies Q')\land (Q'\implies Q)$ thus $P\implies Q$

Proof of "$\Leftarrow$"

Direct proof, i.e. we assume $P\land \neg b\implies Q$ for arbitrary $P,Q,b$ and show $\vdash \lbrace P\rbrace {\text{while b do skip end}}\lbrace Q\rbrace$.

We can construct a derivation tree for $\lbrace P\rbrace {\text{while b do skip end}}\lbrace Q\rbrace$ as follows: ${\cfrac {{\cfrac {{\cfrac {{\cfrac {}{\lbrace b\land P\rbrace {\text{skip}}\lbrace b\land P\rbrace }}SKIP_{Ax}}{\lbrace b\land P\rbrace {\text{skip}}\lbrace P\rbrace }}CONS_{Ax},((b\land P)\implies (b\land P))\land ((b\land P)\implies P)}{\lbrace P\rbrace {\text{while b do skip end}}\lbrace \neg b\land P\rbrace }}WH_{Ax}}{\lbrace P\rbrace {\text{while b do skip end}}\lbrace Q\rbrace }}CONS_{Ax},(P\implies P)\land ((\neg b\land P)\implies (P\land \neg b)\implies Q)$

QED

## Assignment 4

Claim: $\forall i\in \mathbb {N} ,\ s_{1},s_{2}\in {\text{Stm}},\ \sigma ,\sigma '\in {\text{State}}\ .\ \langle s_{1};s_{2},\sigma \rangle \rightarrow _{1}^{i}\sigma '\implies \langle s_{1}{\text{ par }}s_{2},\sigma \rangle \rightarrow _{1}^{i}\sigma '$

Proof (by strong induction on $i$, i.e. the length of the derivation sequence):

Induction hypothesis: $\forall k\in \mathbb {N}

Let $s_{1},s_{2},\sigma ,\sigma '$ be arbitrary.

• Case $i=0$
• If $i=0$ the implication holds trivially since there is no derivation sequence of length $0$ from a non-final state into a final state in the SOS.
• Case $i\geq 1$
• For this case we proceed by a direct proof, i.e. we assume, for an arbitrary $i\geq 1$, that $\langle s_{1};s_{2},\sigma \rangle \rightarrow _{1}^{i}\sigma '$ holds and then show that $\langle s_{1}{\text{ par }}s_{2},\sigma \rangle \rightarrow _{1}^{i}\sigma '$ also holds.
• There are two possible rules which can have been applied at the root:
• Case $SEQ1_{SOS}$
• From the rule $SEQ1_{SOS}$ follows: $\langle s_{1};s_{2},\sigma \rangle \rightarrow _{1}\langle s_{2},\sigma ''\rangle \rightarrow _{1}^{i-1}\sigma '$ for some state $\sigma ''$
• The first transition is justified by the following derivation tree: ${\cfrac {\cfrac {...}{\langle s_{1},\sigma \rangle \rightarrow _{1}\sigma ''}}{\langle s_{1};s_{2},\sigma \rangle \rightarrow _{1}\langle s_{2},\sigma ''\rangle }}SEQ1_{SOS}$
• From this we can construct the following derivation tree using the rule $PAR2_{SOS}$:${\cfrac {\cfrac {...}{\langle s_{1},\sigma \rangle \rightarrow _{1}\sigma ''}}{\langle s_{1}{\text{ par }}s_{2},\sigma \rangle \rightarrow _{1}\langle s_{2},\sigma ''\rangle }}PAR2_{SOS}$
• Putting all together we get: $\langle s_{1}{\text{ par }}s_{2},\sigma \rangle \rightarrow _{1}\langle s_{2},\sigma ''\rangle \rightarrow _{1}^{i-1}\sigma '$
• So $\langle s_{1}{\text{ par }}s_{2},\sigma \rangle \rightarrow _{1}^{i}\sigma '$ holds
• Case $SEQ2_{SOS}$
• From the rule $SEQ2_{SOS}$ follows: $\langle s_{1};s_{2},\sigma \rangle \rightarrow _{1}\langle s_{1}';s_{2},\sigma ''\rangle \rightarrow _{1}^{i-1}\sigma '$ for some statement $s_{1}'$ and some state $\sigma ''$
• The first transition is justified by the following derivation tree: ${\cfrac {\cfrac {...}{\langle s_{1},\sigma \rangle \rightarrow _{1}\langle s_{1}',\sigma ''\rangle }}{\langle s_{1};s_{2},\sigma \rangle \rightarrow _{1}\langle s_{1}';s_{2},\sigma ''\rangle }}SEQ2_{SOS}$
• From this we can construct the following derivation tree using the rule $PAR1_{SOS}$: ${\cfrac {\cfrac {...}{\langle s_{1},\sigma \rangle \rightarrow _{1}\langle s_{1}',\sigma ''\rangle }}{\langle s_{1}{\text{ par }}s_{2},\sigma \rangle \rightarrow _{1}\langle s_{1}'{\text{ par }}s_{2},\sigma ''\rangle }}PAR1_{SOS}$
• By applying the induction hypothesis on the second transition, i.e. on $\langle s_{1}';s_{2},\sigma ''\rangle \rightarrow _{1}^{i-1}\sigma '$, we get (possible because $i-1 and because $i\geq 1$ $i-1$ is for sure greater or equal to 0): $\langle s_{1}'{\text{ par }}s_{2},\sigma ''\rangle \rightarrow _{1}^{i-1}\sigma '$
• Putting all together yields $\langle s_{1}{\text{ par }}s_{2},\sigma \rangle \rightarrow _{1}\langle s_{1}'{\text{ par }}s_{2},\sigma ''\rangle \rightarrow _{1}^{i-1}\sigma '$
• So $\langle s_{1}{\text{ par }}s_{2},\sigma \rangle \rightarrow _{1}^{i}\sigma '$ holds

QED

let $s_{1}$ be

(1) x = x + 1;
(2) x = x * 2;


and $s_{2}$

(3) x = x + 2;
(4) x = x * 3;


and $\sigma =[x\mapsto 2]$
then by applying first PAR1_SOS, then PAR3_SOS and repeating these two steps (doing lines 1-3-2-4 in that order), we reach the state $\sigma '[x\mapsto 30]$, which is not reachable from either 〈$s_{1};s_{2},\sigma$〉 nor 〈$s_{2};s_{1},\sigma$

## Assignment 5

active proctype client (int address; mtype language) {
request req;
req.language = language;
dummy.data = 0;
net ! dummy, req;
net ? (ans, _);
do
net ? (ans, _);
:: else -> break
od
}


active proctype server() {
request req;
request dummy;
dummy.language = de;
do
:: net ? (_, req);
if
:: req.language == de -> ans.data = msg_de;
nreq_de = nreq_de + 1;
net ! ans, dummy;
:: else -> ans.data = msg_en;
nreq_en = nreq_en + 1;

• $\square ($request_m $\implies \diamond$ answer_m$)$