True
is a bad argument10
is a good argument0
average
take
fib
fib
is an uninterpreted function
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
N :: {v:List a | length v = 0}
C :: x:a -> xs:List a
-> {v:List a | length v = 1 + length xs}
Fear head
and tail
no more!
Q: Write types for head
and tail
that verify impossible
.
A convenient type alias
Partial Functions are automatically detected when totality
check is on!
average
Q: Write type for avg
that verifies safe division.
take
Use measures to specify take
Assuming the library Text
types...
... HeartBleed cannot happen!
What properties can be expressed in the logic?
Linear Arithmetic, Booleans, Uninterpreted Functions, ... (SMT logic)
Terminating Haskell functions.
Next: Termination
Next: Refinement Reflection