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

Aus VISki
Wechseln zu: Navigation, Suche
(Assignment 4: Haskell Intervals)
(Assignment 4: Haskell Intervals)
 
Zeile 196: Zeile 196:
 
  | l2 >= l1 && u2 <= u1 && u2 >= l2 = intersect ((V l2 u2):rest)
 
  | l2 >= l1 && u2 <= u1 && u2 >= l2 = intersect ((V l2 u2):rest)
 
  | otherwise = Nothing
 
  | otherwise = Nothing
 +
</syntaxhighlight>
 +
 +
Straightforwarder alternative:
 +
<syntaxhighlight lang="Haskell">
 +
intersect::Ord a => [Interval a] -> Maybe (Interval a)
 +
intersect [] = Nothing
 +
intersect [a] = Just a
 +
intersect ((V l1 u1):(V l2 u2):rest)
 +
| max l1 l2 <= min u1 u2  = intersect ((V (max l1 l2) (min u1 u2)):rest)
 +
| otherwise                = Nothing
 
</syntaxhighlight>
 
</syntaxhighlight>
  

Aktuelle Version vom 13. August 2017, 15:28 Uhr

Assignment 1: Typing

a)

  • i. a -> (a -> b) -> b
  • ii. (Num a, Ord a) => a -> ([b] -> a -> a) -> Bool

b)

  • i. \(x, y) f -> (f x, y)
  • ii. \f x -> if x > x then (f [x,x])+1 else (f [x,x,x])+2

(or \f x -> (f [x]) + (\_ -> 1) (x < x) )

c) Let $ \Gamma :\equiv x : \tau_1 $

                        _____________________Var  _____________Int
                        $ \Gamma\vdash $ x :: $ \tau_5 \to (\tau_4, \tau_3) $       $ \Gamma\vdash $ 0 :: $ \tau_5 $
                       __________________________________________App
                                 $ \Gamma\vdash $ (x 0) :: $ (\tau_4, \tau_3) $
__________________Var        __________________________snd
$ \Gamma\vdash $ x :: $ \tau_3 \to \tau_2 $                $ \Gamma\vdash $ snd (x 0) :: $ \tau_3 $          
______________________________________________________App
           $ \Gamma\vdash $ x (snd ( x 0)) :: $ \tau_2 $
______________________________________________________Abs*
           $ \vdash\lambda $ x.x (snd (x 0)) :: $ \tau_0 $

Constraints: $ \tau_0 = \tau_1 \to \tau_2, \tau_1 = \tau_3 \to \tau_2, \tau_1 = \tau_5 \to (\tau_4, \tau_3), \tau_5 $ = Int

Unifying all the constraints, we get $ \tau_0 = ( $Int$ \to (\tau_4, $Int$ )) \to (\tau_4, $Int$ ) $.

Thus the most general type is (Int -> (a, Int)) -> (a, Int).

Assignment 2: Proof by Induction

Let $ P(xs) := \forall f. \forall ys. zipWith (flip~f)~xs~ys = zipWith~f~ys~xs. $ We show $ \forall xs. P(xs) $ by induction.

Base Case: We have to show P([]). Let f and ys be arbitrary.

zipWith (flip f) [] ys =               -- zipWith.2
[] =                                   -- zipWith.2
zipWith f ys []

Step case: Let x and xs be arbitrary. We assume P(xs) and show P(x:xs). Let f and ys be arbitrary. We do a case destinction over ys. Case ys = []

zipWith (flip f) (x:xs) [] =            -- zipWith.2
[] =                                    -- zipWith.2
zipWith f [] (x:xs)

Case ys = (a:as)

zipWith (flip f) (x:xs) (a:as) =              -- zipWith.1
((flip f) x a):(zipWith (flip f) xs as) =     -- flip
(f a x):(zipWith (flip f) xs as) =            -- I.H.
(f a x):(zipWith f as xs) =                   -- zipWith.1
zipWith f (a:as) (x:xs)

This completes the proof.

Assignment 3: Haskell Lists (7 points)

a)

