# Lösungsvorschlag Formal Methods Endterm 2012

## 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
$G,Z,Q(x)\vdash G$
-------------------------- $\forall E$
$G,Z,Q(x)\vdash P(x)\wedge R(x)$
------------------- Ax        -------------------------- $\wedge ER$
$G,Z,Q(x)\vdash Q(x)$                  $G,Z,Q(x)\vdash R(x)$
-------------------------------------------------------- $\wedge I$
$G,Z,Q(x)\vdash Q(x)\wedge R(x)$
----------- Ax         -------------------------------------------------------- $\exists I$
$G,Z\vdash Z$                          $G,Z,Q(x)\vdash \exists x.Q(x)\wedge R(x)$
------------------------------------------------------------------------------- $\exists E$
$G,Z\vdash \exists x.Q(x)\wedge R(x)$
------------------------------------------------------------------------------- $\rightarrow I$
$G\vdash Z\rightarrow \exists x.Q(x)\wedge R(x)$
------------------------------------------------------------------------------- $\rightarrow I$
$\vdash (\forall y.P(y)\wedge R(y))\rightarrow ((\exists x.Q(x))\rightarrow \exists x.Q(x)\wedge R(x))$


 $G=\forall y.P(y)\wedge R(y)$
$Z=\exists x.Q(x)$


### 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         = 
| x mod 2 == 0 = x : collatz (x div 2)
| otherwise      = x : collatz (3*x + 1)

collatz :: Int -> [Int]
collatz 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: $\forall xs::[a].\forall ys::[a].$ 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)


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

$\{x=X\land y=Y\land X\leq Y\}$
$\models \{{\frac {x+y}{2}}={\frac {X+Y}{2}}\land x\leq y\}$
while x < y do
$\{x
$\models \{{\frac {x+1+y-1}{2}}={\frac {X+Y}{2}}\land x\leq y-1\land y-1-x
y := y - 1
$\{{\frac {x+1+y}{2}}={\frac {X+Y}{2}}\land x\leq y\land y-x
if x < y then
$\{x
$\models \{{\frac {x+1+y}{2}}={\frac {X+Y}{2}}\land x+1\leq y\land y-(x+1)
x := x + 1
$\{{\frac {x+y}{2}}={\frac {X+Y}{2}}\land x\leq y\land y-x=Z$
else
$\{\lnot (x
$\models \{{\frac {x+y}{2}}={\frac {X+Y}{2}}\land x\leq y\land y-x
skip
$\{{\frac {x+y}{2}}={\frac {X+Y}{2}}\land x\leq y\land y-x
end
$\{\Downarrow {\frac {x+y}{2}}={\frac {X+Y}{2}}\land x\leq y\land y-x
end
$\{\Downarrow \lnot (x
$\{\Downarrow x=y\land y={\frac {X+Y}{2}}\}$


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

$x>0\wedge y>0$

$x<=0\wedge y<=0$

$x<=0\wedge y>0$

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

### Assignment 2

We assume: $\vdash \{P\}{\text{while b do s end}}\{Q\}$
From our assumption, we know that $\exists T:root(T)\equiv \{P\}{\text{while do s end}}\{Q\}$

to prove: $\vdash \{P\}{\text{if b the s; while b do s end else skip end}}\{Q\}$
We prove this by induction on the structure of the derivation tree T, considering cases for the last rule applied.

Case 1: $WH_{Ax}$:

Then T has the form:

           $T1$
-------------------------
$\{b\wedge P\}{\text{s}}\{P\}$
-------------------------
$\{P\}{\text{while b do s end}}\{Q\}$

With this informations we can construct the following derivation tree:
$T$
-------------------------
$T1$   $\{P\}{\text{while b do s end}}\{Q\}$
--------------------------------              ------------------
$\{b\wedge P\}{\text{s;while b do s end}}\{Q\}$                      $\{\neg b\wedge P\}{\text{skip}}\{Q\}$
----------------------------------------------------------------------------
$\{P\}{\text{if b then s; while b do s end else skip end}}\{Q\}$

Case 2: $CONS_{Ax}$:



then T has the form

          $T1$
-------------------------
$\{P'\}{\text{while b do s end}}\{Q'\}$
-------------------------
$\{P\}{\text{while b do s end}}\{Q\}$


and we build the following tree

                      $T2$
------------------------------------------------
$\{P'\}{\text{if b then s; while b do s end else skip end}}\{Q'\}$
------------------------------------------------
$\{P\}{\text{if b then s; while b do s end else skip end}}\{Q\}$


where we know from our I.H. $\forall T' and the fact that $T2 that there exists a tree T2 with root(T2) = $\{P'\}{\text{if b then s; while b do s end else skip end}}\{Q'\}$ and thus have proven the statement.

### Assignment 3

Choose:

• op = par
• $\sigma =\sigma _{\text{zero}}$
• $\sigma '=\sigma _{\text{zero}}[x\mapsto 1][y\mapsto 1]$
• 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

• $\phi _{1}$: 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: $s_{1},(s_{3})^{\omega }$
• $\phi _{2}$: No. The computation $s_{1},(s_{3})^{\omega }$ does not satisfy the property.
• $\phi _{3}$: No. The computation $(s_{1},s_{2})^{\omega }$ does not satisfy the property.
• $\phi _{4}$: Yes. We can simply falsify the left-hand side and therefore the implication becomes true: $(s_{1},s_{2})^{\omega }$.
• $\phi _{4}$: 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.