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

Wechseln zu: Navigation, Suche

## 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 = x:(dvdNxt xs)
| otherwise         = dvdNxt xs

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

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

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

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

--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]$

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

$\{( N = (q+1) \times d + r-d ) \wedge (d=D) \wedge (D>0) \wedge (r >= 0) \wedge (r-d < 0) \}$ $\models\{ (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$