Task 1: Program Verification

{- OPTIONS_GHC -fplugin=LiquidHaskell #-} module Task1 where import Data.Set hiding (insert, elems, take, drop) import Prelude hiding (take, drop) {-@ type TRUE = {v:Bool | v} @-}

1. Lists

1.1 Length Preservation: The function append below takes two lists and returns a new list that is the concatenation of the two input lists. Complete the type specification of append below, so that the property prop_append_1 is accepted by LiquidHaskell.

{-@ append :: xs:[a] -> ys:[a] -> [a] @-} append :: [a] -> [a] -> [a] append [] ys = ys append (x:xs) ys = x : append xs ys {-@ prop_append_1 :: (Ord a) => [a] -> [a] -> TRUE @-} prop_append_1 :: (Ord a) => [a] -> [a] -> Bool prop_append_1 xs ys = length (append xs ys) == length xs + length ys

1.2 Element Preservation: Append also preserves the elements of the input lists. We encode the elements of the list using the measure elems below.

{-@ measure elems @-} elems :: (Ord a) => [a] -> Set a elems [] = empty elems (x:xs) = singleton x `union` elems xs

Edit the type specification of append above, so that the properties prop_append_2 and prop_append_3 are accepted by LiquidHaskell.

{-@ prop_append_2 :: (Ord a) => [a] -> [a] -> TRUE @-} prop_append_2 :: (Ord a) => [a] -> [a] -> Bool prop_append_2 xs ys = isSubsetOf (elems xs) (elems (append xs ys)) {-@ prop_append_3 :: (Ord a) => [a] -> [a] -> TRUE @-} prop_append_3 :: (Ord a) => [a] -> [a] -> Bool prop_append_3 xs ys = isSubsetOf (elems xs) (elems (append xs ys))

1.3 Halve: The function halve below behaves the opposite of append. It takes a list and returns a pair of lists such that the elements of the input list are the union of the elements of the two output lists. Complete the definition of halve below, so that the type signature is accepted by LiquidHaskell.

{-@ halve :: xs:[a] -> {v:([a],[a]) | len (fst v) + len (snd v) = len xs && elems xs = union (elems (fst v)) (elems (snd v)) } @-} halve :: [a] -> ([a],[a]) halve [] = undefined halve [x] = undefined halve (x1:x2:xs) = undefined

2. Insertion Sort

In the class we saw that refinements of data type definitions can be used to encode increasing lists and use them to define insertion sort:

data IncList a = Emp | (:<) a (IncList a) {-@ data IncList a = Emp | (:<) { hd :: a, tl :: IncList {v:a | hd <= v}} @-} infixr 9 :< {-@ insert :: (Ord a) => x:a -> xs:IncList a -> IncList a @-} insert :: (Ord a) => a -> IncList a -> IncList a insert y Emp = y :< Emp insert y (x :< xs) | y <= x = y :< xs | otherwise = x :< insert y xs isort :: (Ord a) => [a] -> IncList a isort [] = Emp isort (x:xs) = insert x (isort xs)

2.1 Length Preservation: Measures can be defined for IncLists too. For example, the measure ilen below defines the length of an IncList.

ilen :: IncList a -> Int {-@ ilen :: IncList a -> Nat @-} {-@ measure ilen @-} ilen Emp = 0 ilen (_ :< xs) = 1 + ilen xs

Give the proper type specification for insert so that isort satisfies the below type:

{-@ isort :: (Ord a) => xs:[a] -> {v:IncList a | ilen v = len xs } @-}

Note: You should have discovered a bug in the code above. Fix it!

2.2 Element Preservation: We can also measure the elements of an IncList using the measure ielems below.

ielems :: Ord a => IncList a -> Set a {-@ ielems :: Ord a => IncList a -> Set a @-} {-@ measure ielems @-} ielems Emp = empty ielems (x :< xs) = singleton x `union` ielems xs

Give the proper type specification for insert so that isort satisfies the below type:

{-@ isort :: (Ord a) => xs:[a] -> {v:IncList a | ilen v = len xs && ielems v = elems xs } @-}

3. Merge Sort

The code below defines merge sort using lists refined to be increasing.

{-@ type IList a = [a]<{\x y -> x <= y}>@-} {-@ merge :: Ord a => xs:IList a -> ys:IList a -> {v:IList a | len v = len xs + len ys && elems v = union (elems xs) (elems ys) } @-} merge :: Ord a => [a] -> [a] -> [a] merge [] ys = ys merge xs [] = xs merge (x:xs) (y:ys) = undefined {-@ msort :: Ord a => xs:[a] -> {v:IList a | len v = len xs && elems v = elems xs} @-} msort :: Ord a => [a] -> [a] msort [] = [] msort [x] = [x] msort xs = merge (msort left) (msort right) where (left,right) = halve xs

3.1 Merge Complete the definition of merge above so that the type signature is accepted by LiquidHaskell.

3.2 Termination of Merge Termination of merge is not trivially shown. Provide a termination metric for merge so that you remove the lazy annotation below.

{-@ lazy merge @-}

3.3 Termination of Msort Termination of msort is also not trivial. Can you remove the lazy annotation below by providing a termination metric for msort?

{-@ lazy msort @-}

Hint: You have to refine the result of halve to ensure that when the input list has more than 2 elements, then each of the two output lists is smaller than the input list.