# Abstract Refinements

## Key Idea

Abstract The Property Away to make the specification Modular!

Then, instantiate the property back to get your specification.

## Ordered Lists

Previously we saw how to refine the list data definition to get ordered lists:

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


Just abstract the property away!

## Abstract Refinements on Data Structures

data List a = Emp | (:::) { hd :: a , tl :: List a } {-@ data List a < p :: a -> a -> Bool > = Emp | (:::) { hd :: a , tl :: List < p > a< p hd > } @-} -- a < p hd > stands for {v:a | p hd v}

Every element of the tail recursively satisfies p on the head!

## Instantiation of Refinements

Unrefined Lists
{-@ type TList a = List <{\x v -> true }> a @-}
Increasing Lists
{-@ type OList a = List <{\x v -> x <= v}> a @-}
Decreasing Lists
{-@ type DList a = List <{\x v -> v <= x}> a @-}
Unique Lists
{-@ type UList a = List <{\x v -> x /= v}> a @-}

## Using Abstract Refinements

Use increasing lists

{-@ type OList a = List <{\x v -> x <= v}> a @-}

to specify insertion sort, as before!

{-@ isort :: xs:List a -> OList a @-} isort Emp = Emp isort (x:::xs) = insert x (isort xs) {-@ insert :: x:a -> xs:OList a -> {v : OList a | length v == length xs + 1 && elems v == addElem x xs } @-} insert x (y ::: ys) | x <= y = x ::: y ::: ys | otherwise = y ::: insert x ys insert x _ = x ::: Emp

Haskell build-in list comes parameterized for you!

You can just instantiate the abstract refinement!

{-@ type IList a = [a]<{\x v -> (x <= v)}> @-}

And prove recursive list properties!

{-@ sort :: (Ord a) => [a] -> IList a @-} sort :: (Ord a) => [a] -> [a] sort = mergeAll . sequences where sequences (a:b:xs) | a compare b == GT = descending b [a] xs | otherwise = ascending b (a:) xs sequences [x] = [[x]] sequences [] = [[]] {- descending :: x:a -> IList {v:a | x < v} -> [a] -> [IList a] @-} descending a as (b:bs) | a compare b == GT = descending b (a:as) bs descending a as bs = (a:as): sequences bs {- ascending :: x:a -> (IList {v:a|v>=x} -> IList a) -> [a] -> [IList a] @-} ascending a as (b:bs) | a compare b /= GT = ascending b (\ys -> as (a:ys)) bs ascending a as bs = as [a]: sequences bs mergeAll [x] = x mergeAll xs = mergeAll (mergePairs xs) mergePairs (a:b:xs) = merge1 a b: mergePairs xs mergePairs [x] = [x] mergePairs [] = []

## Recap

1. Refinements: Types + Predicates
2. Subtyping: SMT Implication
3. Measures: Specify Properties of Data
4. Abstract Refinements: Decouple properties from code

Next:Bounded Refinements