Lösungsvorschlag Formal Methods and Functional Programming FS09

Aus VISki
Wechseln zu: Navigation, Suche

Endterm (June 8th, 2009)

Assignment 1 (SOS)

Abbreviations:

  • [2,0] =
  • s₁ = while x#0 do s₂ end
  • s₂ = s₃;s₄
  • s₃ = if (x mod 2=0) then y:=y+x else y:=y-x end
  • s₄ = x:=x-1

Derivation sequence:

  1. 〈s₁ , [2,0]〉→₁
  2. 〈if x#0 then s₂;s₁ else skip end, [2,0]〉→₁
  3. 〈if (x mod 2=0) then y:=y+x else y:=y-x end;s₄;s₁ , [2,0]〉→₁
  4. 〈y:=y+x;s₄;s₁ , [2,0]〉→₁
  5. 〈x:=x-1;s₁ , [2,2]〉→₁
  6. 〈s₁ , [1,2]〉→₁
  7. 〈if x#0 then s₂;s₁ else skip end, [1,2]〉→₁
  8. 〈if (x mod 2=0) then y:=y+x else y:=y-x end;s₄;s₁ , [1,2]〉→₁
  9. 〈y:=y-x;s₄;s₁ , [1,2]〉→₁
  10. 〈x:=x-1;s₁ , [1,1]〉→₁
  11. 〈s₁ , [0,1]〉→₁
  12. 〈if x#0 then s₂;s₁ else skip end, [0,1]〉→₁
  13. 〈skip, [0,1]〉→₁
  14. [0,1]

Justification of the first 4 transitions:

  1. Application of the loop unroll rule.
  2. Sequential composition rule followed by the if-true rule, because evaluates to true.
  3. Sequential composition rule followed by the if-true rule, because evaluates to true.
  4. Sequential composition rule followed by the assignment rule, evaluating to 2.

Assignment 2 (natural semantics)

Claim:

∀ s:Statement. ∀ b:Boolean Expression.
repeat s until b ⇔ s; while not b do s end

Proof: We prove by induction over the shape of derivation trees.

Induction hypothesis: Let s and b be arbitrary. repeat s until b ⇔ s; while not b do s end

Consider the following derivation trees:


  1.  

  2.  

  3.  

  4.  

We prove the implications first from from left to right and then from right to left.

Show ⇒:

Let s and b be arbitrary. Depending on the value of b, we have two rules for the repeat-statement which can apply.

Case .

Consider tree 1 which we constructed using the repeat-statement as the root.
This tree has a single subtree for statement s.
We know that statement s is executed once, and changes the state δ to δ'.
We know that b is evaluated on δ' afterwards.
We can now construct tree 3 with the s;while-statement which has the same properties.
We used the s;while-statement as the root, and then applied the sequential composition rule.
We note that statement s is executed once changing the state δ to δ', and then ¬b is evaluated on δ'. Since we know that b is true on δ', this yields an empty subtree.
Thus the implication holds.

Case

Consider tree 2 which we constructed using the repeat-statement as the root.
If b evaluates to false, the repeat-rule yields a subtree with statement s and again a subtree with the repeat-statement.
We can apply the induction hypothesis on the subtree with the repeat-statement.
The only rule which can be applied on the resulting subtree is sequential composition.
Thus we end up with three subtrees: s, s and while.
We note that state transitions only occur in these subtrees.
We also note that b is evaluated on state ϒ after the first execution of s.
We can now construct tree 4 for the s;while-statement which has the same subtrees.
Thus the implication holds.

Show ⇐:

Let s and b be arbitrary. Depending on the value of b, we have two possible shapes for the derivation tree of the s;while-statement.

Case .

Consider tree 3 which we constructed using the s;while-statement as the root.
As we have already shown, tree 1 is equivalent to tree 3.
Thus the implication holds.

Case

Consider tree 4 which we constructed using the s;while-statement as the root.
As we have already shown, tree 2 is equivalent to tree 4.
Thus the implication holds.


Assignment 3 (Hoare logic)

statement s:
y := 0;
while x > 0 do

y := y + x * x;
x : = x - 1

end
x := y


Proof Outline:
{x = N ∧ N > 0}

{x = N ∧ N > 0 ∧ 0 = 0}