dvdNxt :: [Int] -> [Int]
dvdNxt [] = []
dvdNxt (a:[]) = [a]
dvdNxt (a:b:xs) = if (b `mod` a) == 0 then a:(dvdNxt (b:xs)) else dvdNxt (b:xs)
dvdNxt :: [Int] -> [Int]
dvdNxt (x:xs)
  | xs == []          = [x]
  | ((mod) (head xs) x) == 0 = x:(dvdNxt xs)
  | otherwise         = dvdNxt xs
dvdNxt :: [Int] -> [Int]
dvdNxt a = [a!!i|i<-[0..length a -2], 0==mod (a!!(i+1)) (a!!i)] ++ lastelem a
  where
    lastelem a = if (a==[]) then [] else [last a]

b)

stableDN :: [Int] -> [Int]
stableDN list = stableDNHelper list (dvdNxt list)
  where
  	 stableDNHelper l1 l2
  	   | l1 == l2  = l1
  	   | otherwise = stableDNHelper l2 (dvdNxt l2) -- l2 = (dvdNxt l1)
stableDN :: [Int] -> [Int]
stableDN x
  | x == dvdNxt x     = x
  | otherwise         = stableDN (dvdNxt x)

c)

prepend :: String -> [[String]] -> [String]
prepend p l = prependHelper p (concat l)
  where
  	 prependHelper p [] = []
  	 prependHelper p (x:xs) = (p++x):(prependHelper p xs)

alternatively an easier way (also works on infinite lists thanks to lazy evaluation):

prepend s = map ((++) s) . concat

list comprehension:

prepend p xs = [p++zs | ys <- xs, zs<-ys]

list comprehension extended:

prepend :: String -> [[String]] -> [String]
prepend s (l:ls)      = [s ++ e | e <- l] ++ prepend s ls
prepend s []          = []

foldr:

prepend :: String -> [[String]] -> [String]
prepend s l = foldr (\x y -> (foldr (\x1 y1 -> (s++x1) : y1) [] x) ++ y) [] l

Assignment 4: Haskell Intervals

a)

make a b
  | a > b = make b a
  | otherwise = V a b

b)

instance (Show a) => Show (Interval a) where
  show (V a b) = "[" ++ show a ++ "," ++ show b ++ "]"

c)

intersect :: Ord a => [Interval a] -> Maybe (Interval a)
intersect [] = Nothing
intersect [x] = Just x
intersect xs = foldl1 ov (map (\x -> Just x) xs)
    where
        ov (Just (V a b)) (Just (V c d)) = if legal newI then Just newI else Nothing
            where
                newI = V (max a c) (min b d)
                legal (V x y) = x < y

Alternative:

intersect :: Ord a => [Interval a] -> Maybe (Interval a)
intersect [] = Nothing
intersect [x] = Just x
intersect xs
	| a <= b = Just (V a b)
	| otherwise = Nothing
	where (V a b) = (foldr (\(V a b) (V c d) -> (V (max a c) (min b d))) (head xs) xs)

Straightforward alternative:

intersect::Ord a => [Interval a] -> Maybe (Interval a)
intersect [] = Nothing
intersect [V l u] = Just (V l u)
intersect ((V l1 u1):(V l2 u2):rest)
 | l1 >= l2 && u1 <= u2 && u1 >= l1 = intersect ((V l1 u1):rest)
 | l1 >= l2 && u2 <= u1 && u2 >= l1 = intersect ((V l1 u2):rest)
 | l2 >= l1 && u1 <= u2 && u1 >= l2 = intersect ((V l2 u1):rest)
 | l2 >= l1 && u2 <= u1 && u2 >= l2 = intersect ((V l2 u2):rest)
 | otherwise = Nothing

Straightforwarder alternative:

intersect::Ord a => [Interval a] -> Maybe (Interval a)
intersect [] = Nothing
intersect [a] = Just a
intersect ((V l1 u1):(V l2 u2):rest)
 | max l1 l2 <= min u1 u2   = intersect ((V (max l1 l2) (min u1 u2)):rest)
 | otherwise                = Nothing

Another solution:

