True
is a bad argument10
is a good argumenttake
and drop
reconstruction0
fib
is an uninterpreted function0
average
take
fib
fib
is an uninterpreted functionList
s Elementsappend
take
and drop
reconstructiontake
and drop
reconstruction
Lets define our own List
data type:
Measure
Haskell function with a single equation per constructor
Measure
Strengthens type of data constructor
data List a where
Emp :: {v:List a | length v = 0}
(:::) :: x:a -> xs:List a
-> {v:List a | length v = 1 + length xs}
Hence, we can write Set-valued measures
Using the Data.Set
API for convenience
import qualified Data.Set as S
List
s Elementsinline
lets us reuse Haskell terms in refinements.
Strengthens type of data constructor
data List a where
Emp :: {v:List a | length v == 0
&& elems v == S.empty}
(:::) :: x:a -> xs:List a
-> {v:List a | length v == 1 + length xs
&& elems v == addElem v xs }
Can we specify sortedness?
Make illegal states unrepresentable
Lets define a type for ordered lists
Lets refine the type to enforce order
Head oHd
is smaller than every value v
in tail oTl
Illegal values unrepresentable
Q: Oops. There's a problem! Can you fix it?
Limited to decidable logics but ...
Offer massive amounts of automation
Compare with insertionSort
in:
Problem: How to reason about elems
and lenght
of an OList
?
Solution: Make OList
an instance of List
using Abstract Refinements!
Next: Abstract Refinements