y := 0;

{x = N ∧ N > 0 ∧ y = 0}

{x ≥ 0 ∧ y = }

while x > 0 do

{x > 0 ∧ x ≥ 0 ∧ y = }

{x-1 ≥ 0 ∧ y+x*x = }

y := y + x * x;

{x-1 ≥ 0 ∧ y = }

x := x - 1

{x ≥ 0 ∧ y = }

{x ≥ 0 ∧ y = }

end

{¬(x > 0) ∧ x ≥ 0 ∧ y = }

{y = }

x := y

{x = }

Assignment 4 (axiomatic semantics)

Assignment 5 (WLP)

Claim: ∀ p:Predicate. ∀ s:Statement ∈ IMP. ∀ b:Boolean Expression. wlp(s,P) = P implies ⊢{P} while b do s end {P ∧ ¬B[[b]] }.

Proof on inference trees.

Let p, s, b be arbitrary.

We observe that wlp(s,P) is a function which generates the weakest liberal precondition for s, which satisfies the postcondition P.

Since the implication gives wlp(s,P) = P, we effectively have the Hoare triple {P} s {P} for statement s.

Therefore we can construct the following inference tree using axiomatic semantics rules:

Assignment 6 (Promela)

a) (Promela macro)

 inline produce_item(i) {
   i=1;
   do
   :: i<100 -> i=i+1;
   :: break;
   od
 }

b) (Promela program)

 mtype = {resend,next};
 chan first  = [0] of {byte};
 chan second = [0] of {mtype};
 

 active proctype producer() {
   byte item;
   mtype response;
   
   produce_item(item);
   
   do
   :: first ! item;
      second ? response;
      if
      :: response == next -> produce_item(item);
      :: else -> skip;
      fi
   od
 }
 
 active proctype consumer() {
   byte item;
   
   do
   :: first ? item;
      if
      :: second ! resend;
      :: second ! next;
      fi
   od
 }

Assignment 7 (LTL)

a)

b)

c)

Repetition Exam (September 12th, 2009)

Alternative Solution: Lösungsvorschlag FS 2009

Typing

a)

b)

Constraints:

Induction

Theorem: rev (xs ++ rev ys) = ys ++ rev xs

Proof: Let . I will show by strong structural induction. is my induction hypothesis. I proceed by case analysis on the shape of xs.

Case xs == []:

In this case the equation looks like this:

rev ([] ++ rev ys) = (rev.1) rev (rev ys) = (Lemma 1) ys = (Lemma 2) ys ++ [] = (rev. 1) ys ++ (rev [])

So that case holds.

Case xs == x:foo:

rev (x:foo ++ rev ys) = (app.2) rev (x : (foo ++ rev ys)) = (rev.2) rev (foo ++ rev ys) ++ [x] = (Ind.hyp) (ys ++ rev foo) ++ [x] = (Lemma 3) ys ++ (rev foo ++ [x]) = (rev.2) ys ++ rev (x:foo)

which completes this case. Now all cases are covered so the overall theorem is proven as well.

Lists

-- No one stated the implementation should be efficient...
risers :: Ord a => [a] -> a
risers xs = split xs []
  where 
    split :: Ord a => [a] -> a -> a
    split [] result = reverse result
    split (x:xs) [] = split xs x
    split (x:xs) (result:rest) 
      | x >= (last result) = split xs ((result ++ [x]):rest)
      | x <  (last result) = split xs ([x]:result:rest)

Higher-Order Functions

a)

mapDir :: (Dir -> Dir) -> Block -> Block
mapDir f (Tile []) = Tile []
mapDir f (Tile (list)) = Tile ((flip map) list $ \(direction, block) -> (f direction, mapDir f block))

b)

rotateCw = mapDir turn
  where
    turn :: Dir -> Dir
    turn Up = Right
    turn Right = Down
    turn Down = Left
    turn Left = Up

c)

foldBlock :: ([(Dir, a)] -> a) -> Block -> a
foldBlock function (Tile list) = function list

Operational Semantics

a)

Too lazy. That method using \cfrac is awkward. Consider using bussproofs

b)

s1:

x := 5;
while x # 0 do
  x := x - 1
end

s2:

x := 5;
while x # 10 do
  x := x + 1 
