Case Study: Insertion Sort



















Insertion Sort


sort :: (Ord a) => List a -> List a
sort []           = 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:


  1. Is the same size as the input,
  2. Has the same elements as the input,
  3. Is in increasing order.













Property 1: Size


















Exercise: insert

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

{-@ 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 ?













Recall: Refined Data Types













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 {v:a | oHd <= v}} @-}


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 }













Measures vs. Indexed Types


Unlike indexed types, measures ...


  • Decouple properties from data type

  • Reuse same data type with different invariants













Refinements vs. Full Dependent Types


  • Limited to decidable logics but ...

  • Offer massive amounts of automation


Compare with insertionSort in:













Continue


Next: Case Studies


[Continue]