# Lösungsvorschlag Formal Methods And Functional Programming FS16: Unterschied zwischen den Versionen

## Assignment 1: Typing

a)

1. (a -> b) -> ((a -> b) -> c) -> a -> (c, b)

2. (a -> b) -> $[[$a$]]$ -> $[[$b$]]$

Reasoning:

3. Not typable, x would need to be of the form [a] as well as of the form [a] -> c

4. Num a => a -> a

b)

Constraints:

t1 = t2 -> t3

t2 = (t4, t3)

t6 -> t7 = t0

t7 = Bool

t1 = t6 -> Int

Conclusion: t0 = t6 -> Bool = t2 -> Bool = (t4, t3) -> Bool = (t4, Int) -> Bool

## Assignment 2: Proofs about funct. programs

First prove length (aux ys xs) = (length ys) + 2*(length xs)

Induction on xs (for arbitrary ys)

Base case: xs = []

length (aux ys []) = length ys = length ys + 2*0 = length ys + 2*(length [])

Step case: xs = (a:as)

length (aux ys (a:as)) = length (aux (a:a:ys) as) =IH= (length (a:a:ys)) + 2*(length as) = 1 + (length (a:ys)) + 2*(length as) = length ys + 2 * (1 + length as) = length ys + 2 * (length (a:as))

Using this, we can prove the equality:

length (revdup xs) = length (aux [] xs) = length [] + 2*(length xs) = 0 + 2*(length xs) = 2 * length xs

q.e.d.

## Assignment 3: Lists in Haskell

a)

pairSum xs n = [(a,b) | a <- xs, b <- xs, (a+b == n)]

b)

interlace l1 l2 = helper l1 l2 False
where  helper [] l2 _ = l2
helper l1 [] _ = l1
helper (a:l1) l2 False = a:(helper l1 l2 True)
helper l1 (b:l2) True = b:(helper l1 l2 False)

Alternative solution:

interlace [] ys = ys
interlace xs [] = xs
interlace (x:xs) (y:ys) = x:y:interlace xs ys

c)

open = [n | n <- [1,2..], test n]
where test n = length [b | b <- [1..n], n mod b == 0] mod 2 == 1

Alternative solution:

open = [n*n | n <- [1,2..]]

## Assignment 4: JSON in Haskell

a)

Write a smart constructor that checks the invariant on creation and throws an error if it is violated. Then, hide the "dumb" constructor by not exporting it out of the module like

module JSON (
Json a,
Val a,
constructJson
) where ...

b)

foldJson :: (a -> b) -> ([(String, b)] -> b) -> Json a -> b
foldJson foldVal foldObj json = go json
where go (Val a) = foldVal a
go (Obj vals) = foldObj $map (\(s, js) -> (s, go js)) vals c) instance Eq a => Eq (Json a) where (==) (Val a) (Val b) = a == b (==) (Obj l1) (Obj l2) = all (\e -> e elem l2) l1 && all (\e -> e elem l1) l2 (==) _ _ = False d) values :: Json a -> [(String, a)] values = foldJson (\a -> [("", a)]) foldObj where foldObj l = concat$ map go l
go (s, b) = map (\(name, a) -> (s ++ (separator name) ++ name, a)) b
separator name = if name == [] then "" else "."

## Assignment 5

a)

$\langle s, \sigma\rangle\rightarrow_1\langle if\: x>0\: then\: x:=3-2*x;\: s\: else\: skip\: end, \sigma\rangle\rightarrow_1\langle x:=3-2*x;s\: ,\sigma\rangle\rightarrow_1\langle s,\sigma [x\rightarrow 1]\rangle$

Because $\sigma(x) = 1$, $\sigma = \sigma [x\rightarrow 1]$

b)

$\{x\neq 1\} s \{\Downarrow true\}$

c)

Use $\{x\neq 1\}$ as loop invariant and x<1?0:1 as loop variant

$\{x\neq 1\}$
while x > 0 do
$\{x>0\wedge x\neq 1\wedge x<1?0:1 = Z\}$
$\models$
$\{3-2*x\neq 1\wedge (3-2*x)<1?0:1=0\wedge Z=1\}$
x:=3-2*x
$\{x\neq 1\wedge x<1?0:1=0\wedge Z=1\}$
$\models$
$\{x\neq 1\wedge x<1?0:1 < Z\}$
end
$\{\Downarrow\neg(x>0)\wedge x\neq 1\}$
$\models$
$\{\Downarrow true\}$