end

Each of them terminates as can be veryfied considering the variants x and 10 - x respectively. However, there is a derivation sequence where the two statements alternately increment and decrement x, meaning none of them will ever reach the state where the condition is false.

Hoare Logic

Changes to the formula are marked in bold.

</math> \begin{split} &\qquad\{2 \leq 2\land x > 1\land\forall q.(2\leq q<x)\Rightarrow \lnot(\exists q'.qq' = x)\land 0=0\}\\ &\vDash\\ &\qquad\{2 \leq 2\land \bold{2 \leq x}\land\forall q.(2\leq q<x)\Rightarrow \lnot(\exists q'.qq' = x)\land 0=0\}\\ &\qquad\qquad\text{y := 2;}\\ &\qquad\{\bold{2 \leq y\land y \leq x}\land\forall q.(2\leq q<x)\Rightarrow \lnot(\exists q'.qq' = x)\land 0=0\}\\ &\qquad\qquad\text{z := 0;}\\ &\qquad\{2 \leq y\land y \leq x\land\forall q.(2\leq q<x)\Rightarrow \lnot(\exists q'.qq' = x)\land \bold{z=0}\}\\ &\qquad\qquad\text{while (y < x and z = 0) do}\\ &\qquad\{\bold{y < x}\land 2 \leq y\land y \leq x\land\forall q.(2\leq q<x)\Rightarrow \lnot(\exists q'.qq' = x)\land z=0\}\\ &\qquad\qquad\qquad\text{if (x = y * (x/y) then}\\ &\qquad\{y < x\land 2 \leq y\land y \leq x\land\forall q.(2\leq q<x)\Rightarrow \lnot(\exists q'.qq' = x)\land z=0\land \bold{(x = y \cdot (x\div y)}\}\qquad\text{(Note the contradictional postcondition, so we can state anything here)}\\ &\qquad\qquad\qquad\qquad\text{z := 1}\\ &\qquad\{y < x\land 2 \leq y\land y \leq x\land\forall q.(2\leq q<x)\Rightarrow \lnot(\exists q'.qq' = x)\land z=0\land (x = y \cdot (x\div y)\}\\ &\vDash\\ &\qquad\{2 \leq y\land y \leq x\land\forall q.(2\leq q<x)\Rightarrow \lnot(\exists q'.qq' = x)\land z=0\}\\ &\qquad\qquad\qquad\text{else}\\ &\qquad\{y < x\land 2 \leq y\land y \leq x\land\forall q.(2\leq q<x)\Rightarrow \lnot(\exists q'.qq' = x)\land z=0\land \bold{(x \neq y \cdot (x\div y)}\}\\ &\vDash\\ &\qquad\{2 \leq y\land \bold{y+1 \leq x}\land \forall q.(2\leq q<x)\Rightarrow \lnot(\exists q'.qq' = x)\land z=0\}\\ &\qquad\qquad\qquad\qquad\text{y := y + 1}\\ &\qquad\{2 \leq y\land \bold{y \leq x}\land \forall q.(2\leq q<x)\Rightarrow \lnot(\exists q'.qq' = x)\land z=0\}\\ &\qquad\qquad\qquad\text{end}\\ &\qquad\{2 \leq y\land y \leq x\land \forall q.(2\leq q<x)\Rightarrow \lnot(\exists q'.qq' = x)\land z=0\}\\ &\qquad\qquad\text{end}\\ &\qquad\{2 \leq y\land y \leq x\land \forall q.(2\leq q<x)\Rightarrow \lnot(\exists q'.qq' = x)\land z=0\}\\ &\vDash\\ &\qquad\{z=0\}\\ \end{split} </math>

Linear Temporal Logic

a)

</math> t = (\{p, q\})^\omega\\ t' = (\{\})^\omega </math>

b)

is not a safety property because we cannot check for a finite prefix that satisfies the condition that it is always the case that eventually p will hold. This is easy to see when having a prefix that does not contain p. We can always construct an infinite trace that is appended to that prefix that satisfies the property by simply appending the chain where p always holds. Therefore the property cannot be violated in finite time.

is a safety property because any trace that does not satisfy it, has a finite prefix where at some point only p holds. Independent from how the trace continues it is not contained in the property.