Lösungsvorschlag Formal Methods Endterm 2012

Aus VISki
Wechseln zu: Navigation, Suche

Part 1

Assignment 1

Prelude> :t \x -> [x 0]
\x -> [x 0] :: Num a => (a -> t) -> [t]
Prelude> :t \x z -> z (\y -> x)
\x z -> z (\y -> x) :: t2 -> ((t1 -> t2) -> t) -> t
Prelude> :t map map
map map :: [a -> b] -> [[a] -> [b]]
Prelude> :t \x -> x >>= (\y -> y)
\x -> x >>= (\y -> y) :: Monad m => m (m a) -> m a


Explanation for map map:

Let map map == map map'

map :: (a -> b) -> ([a] -> [b])

map' :: (c -> d) -> ([c] -> [d])

map' :: ((a -> b) -> d) -> ([a -> b] -> [d]) --Substitute c for (a -> b)

map' :: ((a -> b) -> ([a] -> [b])) -> ([a -> b] -> [([a] -> [b]]) --Substitute d for ([a] -> [b])

map' map:: [a -> b] -> [[a] -> [b]] --remove the first argument, because it has already been applied (it is map after all).

Assignment 2

(a)

                                                      -------------------------- Ax
                                                           
                                                      -------------------------- 
                                                        
                        ------------------- Ax        -------------------------- 
                                            
                        -------------------------------------------------------- 
                                  
 ----------- Ax         -------------------------------------------------------- 
                            
 ------------------------------------------------------------------------------- 
                              
 ------------------------------------------------------------------------------- 
                             
 ------------------------------------------------------------------------------- 
                     
 
 
 

Assignment 3

a)

last :: [a] -> a 
last []     = error "empty list"
last [x]    = x
last (x:xs) = last xs


b)

collatz :: Int -> [Int]
collatz x
       | x <= 0         = error "Not supported"
       | x == 1         = [1]
       | x `mod` 2 == 0 = x : collatz (x `div` 2)
       | otherwise      = x : collatz (3*x + 1)
collatz :: Int -> [Int]
collatz 1 = [1]
collatz n = n: if (n `mod` 2 == 0) then collatz (n `div` 2) else collatz (3*n+1)
collatz :: Int -> [Int]
collatz x 		
          | x <= 0     = error "Please insert a number > 0"
          | otherwise  = aux x [x]
              where 
                  aux 1 xs	= xs
                  aux y xs
                       | mod y 2 == 0	= aux (div y 2) (xs ++ [div y 2])
                       | otherwise 	= aux (y*3+1) 	(xs ++ [y*3+1]) 

c)

avg' :: [Int]-> Int
avg' xs = g (foldr f (0,0) xs)
           where
              f a (x,y)  = (x + a, y + 1)
              g   (x,y)  = uncurry div

Assignment 4

imerge :: [a] -> [a] -> [a]
imerge [] ys = ys                       --imerge.1
imerge (x:xs) ys = x:(imerge ys xs)     --imerge.2
length :: [a] -> Int
length [] = 0                           --length.1
length (x:xs) = 1 + length xs           --length.2

To prove: length(imerge xs ys) = length xs + length ys

We prove by induction. let ys be arbitrary.

Base case:

length (imerge [] ys)
= length ys                                -- imerge.1
= 0 + length ys                            -- algebraic
= length [] + length ys                    -- length.1

Step: Assumption: length(imerge xs ys) = length xs + length ys

length (imerge (x:xs) ys)
= length (x: imerge ys xs)                 -- imerge.2
= 1 + length (imerge ys xs)                -- length.2

Remark: The I.H. is here not applicable because imerge xs ys != imerge ys xs

case 0: ys==[]

= 1 + length (imerge [] xs)                -- def ys
= 1 + length xs                            -- imerge.1
= length (x:xs)                            -- length.2
= length (x:xs) + 0                        -- arith.
= length (x:xs) + length []                -- length.1
= length (x:xs) + length ys                -- def ys

case 1: ys == z:zs