intersect :: Ord a => [Interval a] -> Maybe (Interval a)
intersect []  = Nothing
intersect [x] = Just x
intersect xs  = aux (map (\y -> Just y) xs)
 where
  aux (x:y:zs)
   | x == Nothing = Nothing
   | zs == []     = doInter x y
   | otherwise    = aux ((doInter x y):zs)
  doInter (Just a b) (Just c d)
   | (max a c) <= (min b d) = Just (V (max a c) (min b d))
   | otherwise = Nothing

d)

Create a new module with all the interval definitions and functions. Then we can use an export list to export the functions we want to be available to public. To make it impossible to create illegal intervals, we would export the `make` function defined earlier, but not the constructor. As our `make` function automatically fixes attempts to create invalid intervals it's not possible to construct invalid intervals.

Assignment 5: File System Entries

-- (a)
 
fFSE :: (String -> [a] -> a) -> (String -> String -> a) -> FSEntry -> a
fFSE foldFolderFunc foldFileFunc (Folder n entries) = foldFolderFunc n (map (\x -> fFSE foldFolderFunc foldFileFunc x) entries)
fFSE foldFolderFunc foldFileFunc (File n c) = foldFileFunc n c
 
 
-- (b)
 
-- i.
 
number :: FSEntry -> Int
number root = fFSE (\_ y -> (sum y) + 1) (\_ _ -> 1) root
 
-- alternative i. (easier to comprehend imho)
numberME :: FSEntry -> Int
numberME (File _ _) = 1
numberME (Folder _ b) = foldr (\x e -> e + numberME x) 1 b
 
-- ii.
 
count :: Char -> FSEntry -> Int      
count ch root = fFSE (\_ y -> (sum y)) (\_ y -> foldr (\c1 c -> if c1 == ch then c+1 else c) 0 y) root
 
-- alternative ii. with filter
countME c a = fFSE hdir hfile a
  where
    hdir a d = (sum d)
    hfile _ d = length $ filter (c==) d
 
 
-- (c)
 
-- a is [String], a list of files in that FSEntry
-- foldFolderFunc takes a list of lists [[String]], eg [['bla/f1.txt','bla/f2.txt'],['foo/f3.txt','foo/f4.txt']]
-- and 
paths :: FSEntry -> [String]
paths root = fFSE (\name files -> map (\file -> name ++ "/" ++ file) (concat files)) (\name _ -> [name]) root
 
-- alternative using list comprehension instead of map
paths :: FSEntry -> [String]
paths root = fFSE (\name files -> [name ++ "/" ++ f | f <- (concat files)]) (\name _ -> [name]) root
 
--another really easy sololution would be
paths (File n c) = [n]
paths (Folder n e) = prepend (n ++ "/") (map paths e)
 
--using fFSE and prepend
paths = fFSE (\n -> prepend (n ++ "/")) (\n _ -> [n])

Assignment 6

Let $ \sigma[n,m] :\equiv \sigma[x \mapsto n][y \mapsto m] $

FMFP ExFS14 Assignment6.png

Assignment 7

a) Invariant: $ \{ (N = q \times d + r) \wedge (d=D) \wedge (D>0) \wedge (r+d >= 0) \} $ // Variant: $ r = Z $

b) $ \{ N \geq 0 \wedge D > 0 \wedge d=D \wedge r = N \wedge q=0\} $ $ \models\{ (N = q \times d + r) \wedge (d=D) \wedge (D>0) \wedge (r+d >= 0) \}:=P $

while r >= 0 do

$ \{ P \wedge r >= 0 \wedge r=Z \} $ $ \models\{ (N = q \times d + r-d+d) \wedge (d=D) \wedge (D>0) \wedge (r-d+d >= 0) \wedge (r-d+d = Z) \} $

r := r - d;

$ \{ (N = q \times d + r+d) \wedge (d=D) \wedge (D>0) \wedge (r+d >= 0) \wedge (r+d = Z) \} $ $ \models\{\Downarrow (N = (q+1-1) \times d + r+d) \wedge (d=D) \wedge (D>0) \wedge (r+d >= 0) \wedge (r < Z) \} $

