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

Aus VISki
Wechseln zu: Navigation, Suche
(Änderung 14470 von Simhuber (Diskussion) rückgängig gemacht.)
(Assignment 8: Reverted changes 14473-14475 by Florianalexandermoser. Added comment.)
 
Zeile 235: Zeile 235:
  
 
c)
 
c)
 +
Every prefix can be extended with an occurence of <math>\neg q, \neg q</math>, 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.
  
This is a safety property. Proof: Let <math>t</math> be a trace which violates <math>p</math>, let <math>t2</math> be the trace from <math>t[0]</math> till at which point the violation occurs (so a finite prefix). Let <math>t3</math> be any trace. The trace <math>t2t3</math> will not fulfil <math>p</math>. Therefore <math>p</math> is a safety property. As it is a safety property and it is not the property <math>true</math> it cannot be a liveness property too.
 
 
 
''Original Answer:'' Every trace can be extended with an occurence of <math>\neg q, \neg q</math>, 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. (The only property which is both a safety and liveness property is "true".)
 
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".)
  
''Comment to Original Answer:'' The argument is flawed because you prove liveness properties by appending a fulfilling trace t to any trace t'; the resulting trace tt' will then fulfil p. In the original answer the fulfilling trace is prepended which doesn't make much sense. I will apply this reasoning to a real liveness property and show that it cannot hold: <>[]p is a liveness property (from assignments). By the reasoning from the original answer we would not be able to prove this: Let trace t be "pq" (and q implies not p). There is no t' which would allow t't to hold.
+
Please see [[Diskussion:Lösungsvorschlag_Formal_Methods_And_Functional_Programming_FS16|the discussion page]] before modifying this answer.

Aktuelle Version vom 17. August 2017, 11:58 Uhr

Assignment 1: Typing

a)

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

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

Reasoning:

1a.jpg

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)

Prooftree

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

(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)

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

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

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. 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 $ \square(q \vee \circ q) $ is violated. In order for the negation $ \neg\square(q \vee \circ q) $ to be valid, the formula $ \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 "$ \square(q \vee \circ q) $".

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

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