## Assignment 6

a)

We prove this by induction on the shape of the axiomatic semantics derivation tree.

The predicate is P(T) = root(T) = {P} s {Q} and s contains no ass. or while) => P entails Q

Base case: Last used rule is skip. By definition of the rule, we get P = Q, thus also $P\models Q$.

Step cases:

Last used rule is Cons: Thus we have a subtree proving {P'} s {Q'}, thanks to the IH we get $P'\models Q'$. Because of the rule, we also know $P\models P'$ and $Q'\models Q$. Thus, $P\models Q$

Last used rule is If: Thus we have two subtrees $\{b\wedge P\} s_1\{Q\}$ and $\{\neg b\wedge P\}s_2 \{Q\}$. By using the hypothesis twice and using $P\models (b\wedge P)\vee (\neg b\wedge P)$, we get the needed result of $P\models Q$.

Last used rule is Seq: Thus we have two subtrees $\{P\} s_1\{R\}$ and $\{R\}s_2 \{Q\}$. By using the induction hypothesis twice, we get $P\models Q$.

Q.E.D.

b)

$\{x+1=0\} x:=x+1 \{x=0\}$

c)

$\{true\}$ while x=0 do skip end $\{\neg(x=0)\wedge true\}$

## Assignment 7

We prove this in two steps.

Lemma 4: $\forall\sigma.\sigma(x)=0\Rightarrow\langle s,\sigma\rangle\rightarrow_1^*\langle s,\sigma [x\rightarrow 1]\rangle$

Proof: $\langle s,\sigma\rangle\rightarrow_1^k\langle x:=1;s,\sigma\rangle\rightarrow_1^1\langle s,\sigma [x\rightarrow 1]\rangle$

Lemma 5: $\forall n:Nat,\forall\sigma.\sigma(x)=0\Rightarrow\langle s,\sigma\rangle\rightarrow_1^*\langle s,\sigma [y\rightarrow\sigma(y)+n]\rangle$

Proof by induction on n:

Base case n=0:

$\langle s,\sigma\rangle\rightarrow_1^0\langle s,\sigma\rangle = \langle s, \sigma [y\rightarrow\sigma(y)+0]\rangle$ (using Lemma 1)

Step case:

Using the IH, we get $\langle s,\sigma\rangle\rightarrow_1^*\langle s,\sigma [y\rightarrow\sigma (y)+n-1]\rangle\rightarrow_1^k\langle s,\sigma[y\rightarrow\sigma(y)+n-1][y\rightarrow\sigma[y\rightarrow\sigma(y)+n-1](y)+1]\rangle = \langle s,\sigma[y\rightarrow\sigma(y)+n]\rangle$ using Lemma 2 and the fact that $\sigma[y\rightarrow\sigma(y)+n-1](y)=\sigma(y)+n-1$.

Now we can combine Lemmas 4 and 5:

$\forall n:Nat,\forall\sigma.\sigma(x)=0\Rightarrow\langle s,\sigma\rangle\rightarrow_1^*\langle s,\sigma[y\rightarrow\sigma(y)+n]\rangle\rightarrow_1^*\langle s,\sigma[y\rightarrow\sigma(y)+n][x\rightarrow 1]\rangle$

## Assignment 8

a)

1. Not valid, counterexample: Loop s1, s2, s1...

2. Valid, there is no loop that doesn't go through either q or p

3. Not valid, counterexample: Loop s1, s2, s1...

4. Valid, for the left part to be true, the trace has to loop s1, s2, s1..., which doesn't reach p

b)

If A is a liveness property, every finite prefix t can be extended to an infinite trace $t'\in A$. Because $A\implies A\vee A'$, $t'\in A\vee A'$. Thus $A\vee A'$ is also a liveness property.

c)

Every trace can be extended with an occurence of $\neg q, \neg q$, making it valid for the property (the left hand side of the implication won't hold anymore). Thus, it describes a liveness property.

It can't be a safety property too, because the definitions of liveness and safety properties directly contradict.