Case Study: Insertion Sort

sort :: (Ord a)   => List a -> List a
sort Emp          = Emp
sort (x:::xs)     = insert x (sort xs)

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

Goal: Verified Insertion Sort

Goal: specify & verify that output:

Is the same size as the input,

Has the same elements as the input,

Is in increasing order.

Exercise: insert

Q: Can you fix the type of insert so sort checks?

{-@ type ListN a N = {v:List a | length v == N } @-} {-@ sort :: (Ord a) => xs:List a -> ListN a {length xs} @-} sort Emp = Emp sort (x:::xs) = insert x (sort xs) {-@ insert :: (Ord a) => a -> xs:List a -> List a @-} insert x Emp = x ::: Emp insert x (y:::ys) | x <= y = x ::: y ::: ys | otherwise = y ::: insert x ys

Permutation

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

Hence, we can write Set-valued measures

Using the Data.Set API for convenience

import qualified Data.Set as S

Specifying A Lists Elements

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

inline lets us reuse Haskell terms in refinements.

Exercise: Verifying Permutation

Lets verify that sortE returns the same set of elements:

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

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

Property 3: Order

Yes, yes, but does sort actually sort ?

How to specify ordered lists ?

Refined Data: Ordered Pairs

Lets write a type for ordered pairs

data OrdPair = OP {opX :: Int, opY :: Int}

Legal Values value of opX < opY

okPair  = OP 2 4  -- legal
badPair = OP 4 2  -- illegal

Exercise: Ordered Pairs

Q: Can you refine the data type to legal values only?

{-@ data OrdPair = OP { opX :: Int, opY :: Int} @-} okPair = OP 2 4 -- legal badPair = OP 4 2 -- illegal

Refined Data: CSV Tables

data Csv = Csv { hdrs :: List String , vals :: List (List Int) } scores = Csv { hdrs = "Id" ::: "Midterm" ::: "Final" ::: Emp , vals = ( 1 ::: 25 ::: 88 ::: Emp) ::: ( 2 ::: 27 ::: 83 ::: Emp) ::: ( 3 ::: 19 ::: 93 ::: Emp) ::: Emp }

Exercise: Valid CSV Tables

Q: Can you refine Csv so scores' is rejected?

{-@ data Csv = Csv { hdrs :: List String , vals :: List (List Int) } @-} scores' = Csv { hdrs = "Id" ::: "Midterm" ::: "Final" ::: Emp , vals = ( 1 ::: 25 ::: 88 ::: Emp) ::: ( 2 ::: 83 ::: Emp) ::: ( 3 ::: 19 ::: 93 ::: Emp) ::: Emp }

Property 3: Ordered Lists

Refine the List data type to enforce ordering!

Lists

Lets define a type for ordered lists

data OList a = OEmp | (:<:) { oHd :: a , oTl :: OList a }

Ordered Lists

Lets refine the type to enforce order

{-@ data OList a = OEmp | (:<:) { oHd :: a , oTl :: OList a} @-}

Head oHd is smaller than every value v in tail oTl

Ordered Lists

Illegal values unrepresentable

okList :: OList Int okList = 1 :<: 2 :<: 3 :<: OEmp badList :: OList Int badList = 1 :<: 3 :<: 2 :<: OEmp

Exercise: Insertion Sort

Q: Oops. There's a problem! Can you fix it?

{-@ sortO :: xs:List a -> OListE a {elems xs} @-} sortO Emp = OEmp sortO (x:::xs) = insertO x (sortO xs) {-@ insertO :: x:a -> xs:_ -> OListE a {addElemO x xs} @-} insertO x (y :<: ys) | x <= y = y :<: x :<: ys | otherwise = y :<: insertO x ys insertO x _ = x :<: OEmp

Different Measures for List

We just wrote two measures for List

• length :: List a -> Nat
• elems :: List a -> Set a

Multiple Measures are Conjoined

Data constructor refinements are conjoined

data List a where
Emp   :: {v:List a |  length v = 0
&& elems v  = empty}
(:::) :: x:a
-> xs:List a
-> {v:List a |  length v = 1 + length xs
&& elems v  = addElem x  xs }

Recap

 Refinements: Types + Predicates Specification: Refined Input/Output Types Verification: SMT-based Predicate Subtyping Measures: Specify Properties of Data

Continue

Other Case Studies

Continue: [Termination Checking]