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.

Property 1: Size


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


Property 2: Elements


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 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

Multiple Measures

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]