q := q + 1;

$ \{\Downarrow (N = (q-1) \times d + r+d) \wedge (d=D) \wedge (D>0) \wedge (r+d >= 0) \wedge (r < Z) \} $ $ \models\{\Downarrow (N = q \times d + r) \wedge (d=D) \wedge (D>0) \wedge (r+d >= 0) \wedge (r < Z) \} $

end

$ \{\Downarrow P \wedge r < 0 \} $ $ \models\{\Downarrow (N = q \times d + r+d-d) \wedge (d=D) \wedge (D>0) \wedge (r+d >= 0) \wedge (r+d-d < 0) \} $

r := r + d;

$ \{\Downarrow (N = q \times d + r-d) \wedge (d=D) \wedge (D>0) \wedge (r >= 0) \wedge (r-d < 0) \} $ $ \models\{\Downarrow (N = (q-1+1) \times d + r-d) \wedge (d=D) \wedge (D>0) \wedge (r >= 0) \wedge (r-d < 0) \} $

q := q - 1;

$ \{\Downarrow( N = (q+1) \times d + r-d ) \wedge (d=D) \wedge (D>0) \wedge (r >= 0) \wedge (r-d < 0) \} $ $ \models\{\Downarrow (N = q \times D + r) \wedge (r \geq 0) \wedge (r < D) \} $

Assignment 8

a)

$ wr(\text{skip}) = \emptyset $

$ wr(x := e) = \{x\} $

$ wr(s_1;s_2) = wr(s_1) \cup wr(s_2) $

$ wr(\text{if }b\text{ then }s_1\text{ else }s_2\text{ end}) = wr(s_1) \cup wr(s_2) $

$ wr(\text{while }b\text{ do }s\text{ end}) = wr(s) $

b)

Open for discussion:

Let s, $ \sigma', \sigma $, x be some arbitrary statement, states and variable for which the left hand side of the lemma holds. We prove the Lemma by induction over the shape of the derivation tree for <s, $ \sigma $> -> $ \sigma' $. We do a case distinction on s:

Base cases:

s = skip: Then $ \sigma' = \sigma $ and therefore $ \sigma' (x) = \sigma (x) $.

s = a := e: Since x is not in wr(s), x ≠ a. Therefore $ \sigma'(x) = \sigma[a -> A[[e]]\sigma (x) = \sigma (x) $

Step cases: Assuming the Lemma holds for any subtree of the derivation tree, prove that it holds for the whole tree.

s = s1; s2: Since x is not in wr(s) = wr(s1) ∪ wr(s2), x is not element of neither wr(s1) nor wr(s2). The last rule applied in the derivation tree for <s, $ \sigma $> -> $ \sigma' $ has to be Seq(NS). Therefore, we know that there is a state $ \sigma'' $ for which <s1, $ \sigma $> -> $ \sigma'' $ and <s2, $ \sigma'' $> -> $ \sigma' $ can be derived. Then we can apply the Lemma for s1 and s2 and we have $ \sigma''(x) = \sigma' (x) = \sigma (x) $.

s = while b do s1 end: If b evaluates to false in $ \sigma $, then we know that the last rule applied in the derivation tree was WhF(NS). Then $ \sigma = \sigma' $ and therefore $ \sigma' (x) = \sigma (x) $.

If b evaluates to true in $ \sigma $, then we know that the last rule applied in the derivation tree was WhT(NS). Therefore, we know that there is a state $ \sigma'' $ for which <s1, $ \sigma $> -> $ \sigma'' $ and <while b do s1 end, $ \sigma'' $> -> $ \sigma' $ can be derived. Since x is not in wr(s), it is by definition of wr also not in wr(s1). That means we can apply the Lemma for both subtrees and have $ \sigma''(x) = \sigma' (x) = \sigma (x) $.

s = if b then s1 else s2 end: If b evaluates to false in $ \sigma $, then we know that the last rule applied in the derivation tree was IfF(NS). Therefore, we know that there is a derivation tree for <s2, $ \sigma $> -> $ \sigma' $. We also know from our definition of wr, that x is not in wr(s2). That means we can apply the Lemma for this subtree and get $ \sigma' (x) = \sigma (x) $.

