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

Aus VISki
Wechseln zu: Navigation, Suche
(fixed formatting und Erklärung 1b) ausführlicher)
(Assignment 4: JSON in Haskell)
Zeile 158: Zeile 158:
<syntaxhighlight lang="Haskell">
<syntaxhighlight lang="Haskell">
values = foldJson fval fobj
values = foldJson fval fobj
     where fval a    = ("", a)
     where fval a    = [("", a)]
           fobj ls    = [ (cat k path,value) | (k,tuples) <- ls , (path,value) <- tuples ]
           fobj ls    = [ (cat k path,value) | (k,tuples) <- ls , (path,value) <- tuples ]
           cat k ""  = k
           cat k ""  = k

Aktuelle Version vom 15. August 2019, 13:07 Uhr

Assignment 1: Typing


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

2. (a -> b) -> a -> b



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




t1 = t2 -> t3

t2 = (t4, t3)

t6 -> t7 = t0

t7 = Bool

t1 = t6 -> Int


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


Assignment 3: Lists in Haskell


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


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


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


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,
 ) where ...

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

module Json (
  Json (Val),
) where

-- rest of code here with no indent


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


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


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


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


Because ,



Use as loop invariant and x<1?0:1 as loop variant

while x > 0 do



Assignment 6


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 .

Step cases:

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

Last used rule is If: Thus we have two subtrees and . By using the hypothesis twice and using , we get the needed result of .

Last used rule is Seq: Thus we have two subtrees and . By using the induction hypothesis twice, we get .




while x=0 do skip end

Assignment 7

We prove this in two steps.

Lemma 4:


Lemma 5:

Proof by induction on n:

Base case n=0:

(using Lemma 1)

Step case:

Using the IH, we get using Lemma 2 and the fact that .

Now we can combine Lemmas 4 and 5:

Assignment 8


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 is violated. In order for the negation to be valid, the formula must be violated for any execution. Therefore this formula is not valid, a counterexample being s1, s2, s1, s2, ... which fulfills "".

Please see the discussion page before modifying this answer.

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


If A is a liveness property, every finite prefix t can be extended to an infinite trace . Because , . Thus is also a liveness property.

c) Every prefix can be extended with an occurence of , 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.

It can't be a safety property too, because the definitions of liveness and safety properties directly contradict. (The only property which is both a safety and liveness property is "true".)

Please see the discussion page before modifying this answer.