0
size
returns positive valuesavg
head
and tail
are Safefoldr1
average
map
init
init'
insert
List
s ElementsList
max
type (I)max
type (II)max
type (III)max
typekeys
Map
eval
create
unsafeTake
unpack
chop
Recall the simplest sorting algorithm:
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: specify & verify that output:
insert
Q: Can you fix the type of insert
so sort
checks?
Same size is all fine, how about same elements in output?
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.
Lets verify that sortE
returns the same set of elements:
Q: Can you fix the type for insertE
so sortE
verifies?
Yes, yes, but does sort
actually sort ?
How to specify ordered lists ?
Lets write a type for ordered pairs
Legal Values value of opX < opY
okPair = OP 2 4 -- legal
badPair = OP 4 2 -- illegal
Q: Can you refine the data type to legal values only?
Q: Can you refine Csv
so scores'
is rejected?
Refine the List
data type to enforce *ordering**!
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?
List
We just wrote two measures for List
length :: List a -> Nat
elems :: List a -> Set a
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 }
Limited to decidable logics but ...
Offer massive amounts of automation
Compare with insertionSort
in:
Unlike indexed types, measures ...
Decouple properties from data type
Reuse same data type with different invariants
How? Using Abstract Refinements