Lösungsvorschlag Formal Methods And Functional Programming FS09 Repetition

Aus VISki
Wechseln zu: Navigation, Suche

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 be the same as
                                                             ------------------------- 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, > and <s2, > obviously terminate.
  • However, <s1 par s2, > does not terminate for the derivation sequence:
  1. <s1 par s2, > →₁
  2. <s1 par if x#0 then while true do skip end else skip end, > →₁
  3. <if x#0 then while true do skip end else skip end, > →₁
  4. <while true do skip end, > →₁
  5. ...

Assignment 6

Work in progress.png

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 =

t' =

where

(b)

Safety properties need to be violated in finite time.

is a safety property. Consider the finite sequence t' = . This sequence violates the property and can't be repaired by any infinite sequence t with t' as prefix.

is a safety property. Consider the finite sequence t' = . This sequence violates the property and can't be repaired by any infinite sequence t with t' as prefix.