Guarantee Functions are Total
LH warns you that
head is not total as it
is missing the case for [] and checks that
it is total on NonEmpty lists.
(more...)
The input contract propagates to uses of
head
which are verified by ensuring the arguments are
NonEmpty.
Keep Pointers Within Bounds
LH lets you avoid off-by-one errors that can lead to crashes
or buffer overflows. (more...)
Dependent contracts let you specify, e.g. that
dotProduct requires equal-sized vectors.
Avoid Infinite Loops
LH checks that functions terminate and so
warns about the infinite recursion due to the missing
case in
fib. (more...)
Metrics let you check that recursive functions
over complex data types terminate.
Enforce Correctness Properties
Write correctness requirements, for example a list is ordered,
as refinements. LH makes illegal values be unrepresentable.
(more...)
LH automatically points out logic bugs, and proves
that functions return correct outputs
for all inputs.
Prove Laws by Writing Code
Specify laws, e.g. that the append
function
++ is associative,
as Haskell functions.
Verify laws via equational proofs that are plain Haskell
functions. Induction is simply recursion, and case-splitting is
just pattern-matching. (more...)