If b evaluates to true in $ \sigma $, then we know that the last rule applied in the derivation tree was IfT(NS). Therefore, we know that there is a derivation tree for <s1, $ \sigma $> -> $ \sigma' $. We also know from our definition of wr, that x is not in wr(s1). That means we can apply the Lemma for this subtree and get $ \sigma' (x) = \sigma (x) $.

Assignment 9

This solution has not yet been reviewed by a second party. Please discuss! (schaerl: started discussion)

a) Satisfied. $ \Diamond(p \or r) $ holds for the states $ s_1, s_2, s_3 $, and $ (\Diamond u) $ holds for $ s_4, s_5, s_6 $. Therefore $ (\Diamond(p\or r)\or(\Diamond u)) $ holds for every state, $ \Rightarrow (\Box\diamond(p\or r))\or(\Box\Diamond u)) $

b) Not satisfied. Consider the trace $ s_1 s_2 s_1 s_2 ... $. $ not~u $ is always true. but $ s~or~t $ has to become true in finite time - which doesn't happen. Thus the trace is a counterexample. (See discussion for earlier unclarities and a verification in spin)

c) Satisfied. Same reason as in b) (See discussion)

d) Satisfied. If $ s $ holds at the next state, the next state will be $ s_4 $, from which no path can reach a state where $ p $ holds.

e) Not satisfied. For example does not hold for the path: $ s_1 s_3 s_5 s_4 s_6 s_5 s_4 s_6 ... $ (loop)

Assignment 10

a) $ P:= (x=0), e:=2, \sigma:=\{x=0\} $, $ \sigma':=\{x=2\} $

The left side of the implication is then true. But the right side of the implication is not as $ \mathfrak{B}[[x=e \land P]] \sigma' == ff $ as $ \mathfrak{B}[[x=2 \land x=0]]\sigma'==ff $ trivially Thus the right side of the implication is false and the implication doesn't hold.

b) Side condition $ x \not \in FV(P) \and x \not \in FV(e) $ This forbids the use of $ AssFw_{Ax} $ in 10a) and also allows the use in 10b.

c) Let $ P,x, e,\sigma,\sigma' $ be arbitrary.

Assume $ \mathfrak{B}[[P]]\sigma = tt $ and $ \exists T. root(T) = <x:=e,\sigma> \rightarrow \sigma' $.

Further assume our side-condition $ x \not \in FV(P) \and x \not \in FV(e) $.

By matching with $ Ass_{NS} $ we get $ \sigma' = \sigma[x \rightarrow A[[e]]\sigma] $.

To show: $ \mathfrak{B}[[x = e \and P]]\sigma' = tt $.

We have $ \mathfrak{B}[[x = e \and P]]\sigma' = \mathfrak{B}[[x = e]]\sigma' \and \mathfrak{B}[[P]]\sigma' $ by definition.

Since L1 and $ \mathfrak{B}[[P]]\sigma = tt \and x\not \in FV(P) $ we have $ \mathfrak{B}[[P]]\sigma' $.

Thus we get $ \mathfrak{B}[[x = e \and P]]\sigma' = \mathfrak{B}[[x = e]]\sigma' = ( \sigma'(x) = A[[e]]\sigma' ) $.

Thus we need to show $ \sigma'(x) = A[[e]]\sigma' $.

We have $ A[[e]]\sigma = A[[e]]\sigma \overset{L2 \, with \, v = A[[e]]\sigma}{\Leftrightarrow} \sigma[x \rightarrow A[[e]]\sigma](x) = A[[e]](\sigma[x \rightarrow A[[e]]\sigma]) \overset{\sigma' = \sigma[x \rightarrow A[[e]]\sigma]}{\Leftrightarrow} \sigma'(x) = A[[e]]\sigma' $.

Thus we can conclude $ \mathfrak{B}[[x = e \and P]]\sigma' = tt. \blacksquare $