# Lösungsvorschlag Formal Methods And Functional Programming FS13

Wechseln zu: Navigation, Suche
ToDo:
Part II
Alle momentan zu editierenden Einträge werden hier gesammelt.

# Part I

## Aufgabe 1

### (a)

1. `:: (a->Bool->b)->a->b`
2. `:: a->(a->a)->(a->Bool)->a`
3. `:: Num a1 => (a1 -> a -> Bool) -> [a] -> [a]`

### (b)

1. `\x y -> x y y`
2. `\x y -> x (head y)` oder ` \f xs -> head (map f xs) `
• `\x y -> if (head (takeWhile x y) == head y) then [1] else [0]`
• or ` \f xs -> if f (head xs) then (\_ -> [1]) ([head xs == head xs]) else [2] `
• or, maybe slightly easier: `\x y -> if x (head y) && (head y)==(head y) then [1] else [2]`
• or `\x y -> ( filter (\z -> x z && (z==z)) y >> return 3 )`
• or with map `\x y -> map (\l -> if l==l && x l then 1 else 0) y`

## Aufgabe 2

### (a)

```                                            ---------------- Ax
Gamma,A |- Gamma
---------------- Ax    ------------- Ax    ---------------- and ER
Gamma |- Gamma          Gamma,A |- A         Gamma,A |- ¬A
---------------- and EL ----------------------------------- ¬E  --------------- Ax
Gamma |- A or B              Gamma, A |- B                       Gamma, B |- B
------------------------------------------------------------------------------- or E
(A or B) and ¬A |- B
------------------------------------------------------------------------------- -> I
|- (A or B) and ¬A -> B

Gamma = (A or B) and ¬A
```

### (b)

``` Gamma |- P(Leaf t)    Gamma, P(sub) |- P(List s sub)    Gamma, P(l), P(r) |- P(Node l r)
----------------------------------------------------------------------------------------- **
Gamma |- forall x element of Tree a b P(x)

**t,sub,s,l,r not free in Gamma or P.

(t el a; s el [b]; l, r, sub el Tree a b)
```

## Aufgabe 3

Proof by Induction over n

• let xs be arbitrary
• Base case: n=0
``` `(take 0 xs)++(drop 0 xs) `
`= [] ++ (drop 0 xs) `     (take.2)
`= drop 0 xs `             (app.1)
`= xs `                    (drop.2)
```
• Step case: Suppose the equality holds for any arbitrary "n"; let's prove that it also holds for (n+1)
• Do case destinction on whether xs = [] or xs = (y:ys) for arbitrary y,ys
• Case 1: xs = []
``` `(take (n+1) []) ++ (drop (n+1) [])`
`= [] ++ (drop (n+1) xs)`              (take.1)
`= [] ++ []`                           (drop.1)
`= [] = xs`                            (app.1)
```
• Case 2: xs = (y:ys)
``` `(take (n+1) (y:ys))++(drop (n+1) (y:ys))`
`= (y:(take n ys))++(drop (n+1) (y:ys))`       (take.3)
`= (y:(take n ys))++(drop n ys)`               (drop.3)
`= y:((take n ys)++(drop n ys))`               (app.2)
`= y:ys = xs`                                  (Induction Hypothesis)
```

q.e.d.

## Aufgabe 4

### (a)

["moo","foo","goo"]

### (b)

``` filterSeq :: (a->Bool) -> Seq a -> Seq a
filterSeq f seq = foldSeq Empty check Concat seq
where
check a
| f a = Single a
| otherwise = Empty
```

I don't think that works, GHCi throws an illegal type signature error. (It might be valid. See Discussion) Here is an alternative solution:

```filterSeq f = foldSeq Empty (\s -> if f s then Single s else Empty) (\a b -> Concat a b)
```

The way I understood the assignment was that we only return Seq elements if they satisfy the condition. And the Empty element in my opinion doesn't satisfy it. Also in the above solution all elements that don't satisfy the condition are changed to the Empty element. So if there were 5 elements that don't satisfy the condition the above would return 5 Empty elements.

