# 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] = ${\displaystyle \sigma [j\mapsto 2,r\mapsto 0]}$

Derivation Sequence:

1. 〈s, [3]〉→₁
2. 〈r := 1; l, [3]〉→₁
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: ${\displaystyle \{(i\geq 0)\land sum={\frac {N*(N+1)}{2}}-{\frac {i*(i+1)}{2}}\}}$

Proof outline

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

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

 i := n


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

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

 sum := 0


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

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

 while i # 0 do


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

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

   sum := sum + i;


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

   i := i - 1;


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

 end


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

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

## Assignment 3

Claim: ${\displaystyle \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 "${\displaystyle \Rightarrow }$"

• I'll do a proof by induction on the shape of the inference tree of ${\displaystyle \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, ${\displaystyle \lbrace P\rbrace {\text{while b do skip end}}\lbrace P\land \lnot b\rbrace }$

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

• Case CONS_Ax:
• From CONS_Ax we know, there exists an inference tree for ${\displaystyle \lbrace P'\,\rbrace {\text{while b do skip end}}\lbrace Q'\,\rbrace }$, where ${\displaystyle P\implies P'\land Q'\implies Q}$
• By applying the induction hypothesis to ${\displaystyle \lbrace P'\,\rbrace {\text{while b do skip end}}\lbrace Q'\,\rbrace }$, we get ${\displaystyle (P'\land \lnot b)\implies Q'}$
• Because we have ${\displaystyle P\implies P'}$ and ${\displaystyle Q'\implies Q}$, we can build following chain of implications: ${\displaystyle (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 ${\displaystyle \lbrace P'\rbrace {\text{while b do skip end}}\lbrace Q'\rbrace }$, we get ${\displaystyle P'\implies Q'}$
• Old Version: Now we have ${\displaystyle (P\implies P')\land (P'\implies Q')\land (Q'\implies Q)}$ thus ${\displaystyle P\implies Q}$

Proof of "${\displaystyle \Leftarrow }$"

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

We can construct a derivation tree for ${\displaystyle \lbrace P\rbrace {\text{while b do skip end}}\lbrace Q\rbrace }$ as follows: ${\displaystyle {\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: ${\displaystyle \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 ${\displaystyle i}$, i.e. the length of the derivation sequence):

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

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

• Case ${\displaystyle i=0}$
• If ${\displaystyle i=0}$ the implication holds trivially since there is no derivation sequence of length ${\displaystyle 0}$ from a non-final state into a final state in the SOS.
• Case ${\displaystyle i\geq 1}$
• For this case we proceed by a direct proof, i.e. we assume, for an arbitrary ${\displaystyle i\geq 1}$, that ${\displaystyle \langle s_{1};s_{2},\sigma \rangle \rightarrow _{1}^{i}\sigma '}$ holds and then show that ${\displaystyle \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 ${\displaystyle SEQ1_{SOS}}$
• From the rule ${\displaystyle SEQ1_{SOS}}$ follows: ${\displaystyle \langle s_{1};s_{2},\sigma \rangle \rightarrow _{1}\langle s_{2},\sigma ''\rangle \rightarrow _{1}^{i-1}\sigma '}$ for some state ${\displaystyle \sigma ''}$
• The first transition is justified by the following derivation tree: ${\displaystyle {\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 ${\displaystyle PAR2_{SOS}}$:${\displaystyle {\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: ${\displaystyle \langle s_{1}{\text{ par }}s_{2},\sigma \rangle \rightarrow _{1}\langle s_{2},\sigma ''\rangle \rightarrow _{1}^{i-1}\sigma '}$
• So ${\displaystyle \langle s_{1}{\text{ par }}s_{2},\sigma \rangle \rightarrow _{1}^{i}\sigma '}$ holds
• Case ${\displaystyle SEQ2_{SOS}}$
• From the rule ${\displaystyle SEQ2_{SOS}}$ follows: ${\displaystyle \langle s_{1};s_{2},\sigma \rangle \rightarrow _{1}\langle s_{1}';s_{2},\sigma ''\rangle \rightarrow _{1}^{i-1}\sigma '}$ for some statement ${\displaystyle s_{1}'}$ and some state ${\displaystyle \sigma ''}$
• The first transition is justified by the following derivation tree: ${\displaystyle {\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 ${\displaystyle PAR1_{SOS}}$: ${\displaystyle {\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 ${\displaystyle \langle s_{1}';s_{2},\sigma ''\rangle \rightarrow _{1}^{i-1}\sigma '}$, we get (possible because ${\displaystyle i-1 and because ${\displaystyle i\geq 1}$ ${\displaystyle i-1}$ is for sure greater or equal to 0): ${\displaystyle \langle s_{1}'{\text{ par }}s_{2},\sigma ''\rangle \rightarrow _{1}^{i-1}\sigma '}$
• Putting all together yields ${\displaystyle \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 ${\displaystyle \langle s_{1}{\text{ par }}s_{2},\sigma \rangle \rightarrow _{1}^{i}\sigma '}$ holds

QED

let ${\displaystyle s_{1}}$ be

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


and ${\displaystyle s_{2}}$

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


and ${\displaystyle \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 ${\displaystyle \sigma '[x\mapsto 30]}$, which is not reachable from either 〈${\displaystyle s_{1};s_{2},\sigma }$〉 nor 〈${\displaystyle 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;

• ${\displaystyle \square (}$request_m ${\displaystyle \implies \diamond }$ answer_m${\displaystyle )}$