= 1 + length (imerge (z:zs) xs)            -- def ys
= 1 + length (z:(imerge xs zs))            -- imerge.2
= 1 + 1 + length (imerge xs zs)            -- length.2
= 1 + 1 + length xs + length zs            -- Induction Hypothesis
= 1 + length xs + 1 + length zs            -- arith.
= length (x:xs) + length (z:zs)            -- twice length.2
= length (x:xs) + length ys                -- def ys

Assignment 5

a)

foldDict :: (c -> k -> v -> c -> c) -> c -> Dict k v -> c
foldDict f e (Empty)          = e
foldDict f e (Join d1 k v d2) = f (foldDict f e d1) k v (foldDict f e d2)

b)

lookupDict :: Ord k => k -> Dict k v -> Maybe v
lookupDict key (Empty)        = Nothing
lookupDict key (Join d1 k v d2)
          | k == key  = Just v
          | key < k   = lookupDict key d1
          | otherwise = lookupDict key d2


c)

insertDict :: Ord a => a -> b -> Dict a b -> Dict a b
insertDict k v Empty = Join Empty k v Empty
insertDict k v (Join l k2 v2 r)
       | k2 > k = (Join (insertDict k v l) k2 v2 r)
       | k2 < k = (Join l k2 v2 (insertDict k v r))
       | otherwise = Join l k v r

d)

ordered :: Ord k => Dict k v -> Bool
ordered = sorted . flatten
       where
           sorted xs = and $ zipWith (<) xs (drop 1 xs) 
           flatten = foldDict (\xs k _ ys -> xs ++ [k] ++ ys) []
   -- easy alternative for sorted which is more readable (recursive):
           sorted [] = True
           sorted [x] = True
           sorted (x:y:xs) = (x<y) && sorted (y:xs)
ordered :: Ord k => Dict k v -> Bool
ordered = sorted . flatten
       where
           sorted xs = all (uncurry (<)) $ zip xs (drop 1 xs) 
           flatten = foldDict (\xs k _ ys -> xs ++ [k] ++ ys) []
ordered :: Ord k => Dict k v -> Bool
ordered = sorted . flatten
       where
           sorted [] = True
           sorted xs = all (uncurry (<)) $ zip xs (tail xs) 
           flatten = foldDict (\xs k _ ys -> xs ++ [k] ++ ys) []
ordered Empty = True
ordered d = extract $ aux d
       where
         comb (lmin, lmax, lord) k v (rmin, rmax, rord) = (lmin, rmax, lmax <= k && k <= rmin && lord && rord)
         aux (Join Empty k v Empty) = (k, k, True)
         aux (Join d1 k v Empty) = comb (aux d1) k v (k, k, True)
         aux (Join Empty k v d2) = comb (k, k, True) k v (aux d2)
         aux (Join d1 k v d2) = comb (aux d1) k v (aux d2)
         extract (a, b, c) = c
   -- using a lambda pair for lower and upper bound checks starting with no bounds
ordered :: Ord k => Dict k v -> Bool
ordered = ordered' (\x -> True, \x -> True)
     where
       ordered' _ Empty = True
       ordered' (a, b) (Join l k v r) = (a k) && (b k) && (ordered' (a, (<k)) l) && (ordered' ((>k), b) r)

My "slightly" more readeable version:

ordered :: Ord k => Dict k v -> Bool
ordered (Empty) = True
ordered (Join d1 k v d2) = and ([ordered d1, ordered d2] ++ map (k <) (enumerateKeys d2) ++ map (k >) (enumerateKeys d1))  
enumerateKeys :: Dict k v -> [k]
enumerateKeys (Empty) = []
enumerateKeys (Join d1 k v d2) = [k] ++ (enumerateKeys d2) ++ (enumerateKeys d1)

The idea behind this is to exactly implement all the requirements for a dictionary beeing ordered. Namely: 1. all the keys in the left subtree are smaller than k 2. all the keys in the right subtree are greater than k 3. both the left nd the right subtree are ordered


and ([ordered d1, ordered d2] ++     map (k <) (enumerateKeys d2) ++                   map (k >) (enumerateKeys d1))
    ^checks if subtrees are ordered ^boolean list with k < every key in right subtree ^boolean list with k > every key in left subtree

The and then and's all entries in the list together and only iff all requirements are set it return True


Another version:

ordered Empty = True
ordered (Join Empty k v Empty) = True
ordered (Join Empty k v d2) = key d2 > k && ordered d2
ordered (Join d1 k v Empty) = key d1 < k && ordered d1
ordered (Join d1 k v d2) = key d1 < k && key d2 > k && ordered d1 && ordered d2
key Empty = 0
key (Join _ k _ _) = k

Part 2

Assignment 1



while x < y do
  
  
  y := y - 1
  
  if x < y then
    
    
    x := x + 1
    
  else
    
    
    skip
    
  end
  
end


The loop variant might not be obvious. But as we have the side condition of the total correnctnes rule we have to ensure that given the loop invariant and the loop condition. So only will not work. So let's take a closer look at . There are 3 cases:

The forth case is omited as we have from the loop condition. In all these cases will decrease during the loop. Check this yourself. ;-)

