# Lösungsvorschlag Formal Methods Endterm 2010

Wechseln zu: Navigation, Suche

## Assignment 1

### (a)

See Exercise Sheet 10, Assignment 1 (FS15)

### (b)

See Exercise Sheet 11, Assignment 1 (FS15)

## Assignment 2

<s1,sig> -> sig'     <(s;s2);for (skip, b, s2) s end, sig'> -> sig"
------------------------------------------------------------------------- ForT      B[b]sig' = tt
<for (s1, b, s2) s end, sig> -> sig"

                           <s1,sig> -> sig'
------------------------------------------------------------------------- ForF      B[b]sig' = ff
<for (s1, b, s2) s end, sig> -> sig'


## Assignment 3

s1 = while true do skip end

s2 = skip

• There is a derivation tree for <s1 [] s2, sig> -> sig'. Since there is only one branch which terminates successfully (s2), non-determinism chooses this branch. However, <if true then s1 else s2 end, sig> -> sig' is not the same, since <if true then s1 else s2 end, sig> -> sig' can't exist.
• We show <if b then s1 else s2 end, sig> -> sig' => |- <s1 [] s2, sig> -> sig' by induction on the shape of the derivation tree. Thus, we assume <if b then s1 else s2 end, sig> -> sig'. Let b, s1, s2, sig, sig' be arbitrary. We consider the last rule applied to <if b then s1 else s2 end, sig> -> sig':
 IfT: With the first rule for s1[]s2 we can derive <s1[]s2, sig> -> sig'

IfF: With the second rule for s1[]s2 we can derive <s1[]s2, sig> -> sig'


## Assignment 4

Invariant: $\{i\leq j\land x=y^{i}\land j>0\land y\neq 0\}$

$\{y\neq 0\land j\geq 0\}$

if j>0 then


$\{j\geq 0\land y\neq 0\land j>0\}$
|=
$\{0\leq j\land 1=y^{0}\land j>0\land y\neq 0\}$

 x := 1;


$\{0\leq j\land x=y^{0}\land j>0\land y\neq 0\}$

 i := 0;


$\{i\leq j\land x=y^{i}\land j>0\land y\neq 0\}$

 while j # i do


$\{i\leq j\land x=y^{i}\land j>0\land y\neq 0\land j\neq i\}$
|=
$\{i+1\leq j\land x*y=y^{i+1}\land j>0\land y\neq 0\}$

  x:= x*y;


$\{i+1\leq j\land x=y^{i+1}\land j>0\land y\neq 0\}$

  i := i+1


$\{i\leq j\land x=y^{i}\land j>0\land y\neq 0\}$

 end


$\{i\leq j\land x=y^{i}\land j>0\land y\neq 0\land j=i\}$
|=
$\{x=y^{j}\land y\neq 0\}$

else


$\{j\geq 0\land j\leq 0\land y\neq 0\}$
|=
$\{j=0\land y\neq 0\}$
|=
$\{1=y^{j}\land y\neq 0\}$

 x := 1


$\{x=y^{j}\land y\neq 0\}$

end


$\{x=y^{j}\land y\neq 0\}$

## Assignment 5

• =>
We show this by induction on the shape of the derivation tree. Let P,Q,x,e be arbitrary. We consider the last rule applied to |- {P} x:=e {Q}:

Ass: We get P = R[x -> e] and Q = R for some R. Thus, R[x -> e] |= R[x -> e] is trivially true.

Cons: We get |- {P'} x:=e {Q'} and P |= P' and Q' |= Q. By using our induction hypothesis, we can derive P' |= Q'[x -> e]. We can further
derive that P |= P' |= Q'[x -> e] |= Q[x -> e] by using the provided lemma.

• <=
We show this directly. Let P,Q,x,e be arbitrary. We assume that P |= Q[x -> e].
We now construct a derivation tree T such that root(t) = {P} x:=e {Q}:

--------------------- Ass
{Q[x -> e]} x:=e {Q}
--------------------- Cons*
{P} x:=e {Q}

*P |= Q[x -> e] true by assumption, Q |= Q trivially true.


## Assignment 6

See Exercise Sheet 13, Assignment 5 (FS15)