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

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