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
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX


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

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
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

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


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
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX


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

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

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


Ordered Lists


Lets refine the type to enforce order

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


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
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

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
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

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]