Assignment 2

We assume: 
From our assumption, we know that 

to prove: 
We prove this by induction on the structure of the derivation tree T, considering cases for the last rule applied.
Case 1: : 

Then T has the form:
           
-------------------------
      
-------------------------


With this informations we can construct the following derivation tree:
                   
      -------------------------
   
--------------------------------              ------------------
                      
----------------------------------------------------------------------------
                 
Case 2: : 

then T has the form

          
-------------------------

-------------------------

and we build the following tree

                      
------------------------------------------------

------------------------------------------------

where we know from our I.H. and the fact that that there exists a tree T2 with root(T2) = and thus have proven the statement.

Assignment 3

Choose:

  • op = par
  • s2 = x := 1;

It is easily reachable for the default rules by applying the rules in the order

  1. Par, execute first if
  2. Par, execute s2
  3. If
  4. Ass

But when choosing the rules given in the assignment, it is only possible to execute the entire if statement in one step. No parallel computation can interfere in this step. Therefore y can never be assigned to 1 by that rules. It is a similar situation to the big step (natural) semantics that cannot perform "real" interleaving computations.

Assignment 4

init {
    byte stack_1 = 100;
    byte stack_2 = 100;
    bit p1_wins = 0;
    bit p2_wins = 0;

    do     // game loop
      :: stack_1 == 0 && stack_2 == 0 -> break
      :: else ->
                if   // player 1 chooses a stack and removes some matches
                  :: stack_1 > 0 -> stack_1--;
                                    do
                                      :: stack_1 > 0 -> stack_1--
                                      :: break      // edit note: you cannot use "else" here, otherwise player 1 would always take the whole stack
                                    od
                  :: stack_2 > 0 -> stack_2--;
                                    do
                                      :: stack_2 > 0 -> stack_2--
                                      :: break      // edit note: you cannot use "else" here, otherwise player 1 would always take the whole stack
                                    od
                fi;
                if
                  :: stack_1 == 0 && stack_2 == 0 -> p1_wins = 1; break;   // check if player 1 removed the last sticks.
                  :: else -> skip //otherwise it will timeout here
                fi
                if // player 2 turn
                  :: stack_1 > stack_2 -> stack_1 = stack_2
                  :: stack_2 > stack_1 -> stack_2 = stack_1
                fi
                if
                  :: stack_1 == 0 && stack_2 == 0 -> p2_wins = 1; break;   // check if player 2 removed the last sticks
                  :: else -> skip //otherwise it will timeout here
                fi
    od;
    assert(p1_wins == 0);
    assert(p2_wins == 1);
}

Assignment 5

  • : Yes. We start in s1 and in the next step definitely q holds, making the left side of the implication false. Therefore the formula holds. Computation:
  • : No. The computation does not satisfy the property.
  • : No. The computation does not satisfy the property.
  • : Yes. We can simply falsify the left-hand side and therefore the implication becomes true: .
  • : Yes but not because of the reason above: The LTL formula has to be satisfied for every trace, not just the ones where the left hand side evaluates to false. It is satisfied because we start in s1 where q does not hold (so we cannot have an infinite trace of states in which q holds), therefore for the left hand side to be true, eventually r must hold. This trivially implies that eventually r must hold.