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.