Case Study: Sorting Lists



Insertion Sort


Merge Sort

Case Study: Sorting Lists



Insertion Sort


Merge Sort

Insertion Sort


            sort :: (Ord a) => List a -> List a
            sort []         = []
            sort (x:xs)     = insert x (sort xs)
            
            insert :: (Ord a) => a -> List a -> List a
            insert x []     = x : Emp
            insert x (y:ys)
              | x <= y      = x : y : ys
              | otherwise   = y : insert x ys

Goal: Verified Insertion Sort



Specify & Verify that output of sort


Is the same size as the input

Has the same elements as the input

(Later) Is actually sorted in increasing order

Goal: Verified Insertion Sort



Specify & Verify that output of sort


Is the same size as the input

Has the same elements as the input

(Later) Is actually sorted in increasing order

Property 1: Size



An Alias for lists of size N

{-@ type ListN a N = {v:[a] | length v == N} @-}

Property 1: Size


{-@ sort :: xs:[a] -> ListN a (length xs) @-} sort [] = [] sort (x:xs) = insert x (sort xs) {-@ insert :: a -> xs:[a] -> [a] @-} insert x [] = [x] insert x (y:ys) | x <= y = x : y : ys | otherwise = y : insert x ys

Exercise: Fix the type of insert so sort checks?

Goal: Verified Insertion Sort



Specify & Verify that output of sort


Is the same size as the input

Has the same elements as the input

(Later) Is actually sorted in increasing order

Property 2: Permutation


Same size is all fine, how about same elements in output?

SMT Solvers Reason About Sets


Hence, we can write Set-valued measures


Using the standard library Data.Set API for convenience


                    import qualified Data.Set as S

Specifying A List's Elements


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


inline lets us reuse (non-recursive) program functions in refinements

Property 2: Permutation

Lets verify that sortE returns the same set of elements:

{-@ type ListE a S = {v:[a] | elems v = S} @-} {-@ sortE :: xs:[a] -> ListE a (elems xs) @-} sortE [] = [] sortE (x:xs) = insertE x (sortE xs) {-@ insertE :: x:a -> xs:[a] -> [a] @-} insertE x [] = [x] insertE x (y:ys) | x <= y = x : y : ys | otherwise = y : insertE x ys

Exercise: Can you fix the type for insertE so sortE verifies?

Goal: Verified Insertion Sort



Specify & Verify that output of sort


Is the same size as the input

Has the same elements as the input

(Later) Is actually sorted in increasing order

Case Study: Sorting Lists



Insertion Sort


Merge Sort

MergeSort: Size

Exercise: Fix specifications for split and merge to verify msort

{-@ msort :: xs:[a] -> ListN a (length xs) @-} msort [] = [] msort [x] = [x] msort xs = let (ys, zs) = split xs in merge (msort ys) (msort zs) {-@ split :: xs:[a] -> ([a], [a]) @-} split (x:y:zs) = let (xs, ys) = split zs in (x:xs, y:ys) split xs = (xs, []) {-@ merge :: xs:[a] -> ys:[a] -> [a] @-} merge xs [] = xs merge [] ys = ys merge (x:xs) (y:ys) | x <= y = x : merge xs (y:ys) | otherwise = y : merge (x:xs) ys

MergeSort: Permutation




Exercise: Modify the previous code to verify that

                {-@ msort :: xs:[a] -> ListE a (elems xs) @-}