# Lösungsvorschlag Formal Methods and Functional Programming FS09

Wechseln zu: Navigation, Suche

# Endterm (June 8th, 2009)

## Assignment 1 (SOS)

Abbreviations:

• [2,0] = ${\displaystyle \sigma [x\mapsto 2,y\mapsto 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 ${\displaystyle B[[x\neq 0]]\sigma [x\mapsto 2,y\mapsto 0]}$ evaluates to true.
3. Sequential composition rule followed by the if-true rule, because ${\displaystyle B[[xmod2=0]]\sigma [x\mapsto 2,y\mapsto 0]}$ evaluates to true.
4. Sequential composition rule followed by the assignment rule, evaluating ${\displaystyle A[[y+x]]\sigma [x\mapsto 2,y\mapsto 0]}$ 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. ${\displaystyle {\cfrac {\cfrac {...}{\langle s,\sigma \rangle \rightarrow \sigma '}}{\langle repeat~s~until~b,\sigma \rangle \rightarrow \sigma }}B[[b]]\sigma '=tt}$

2. ${\displaystyle {\cfrac {{\cfrac {...}{\langle s,\sigma \rangle \rightarrow \gamma }}~~{\cfrac {{\cfrac {{\cfrac {...}{\langle s,\gamma \rangle \rightarrow \gamma '}}~~{\cfrac {...}{\langle while~not~b~do~s~end,\gamma '\rangle \rightarrow \sigma '}}}{\langle s;while~not~b~do~s~end,\gamma \rangle \rightarrow \sigma '}}SeqComp}{\langle repeat~s~until~b,\gamma \rangle \rightarrow \sigma '}}IH}{\langle repeat~s~until~b,\sigma \rangle \rightarrow \sigma '}}B[[b]]\gamma =ff}$

3. ${\displaystyle {\cfrac {{\cfrac {...}{\langle s,\sigma \rangle \rightarrow \sigma '}}~~{\cfrac {}{\langle while~not~b~do~s~end,\sigma '\rangle \rightarrow \sigma '}}B[[\neg b]]\gamma =ff}{\langle s;while~not~b~do~s~end,\sigma \rangle \rightarrow \sigma '}}SeqComp}$

4. ${\displaystyle {\cfrac {{\cfrac {...}{\langle s,\sigma \rangle \rightarrow \gamma }}~~{\cfrac {{\cfrac {...}{\langle s,\gamma \rangle \rightarrow \gamma '}}~~{\cfrac {...}{\langle while~not~b~do~s~end,\gamma '\rangle \rightarrow \sigma '}}}{\langle while~not~b~do~s~end,\gamma \rangle \rightarrow \sigma '}}B[[\neg b]]\gamma =tt}{\langle s;while~not~b~do~s~end,\sigma \rangle \rightarrow \sigma '}}SeqComp}$

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 ${\displaystyle B[[b]]\sigma '=tt}$.

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 ${\displaystyle B[[b]]\gamma '=ff}$

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 ${\displaystyle B[[b]]\sigma '=tt}$.

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 ${\displaystyle B[[b]]\gamma '=ff}$

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 = ${\displaystyle \sum _{j=x+1}^{N}j^{2}}$}

while x > 0 do

{x > 0 ∧ x ≥ 0 ∧ y = ${\displaystyle \sum _{j=x+1}^{N}j^{2}}$}

{x-1 ≥ 0 ∧ y+x*x = ${\displaystyle \sum _{j=x}^{N}j^{2}}$}

y := y + x * x;

{x-1 ≥ 0 ∧ y = ${\displaystyle \sum _{j=x}^{N}j^{2}}$}

x := x - 1

{x ≥ 0 ∧ y = ${\displaystyle \sum _{j=x+1}^{N}j^{2}}$}

{x ≥ 0 ∧ y = ${\displaystyle \sum _{j=x+1}^{N}j^{2}}$}

end

{¬(x > 0) ∧ x ≥ 0 ∧ y = ${\displaystyle \sum _{j=x+1}^{N}j^{2}}$}

{y = ${\displaystyle \sum _{j=1}^{N}j^{2}}$}

x := y

{x = ${\displaystyle \sum _{j=1}^{N}j^{2}}$}

## Assignment 4 (axiomatic semantics)

${\displaystyle {\cfrac {\lbrace P\rbrace s_{1}\lbrace Q\rbrace ~~\lbrace P\rbrace s_{2}\lbrace Q\rbrace }{\lbrace P\rbrace s_{1}[]s_{2}\lbrace Q\rbrace }}}$

## 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:

${\displaystyle {\cfrac {\cfrac {{\cfrac {\lbrace P\rbrace s\lbrace P\rbrace }{\lbrace B[[b]]\land P\rbrace s\lbrace \lbrace P\rbrace }}if\lbrace B[[b]]\land P\rbrace \Rightarrow \lbrace P\rbrace and\lbrace P\rbrace \Rightarrow P\rbrace }{\lbrace P\rbrace while~b~do~s~end\lbrace \neg B[[b]]\land P\rbrace }}{\lbrace P\rbrace while~b~do~s~end\lbrace P\land \neg B[[b]]\rbrace }}if\lbrace P\rbrace \Rightarrow \lbrace P\rbrace and\lbrace P\land \neg B[[b]]\rbrace \Rightarrow \lbrace \neg B[[b]]\land P\rbrace }$

## 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)

${\displaystyle \square {\Big (}(ped\_red\wedge \neg ped\_green)\vee (\neg ped\_red\wedge ped\_green){\Big )}}$

### b)

${\displaystyle \square (signal\rightarrow \lozenge ped\_green)}$

### c)

${\displaystyle \square {\Big (}(\bigcirc ped\_green\rightarrow traf\_red)\wedge (ped\_green\rightarrow \bigcirc traf\_red){\Big )}}$

# Repetition Exam (September 12th, 2009)

Alternative Solution: Lösungsvorschlag FS 2009

## Typing

### a)

1. ${\displaystyle a\rightarrow b\rightarrow (b\rightarrow a\rightarrow c)\rightarrow c}$
2. ${\displaystyle Num\ a\Rightarrow (a\rightarrow b)\rightarrow (c\rightarrow c,b)}$
3. ${\displaystyle Ord\ a\Rightarrow [Bool\rightarrow a]\rightarrow a\rightarrow Bool}$

### b)

${\displaystyle {\cfrac {{\cfrac {\cfrac {\cfrac {\cfrac {{\cfrac {}{\Gamma \vdash c::a_{4}\rightarrow Int}}~~{\cfrac {}{\Gamma \vdash x::a_{4}}}}{\Gamma \vdash c\ x::Int}}{\Gamma :=c:\sigma ,x:(a,Int)\vdash {\mathbf {\text{iszero}}}(c\ x)::Bool}}{c:\sigma \vdash \lambda x.{\mathbf {\text{iszero}}}(c\ x)::(a,Int)\rightarrow Bool}}{\vdash (\lambda c.(\lambda x.{\mathbf {\text{iszero}}}(c\ x)))::\sigma \rightarrow (a,Int)\rightarrow Bool}}~~{\cfrac {\cfrac {\cfrac {}{x:a_{1}\vdash x::(a_{3},a_{2})}}{x:a_{1}\vdash {\mathbf {\text{snd}}}\ x::a_{2}}}{\vdash \lambda x.{\mathbf {\text{snd}}}\ x::\sigma }}}{\vdash (\lambda c(\lambda x.{\mathbf {\text{iszero}}}(c\ x)))(\lambda x.{\mathbf {\text{snd}}}\ x)::(a,Int)\rightarrow Bool}}}$

Constraints:

• ${\displaystyle \sigma =a_{1}\rightarrow a_{2}}$
• ${\displaystyle a_{1}=(a_{3},a_{2})}$
• ${\displaystyle \sigma =a_{4}\rightarrow Int}$
• ${\displaystyle a_{4}=a_{1}}$
• ${\displaystyle a_{2}=Int}$
• ${\displaystyle a_{4}=(a,Int)}$
• ${\displaystyle a_{3}=a}$

## Induction

Theorem: ${\displaystyle \forall xs,ys::[a].}$ rev (xs ++ rev ys) = ys ++ rev xs

Proof: Let ${\displaystyle P(xs)=\forall ys::[a].rev\ (xs\ +\!\!+\ rev\ ys)=ys\ +\!\!+\ rev\ xs}$. I will show ${\displaystyle \forall xs::[a].P(xs)}$ by strong structural induction. ${\displaystyle \forall xs'\sqsubset xs.P(xs')}$ 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.

$split}“): {\displaystyle \begin{split} &\qquad\{2 \leq 2\land x > 1\land\forall q.(2\leq q

## Linear Temporal Logic

### a)

$\displaystyle t = (\{p, q\})^\omega\\ t' = (\{\})^\omega$

### b)

${\displaystyle t}$ 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.

${\displaystyle t'}$ 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.