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

## 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 `List`

s Elements

`inline`

lets us reuse Haskell terms in refinements.

## Exercise: Verifying Permutation

Lets verify that `sortE`

returns the same set of elements:

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

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

## Refined Data: CSV Tables

## Exercise: Valid CSV Tables

**Q:** Can you refine `Csv`

so `scores'`

is rejected?

## Property 3: Ordered Lists

**Refine** the `List`

data type to enforce **ordering**!

## Lists

Lets **define** a type for ordered lists

## Ordered Lists

Lets **refine** the type to enforce **order**

Head `oHd`

is **smaller than every value** `v`

in tail `oTl`

## Ordered Lists

*Illegal values unrepresentable*

## Exercise: Insertion Sort

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

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