Lösungsvorschlag Formal Methods Endterm 2010

Aus VISki
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:



if j>0 then


|=

 x := 1;


 i := 0;


 while j # i do


|=

  x:= x*y;


  i := i+1


 end


|=

else


|=

|=

 x := 1


end


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)