Lösungsvorschlag Formal Methods And Functional Programming FS13

Aus VISki
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]
 shuffleAdjacent (x:y:xs) = y:x:(shuffleAdjacent xs)

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)

. 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)FMFPFS13Automaton.png

The property is satisfied because there are no accepting states. That would be which is not reachable and thus not drawn.