# Lösungsvorschlag Formal Methods And Functional Programming FS14

## 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 ${\displaystyle \Gamma :\equiv x:\tau _{1}}$

                        _____________________Var  _____________Int
${\displaystyle \Gamma \vdash }$ x :: ${\displaystyle \tau _{5}\to (\tau _{4},\tau _{3})}$       ${\displaystyle \Gamma \vdash }$ 0 :: ${\displaystyle \tau _{5}}$
__________________________________________App
${\displaystyle \Gamma \vdash }$ (x 0) :: ${\displaystyle (\tau _{4},\tau _{3})}$
__________________Var        __________________________snd
${\displaystyle \Gamma \vdash }$ x :: ${\displaystyle \tau _{3}\to \tau _{2}}$                ${\displaystyle \Gamma \vdash }$ snd (x 0) :: ${\displaystyle \tau _{3}}$
______________________________________________________App
${\displaystyle \Gamma \vdash }$ x (snd ( x 0)) :: ${\displaystyle \tau _{2}}$
______________________________________________________Abs*
${\displaystyle \vdash \lambda }$ x.x (snd (x 0)) :: ${\displaystyle \tau _{0}}$


Constraints: ${\displaystyle \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 ${\displaystyle \tau _{0}=(}$Int${\displaystyle \to (\tau _{4},}$Int${\displaystyle ))\to (\tau _{4},}$Int${\displaystyle )}$.

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

## Assignment 2: Proof by Induction

Let ${\displaystyle P(xs):=\forall f.\forall ys.zipWith(flip~f)~xs~ys=zipWith~f~ys~xs.}$ We show ${\displaystyle \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


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 ++ "]"


Alternative:

instance (Show a) => Show (Interval a) where
show (V a b) = show [a, 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 ${\displaystyle \sigma [n,m]:\equiv \sigma [x\mapsto n][y\mapsto m]}$

## Assignment 7

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

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

 while r >= 0 do ${\displaystyle \{P\wedge r>=0\wedge r=Z\}}$ ${\displaystyle \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; ${\displaystyle \{(N=q\times d+r+d)\wedge (d=D)\wedge (D>0)\wedge (r+d>=0)\wedge (r+d=Z)\}}$ ${\displaystyle \models \{\Downarrow (N=(q+1-1)\times d+r+d)\wedge (d=D)\wedge (D>0)\wedge (r+d>=0)\wedge (r q := q + 1; ${\displaystyle \{\Downarrow (N=(q-1)\times d+r+d)\wedge (d=D)\wedge (D>0)\wedge (r+d>=0)\wedge (r ${\displaystyle \models \{\Downarrow (N=q\times d+r)\wedge (d=D)\wedge (D>0)\wedge (r+d>=0)\wedge (r end ${\displaystyle \{\Downarrow P\wedge r<0\}}$ ${\displaystyle \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; ${\displaystyle \{\Downarrow (N=q\times d+r-d)\wedge (d=D)\wedge (D>0)\wedge (r>=0)\wedge (r-d<0)\}}$ ${\displaystyle \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; 

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

## Assignment 8

a)

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

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

${\displaystyle wr(s_{1};s_{2})=wr(s_{1})\cup wr(s_{2})}$

${\displaystyle wr({\text{if }}b{\text{ then }}s_{1}{\text{ else }}s_{2}{\text{ end}})=wr(s_{1})\cup wr(s_{2})}$

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

b)

Open for discussion:

Let s, ${\displaystyle \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, ${\displaystyle \sigma }$> -> ${\displaystyle \sigma '}$. We do a case distinction on s:

Base cases:

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

s = a := e: Since x is not in wr(s), x ≠ a. Therefore ${\displaystyle \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, ${\displaystyle \sigma }$> -> ${\displaystyle \sigma '}$ has to be Seq(NS). Therefore, we know that there is a state ${\displaystyle \sigma ''}$ for which <s1, ${\displaystyle \sigma }$> -> ${\displaystyle \sigma ''}$ and <s2, ${\displaystyle \sigma ''}$> -> ${\displaystyle \sigma '}$ can be derived. Then we can apply the Lemma for s1 and s2 and we have ${\displaystyle \sigma ''(x)=\sigma '(x)=\sigma (x)}$.

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

If b evaluates to true in ${\displaystyle \sigma }$, then we know that the last rule applied in the derivation tree was WhT(NS). Therefore, we know that there is a state ${\displaystyle \sigma ''}$ for which <s1, ${\displaystyle \sigma }$> -> ${\displaystyle \sigma ''}$ and <while b do s1 end, ${\displaystyle \sigma ''}$> -> ${\displaystyle \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 ${\displaystyle \sigma ''(x)=\sigma '(x)=\sigma (x)}$.

s = if b then s1 else s2 end: If b evaluates to false in ${\displaystyle \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, ${\displaystyle \sigma }$> -> ${\displaystyle \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 ${\displaystyle \sigma '(x)=\sigma (x)}$.

If b evaluates to true in ${\displaystyle \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, ${\displaystyle \sigma }$> -> ${\displaystyle \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 ${\displaystyle \sigma '(x)=\sigma (x)}$.

## Assignment 9

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

a) Satisfied. ${\displaystyle \Diamond (p\lor r)}$ holds for the states ${\displaystyle s_{1},s_{2},s_{3}}$, and ${\displaystyle (\Diamond u)}$ holds for ${\displaystyle s_{4},s_{5},s_{6}}$. Therefore ${\displaystyle (\Diamond (p\lor r)\lor (\Diamond u))}$ holds for every state, ${\displaystyle \Rightarrow (\Box \diamond (p\lor r))\lor (\Box \Diamond u))}$

b) Not satisfied. Consider the trace ${\displaystyle s_{1}s_{2}s_{1}s_{2}...}$. ${\displaystyle not~u}$ is always true. but ${\displaystyle 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 ${\displaystyle s}$ holds at the next state, the next state will be ${\displaystyle s_{4}}$, from which no path can reach a state where ${\displaystyle p}$ holds.

e) Not satisfied. For example does not hold for the path: ${\displaystyle s_{1}s_{3}s_{5}s_{4}s_{6}s_{5}s_{4}s_{6}...}$ (loop)

## Assignment 10

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

The left side of the implication is then true. But the right side of the implication is not as ${\displaystyle {\mathfrak {B}}[[x=e\land P]]\sigma '==ff}$ as ${\displaystyle {\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 ${\displaystyle x\not \in FV(P)\land x\not \in FV(e)}$ This forbids the use of ${\displaystyle AssFw_{Ax}}$ in 10a) and also allows the use in 10b.

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

Assume ${\displaystyle {\mathfrak {B}}[[P]]\sigma =tt}$ and ${\displaystyle \exists T.root(T)=\rightarrow \sigma '}$.

Further assume our side-condition ${\displaystyle x\not \in FV(P)\land x\not \in FV(e)}$.

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

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

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

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

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

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

We have ${\displaystyle 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 ${\displaystyle {\mathfrak {B}}[[x=e\land P]]\sigma '=tt.\blacksquare }$