```filterSeq f = foldSeq Empty (\s -> if f s then Single s else Empty) fconcat
where fconcat Empty Empty = Empty
fconcat s     Empty = s
fconcat Empty s     = s
fconcat s1    s2    = Concat s1 s2
```

### (c)

``` toSeq :: [a] -> Seq a
toSeq [] = Empty
toSeq [x] = Single x
toSeq xs = Concat (toSeq xl) (toSeq xr)
where
n = div (length xs) 2
xl = take n xs
xr = drop n xs
```

## Aufgabe 5

### (a)

``` shuffleAdjacent :: [a] -> [a]
shuffleAdjacent [] = []
shuffleAdjacent [x] = [x]
```

alternative version if you really dislike simple solutions. This is only to show that it is possible to do with foldr and zip if you were wondering:

``` shuffleAdjacent :: [a] -> [a]
shuffleAdjacent [] = []
shuffleAdjacent [x] = [x]
shuffleAdjacent l = foldr (\(x,y) e -> x:y:e) [] \$ zip (evens l) (odds l)
where
evens l = [l!!(x-1) | x <- [2..], mod x 2 == 0]
odds l = [l!!(x-1)  | x <- [1..], odd x]
```

### (b)

``` goldbach :: Int -> Bool
goldbach x
| x <= 2 = False
| otherwise = [(a,b)| a<-(primesUntil x), b<-(primesUntil x), a+b==x]/=[]
where
primesUntil :: Int -> [Int]
primesUntil x = 2:[a| a<-[3,5..x], prime a]
prime :: Int -> Bool
prime x = [a| a<-[3,5..x], mod x a == 0]==[x]
```
``` goldbach :: Int -> Bool
goldbach n = or [prime(n-x) | x <- [2..n-2], prime x]
where
prime k = not (or [k 'mod' i == 0 | i <- [2..k-1]])
```

### (c)

``` cartesian :: [[a]] -> [[a]]
cartesian [] = []
cartesian [x] = []
cartesian (x:y:xs) = aux (fcart x y y) xs
where
aux :: [[a]] -> [[a]] -> [[a]]
aux x [] = x
aux x (y:ys) = aux (cart x y y) ys

cart :: [[a]] -> [a] -> [a] -> [[a]]
cart [] _ _ = []
cart (x:xs) ys [] = cart xs ys ys
cart (x:xs) ys (z:zs) = (x++[z]):cart (x:xs) ys zs

fcart :: [a] -> [a] -> [a] -> [[a]]
fcart [] _ _ = []
fcart (x:xs) ys [] = fcart xs ys ys
fcart (x:xs) ys (z:zs) = [x,z]:fcart (x:xs) ys zs
```
``` cartesian :: [[a]] -> [[a]]
cartesian [] = []
cartesian xs = gen xs
where
gen [] = [[]]
gen (x:xs) = [y : ys | y <- x, ys <- gen xs]
```
```  cartesian :: [[a]] -> [[a]]
cartesian [] = []
cartesian [x] = [x]
cartesian (x:y:xs) = aux [[b,a] | a <- x, b <- y] xs
where
aux :: [[a]] -> [[a]] -> [[a]]
aux xs [] = map (reverse) xs
aux xs (z:zs) = aux [y:x | x <- xs, y <- z] zs
```

```  -- Using the hint
cartesian :: [[a]] -> [[a]]
cartesian [] = [[]]
cartesian (x:xs) = concat \$ map (\zs -> [z:zs | z <- x]) \$ cartesian xs
```
``` In one line:
cartesian :: [[a]] -> [[a]]
cartesian a = foldr (\xs ys -> [x:y | x <- xs, y <- ys]) [[]] a
```
```  -- The power of Monads:
cartesian :: [[a]] -> [[a]]
cartesian = sequence
```

# Part II

## Aufgabe 6

Abbreviations:

• w:
``` y := y - 1;
if x < y then
x := x + 1;
else
skip
end
```
• i:
``` if x < y then
x := x + 1;
else
skip
end
```

Derivation Sequence:

1. 〈s, [x=0,y=2]〉→₁ --WHILE
2. 〈if x<y then w; s else skip end,[x=0,y=2]〉→₁ --IFT
3. 〈(y:=y-1;i); s,[x=0,y=2]〉→₁ --SEQ1
4. 〈i;s,[x=0,y=1]〉→₁ --IFT
5. 〈x:=x+1; s,[x=0,y=1]〉→₁ --SEQ1
6. 〈s,[x=1,y=1]〉→₁ --WHILE
7. 〈if x < y then w; s else skip end,[x=1,y=1]〉→₁ --IFF
8. 〈skip,[x=1,y=1]〉→₁ --SKIP
9. [x=1,y=1]

## Aufgabe 7

P(T) = forall b,s,sig,sig' root(T) = <while b do s end, sig> -> sig' => B[b]sig' = ff

Prove by structural induction over the shape of the derivation tree T.

Assume the left side; root(T) = <while b do s end, sig> -> sig'

Need to show that B[b]sig' = ff holds.

let b,s,sig,sig' be arbitrary.

Do a case destinction on the last rule applied. There are only two candidates; WhT and WhF

Case 1: WhT

```                         \                 T1                /
\                                 /
<s,sig> -> sig"     <while b do s end, sig"> -> sig'
------------------------------------------------------ WhT B[b]sig = tt
<while b do s end, sig> -> sig'
```

We learn from the side condition that B[b]sig = tt.

Because T1 is a proper sub tree of T we may assume P(T1) holds;

P(T1) = <while b do s end, sig"> -> sig' => B[b]sig' = ff

Which is what we need. Therefore B[b]sig' = ff holds.

Case 2: WhF

```       ------------------------------------------------------ WhF B[b]sig = ff
<while b do s end, sig> -> sig
```

We learn from the side condition that B[b]sig = ff.

From the shape of the last rule we also learn that sig = sig'.

Therefore B[b]sig = B[b]sig' = ff which is what we need to show.

## Aufgabe 8

### (a)

invariant:

N>0 && k <= N && n=N && fib(k) = res && fib(k-1) = aux

variant:

n - k

### (b)

``` {o_n > 0 && o_res = fib(o_n) && o_aux = fib(o_n - 1) && n=N && N > 0}

if n >= o_n then

{n >= o_n && o_n > 0 && o_res = fib(o_n) && o_aux = fib(o_n-1) && n=N && N > 0}

|=

{N>0 && o_n <= N && n=N && fib(o_n) = o_res && fib(o_n-1) = o_aux}

k:= o_n;

{N>0 && k <= N && n=N && fib(k) = o_res && fib(k-1) = o_aux}

res := o_res;

{N>0 && k <= N && n=N && fib(k) = res && fib(k-1) = o_aux}

aux := o_aux;

{N>0 && k <= N && n=N && fib(k) = res && fib(k-1) = aux}

else

{!(n >= o_n) && o_n > 0 && o_res = fib(o_n) && o_aux = fib(o_n - 1) && n=N && N > 0}

|= (def. fib)

{N>0 && 1 <= N && n=N && fib(1) = 1 && fib(1-1) = 1}

k := 1;

{N>0 && k <= N && n=N && fib(k) = 1 && fib(k-1) = 1}

res := 1;

{N>0 && k <= N && n=N && fib(k) = res && fib(k-1) = 1}

aux := 1;

{N>0 && k <= N && n=N && fib(k) = res && fib(k-1) = aux}

end

{N>0 && k <= N && n=N && fib(k) = res && fib(k-1) = aux}

while k<n do

{k<n && N>0 && k <= N && n=N && fib(k) = res && fib(k-1) = aux && n-k = Z} (side condition 0 <= n-k holds)

|=      fib(n) = fib(n-1) + fib(n-2)

{N>0 && k+1 <= N && n=N && fib(k+1) = res + aux && fib(k+1-1) = res + aux - aux && n-(k+1) < Z}

res := res + aux;

{N>0 && k+1 <= N && n=N && fib(k+1) = res && fib(k+1-1) = res - aux && n-(k+1) < Z}

aux := res - aux;

{N>0 && k+1 <= N && n=N && fib(k+1) = res && fib(k+1-1) = aux && n-(k+1) < Z}

k:= k+1;

{N>0 && k <= N && n=N && fib(k) = res && fib(k-1) = aux && n-k < Z}

end

{!(k<n) && N>0 && k <= N && n=N && fib(k) = res && fib(k-1) = aux}

|=      (!(k<n) && k<=N && n=N) => k=N)

{res = fib(N)}
```

