Lösungsvorschlag Formal Methods And Functional Programming FS09 Repetition

Repetition Exam (September 12th, 2009)

Alternative Solution: Lösungsvorschlag FS 2009

Part 1

Assignment 1

(a)

 

 Prelude> :t (\a b c -> c b a) (\a b c -> c b a) :: t2 -> t1 -> (t1 -> t2 -> t) -> t 

 

 Prelude> :t (\b -> ((\x -> x), b 1)) (\b -> ((\x -> x), b 1)) :: Num a => (a -> t) -> (t1 -> t1, t) 

 

 Prelude> :t (\xs x -> head xs True > x) (\xs x -> head xs True > x) :: Ord a => [Bool -> a] -> a -> Bool 

(b)

Γ = c : t1, x : t5

------------------- Var (6)   ------------ Var (5)
Γ ⊢ c :: t7 -> Int            Γ ⊢ x :: t7
------------------------------------------ App
Γ ⊢ c x :: Int
----------------------- iszero (4)                        ----------------------- Var (2)
Γ ⊢ iszero (c x) :: t6                                    x : t2 ⊢ x :: (t4, t3)
------------------------------- Abs (3)                   ---------------------- snd
c : t1 ⊢ λx.iszero (c x) :: t0                            x : t2 ⊢ snd x :: t3
----------------------------------- Abs                   --------------------- Abs (1)
⊢ λc.(λx.iszero (c x)) :: t1 -> t0                        ⊢ λx.snd x :: t1
---------------------------------------------------------------------------- App
⊢ (λc.(λx.iszero (c x))) (λx.snd x) :: t0


Constraints:

(1) t1 = t2 -> t3
(2) t2 = (t4, t3)
(3) t0 = t5 -> t6
(4) t6 = Bool
(5) t7 = t5
(6) t1 = t7 -> Int
(7) t3 = Int           -- (1) and (6)
(8) t7 = t2            -- (1) and (6)


And we get:

 t0
= t5 -> t6             -- (3)
= t5 -> Bool           -- (4)
= t7 -> Bool           -- (5)
= t2 -> Bool           -- (8)
= (t4, t3) -> Bool     -- (2)
= (t4, Int) -> Bool    -- (7)


Assignment 2

Proof: Let ys::[a] be arbitrary and P(xs) := rev (xs ++ rev ys) = ys ++ rev xs. We show ∀xs::[a]. P(xs) by induction.

Base Case: Show P([]).

 rev ([] ++ rev ys)
= rev (rev ys)        -- app.1
= ys                  -- Lemma 1
= ys ++ []            -- Lemma 2
= ys ++ rev []        -- rev.1


Step case: Let x::a and xs::[a] be arbitrary. Assume P(xs). Show P(x:xs). Hence, we have to show rev ((x:xs) ++ rev ys) = ys ++ rev (x:xs).

 rev ((x:xs) ++ rev ys)
= rev (x:(xs ++ rev ys))     -- app.2
= rev (xs ++ rev ys) ++ [x]  -- rev.2
= (ys ++ rev xs) ++ [x]      -- P(xs)
= ys ++ ((rev xs) ++ [x])    -- Lemma 3
= ys ++ rev (x:xs)           -- rev.2


qed.

Assignment 3

  risers :: Ord a => [a] -> [[a]]
risers = foldr go [[]]
where
go x [[]] = [[x]]
go x (y:ys) = if x <= (head y) then (x:y):ys else [x]:(y:ys)


Assignment 4

(a)

  mapDir :: (Dir -> Dir) -> Block -> Block
mapDir f (Tile b) = Tile (map (\(x,y) -> (f x, mapDir f y)) b)


(b)

  rotateCw :: Block -> Block
rotateCw b = mapDir go b
where
go Down = Left1
go Left1 = Up
go Up = Right1
go Right1 = Down


(c)

  foldBlock :: ([(Dir, a)] -> a) -> Block -> a
foldBlock f (Tile b) = f (map (\(x,y) -> (x, foldBlock f y)) b)


Part 2

Assignment 5

(a)

• Let s be the statement y := y*y; x := x-1
• Let ${\displaystyle [v1,v2]}$ be the same as ${\displaystyle \sigma [x\mapsto v1,y\mapsto v2]}$
                                                             ------------------------- ASS  -------------------------- ASS
<y:=y*y, [1,4]> -> [1,16]      <x:=x-1, [1,16]> -> [0,16]
------------------------ ASS   ------------------------ ASS  --------------------------------------------------------- SEQ ------------------- WHF
<y:=y*y, [2,2]> -> [2,4]       <x:=x-1, [2,4]> -> [1,4]      <s, [1,4]> -> [0,16]                                          <w, [0,16]> -> [0,16]
------------------------------------------------------- SEQ  --------------------------------------------------------------------------------- WHT
<s, [2,2]> -> [1,4]                                          <w, [1,4]> -> [0,16]
--------------------------------------------------------------------------------- WHT
<w, [2,2]> -> [0,16]


(b)

s1 = (x:=1)

s2 = (x:=0; if x#0 then while true do skip end else skip end)

• Both configurations <s1, ${\displaystyle \sigma }$> and <s2, ${\displaystyle \sigma }$> obviously terminate.
• However, <s1 par s2, ${\displaystyle \sigma }$> does not terminate for the derivation sequence:
1. <s1 par s2, ${\displaystyle \sigma }$> →₁
2. <s1 par if x#0 then while true do skip end else skip end, ${\displaystyle \sigma [x\mapsto 0]}$> →₁
3. <if x#0 then while true do skip end else skip end, ${\displaystyle \sigma [x\mapsto 1]}$> →₁
4. <while true do skip end, ${\displaystyle \sigma [x\mapsto 1]}$> →₁
5. ...

Assignment 6

 Diese Aufgabe wurde noch von niemandem gelöst und wartet noch immer auf einen Musterlöser. Hast du dieses Fach bereits besucht? Hilf mit, die Qualität dieser Seite zu verbessern, indem du eine plausible Lösung für diese Frage notierst!

Assignment 7

(a)

t = ${\displaystyle \{p,q\}\{p,q\}\{p,q\}\{p,q\}...}$

t' = ${\displaystyle \{\}\{\}\{\}\{\}...}$

where

${\displaystyle \{\}=\neg p\land \neg q}$

${\displaystyle \{q,p\}=p\land q}$

(b)

Safety properties need to be violated in finite time.

${\displaystyle \phi }$ is a safety property. Consider the finite sequence t' = ${\displaystyle \{p\}\{p\}\{p\}}$. This sequence violates the property ${\displaystyle \phi }$ and can't be repaired by any infinite sequence t with t' as prefix.

${\displaystyle \psi }$ is a safety property. Consider the finite sequence t' = ${\displaystyle \{p\}}$. This sequence violates the property ${\displaystyle \psi }$ and can't be repaired by any infinite sequence t with t' as prefix.