# 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) -> ${\displaystyle [[}$a${\displaystyle ]]}$ -> ${\displaystyle [[}$b${\displaystyle ]]}$

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:

t1 = (t4, t3)  -> t3
= t2        -> Int
= (t4, Int) -> Int
= t6        -> Int

t2 = t6 = (t4, Int)

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


(Sollte das nicht bloss (a -> Bool) sein, da kein Constraint sagt, dass t2 = t6? Die Variablen heissen zwar gleich, aber müssen nicht gleich sein, da Lambdaexpression.

Antwort (Dimitri): Nein, die Antwort (a, Int) -> Bool ist laut ghci richtig

Antwort 2 (Lukas): Argumentation nach Lösungsprogramm ist irrelevant, habe die relevanten Formeln hinzugefügt.

## Assignment 2: Proofs about funct. programs

Let P(xs) be: for all ys. length (aux ys xs) = (length ys) + 2*(length xs).

First we prove: for all xs. P(xs) by strong structural indoction over xs.

Let ys be arbitrary.

IH: for all proper sublists xs' of xs. P(xs') holds.

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) for some 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 ...


Note (voinovp): This module syntax didn't work for me. I used:

module Json (
Json (Val),
makeObj,
) where

-- rest of code here with no indent


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 "."


Alternative:

values = foldJson fval fobj
where fval a     = [("", a)]
fobj ls    = [ (cat k path,value) | (k,tuples) <- ls , (path,value) <- tuples ]
cat k ""   = k
cat k path = k ++ "." ++ path


(bfiedler) Why the fuck did they let us write such a non-canonical function? I have not the slightest idea how to do it without the workaround for ".":

values = f . aux ""
aux p (Val a) = [(p, a)]
aux p (Obj b) = concatMap (\(s, o) -> aux (p ++ "." ++ s) o) b
f = map (\(s, o) -> (dropWhile (=='.') s, o))


## Assignment 5

a)

${\displaystyle \{\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 ${\displaystyle \sigma (x)=1}$, ${\displaystyle \sigma =\sigma [x\rightarrow 1]}$

b)

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

c)

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

${\displaystyle \{x\neq 1\}}$
while x > 0 do
${\displaystyle \{x>0\wedge x\neq 1\wedge x<1?0:1=Z\}}$
${\displaystyle \models }$
${\displaystyle \{3-2*x\neq 1\wedge (3-2*x)<1?0:1=0\wedge Z=1\}}$
x:=3-2*x
${\displaystyle \{x\neq 1\wedge x<1?0:1=0\wedge Z=1\}}$
${\displaystyle \models }$
${\displaystyle \{x\neq 1\wedge x<1?0:1
end
${\displaystyle \{\Downarrow \neg (x>0)\wedge x\neq 1\}}$
${\displaystyle \models }$
${\displaystyle \{\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 ${\displaystyle 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 ${\displaystyle P'\models Q'}$. Because of the rule, we also know ${\displaystyle P\models P'}$ and ${\displaystyle Q'\models Q}$. Thus, ${\displaystyle P\models Q}$

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

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

Q.E.D.

b)

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

c)

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

## Assignment 7

We prove this in two steps.

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

Proof: ${\displaystyle \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: ${\displaystyle \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:

${\displaystyle \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 ${\displaystyle \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 ${\displaystyle \sigma [y\rightarrow \sigma (y)+n-1](y)=\sigma (y)+n-1}$.

Now we can combine Lemmas 4 and 5:

${\displaystyle \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. Original answer: Valid, since there is a sequence: Loop s1, s3, s1... for which "always (q or next q)" does not hold and therefore the negation is true

Comment: It is not enough to find one execution where ${\displaystyle \square (q\vee \circ q)}$ is violated. In order for the negation ${\displaystyle \neg \square (q\vee \circ q)}$ to be valid, the formula ${\displaystyle \square (q\vee \circ q)}$ must be violated for any execution. Therefore this formula is not valid, a counterexample being s1, s2, s1, s2, ... which fulfills "${\displaystyle \square (q\vee \circ q)}$".

If A is a liveness property, every finite prefix t can be extended to an infinite trace ${\displaystyle t'\in A}$. Because ${\displaystyle A\implies A\vee A'}$, ${\displaystyle t'\in A\vee A'}$. Thus ${\displaystyle A\vee A'}$ is also a liveness property.
c) Every prefix can be extended with an occurence of ${\displaystyle \neg q,\neg q}$, making it valid for the property (the left hand side of the implication won't hold anymore making the property true trivially). Thus, it describes a liveness property.