## Aufgabe 9

### (i)

P(T) = all P,Q,b,s1,s2.root(T) = {P} if b then s1 else s2 end {Q} => (exists T1.root(T1) = {P && b} s1 {Q}) && (exists T2.root(T2) = {P && !b} s2 {Q}

Proof by induction over the shape of the derivation tree T. Assume P(T') for all T' < T.

• let P, Q, b, s1, s2 be arbitrary.
• assume the left side.
• need to show (exists T1.root(T1) = {P && b} s1 {Q}) && (exists T2.root(T2) = {P && !b} s2 {Q}
• Case destinction on the last rule applied.

Case 1: Cons

```      \                T'                  /
\                                  /
{P'} if b then s1 else s2 end {Q'}
------------------------------------
{P} if b then s1 else s2 end {Q}
```
• we know from the side condition that P |= P' and Q' |= Q
• Because T' < T we may assume P(T'). Therefore we have T1.root(T1) = {P' && b} s1 {Q'} and T2.root(T2) = {P' && !b} s2 {Q'} for some T1 and T2.
• And we are done because we know that P |= P' and Q' |= Q holds and therefore {P && b} s1 {Q}) holds for T1 and {P && !b} s2 {Q} holds for T2.

Case 2: If

```       \     T2      /   \     T1       /
{b && P} s1 {Q}   {!b && P} s2 {Q}
------------------------------------
{P} if b then s1 else s2 end {Q}
```
• from the rule we get directly two trees of the desired form; T1 and T2.
• Might have to note that {b && P} |= {P && b} and {!b && P} |= {P && !b}

### (ii)

P(T1,T2) = all P,Q,b,s1,s2 (root(T1) = {P && b} s1 {Q}) && (root(T2) = {P && !b} s2 {Q} => exists T.root(T) = {P} if b then s1 else s2 end {Q}

• let P, Q, b, s1, s2 be arbitrary.
• assume (root(T1) = {P && b} s1 {Q}) && (root(T2) = {P && !b} s2 {Q}
• need to show exists T.root(T) = {P} if b then s1 else s2 end {Q}

This follows directly from the If rule. If we have two trees like the above we can construct the following tree T in the desired form;

```       \     T2      /   \     T1       /
{b && P} s1 {Q}   {!b && P} s2 {Q}
------------------------------------
{P} if b then s1 else s2 end {Q}
```

## Aufgabe 10

Promela code:

```int x;

proctype p1(){
x=1;
}

proctype p2(){
x=2;
x=x+2;
}

init{
x=2;
run p1();
run p2();
_nr_pr == 1; //wait until there is only one process left
do
:: skip;
od
}
```

b)

${\displaystyle \lozenge \square (p_{1}\lor p_{3}\lor p_{4})}$. This is satisfied by the Promela code, because the value of x will be either 1, 3 or 4. But the automaton given allows to leave the states {p4} and {p1} again. This is a liveness property, because for every prefix of a trace that is not in the property, we can find an infinite continuation which is inside the property, namely going to state {p3} and staying there.

c)

The property is satisfied because there are no accepting states. That would be ${\displaystyle Cp_{3}}$ which is not reachable and thus not drawn.