Combining Testing and Verification
==================================
This directory contains some examples demonstrating the
combination of testing and verification.
If there are is a property `p` in a program `m` for which
a proof exists, i.e., a file named `proof-m-p` (the name
is case independent), then:
1. Property `p` is not checked by CurryCheck
2. The property is translated into a simplification rule
in order to simplify other postconditions before checking them.
-------------------------------------------------------------------------
Example for applying the available Curry tools
----------------------------------------------
Consider the program `ListProp.curry` which contains a postcondition
for the list concatenation. The postcondition ensures that the length
of the concatenated list is the sum of the lengths of the input lists:
append'post xs ys zs = length xs + length ys == length zs
We can statically simplify this postcondition by proving it.
To do so, we first formulate it as a property:
appendAddLengths xs ys = length xs + length ys -=- length (append xs ys)
To get some confidence in its general correctness, we test it:
> curry-check ListProp
...
Executing all tests...
appendAddLengths_ON_BASETYPE (module ListProp, line 14):
OK, passed 100 tests.
appendSatisfiesPostCondition_ON_BASETYPE (module ListProp, line 7):
OK, passed 100 tests.
Since everything looks fine, we try to prove it with Agda.
For this purpose, we translate the property and all involved
functions into an Agda program:
> curry2verify ListProp
...
Agda module 'TO-PROVE-appendAddLengths.agda' written.
...
Now, we complete the Agda program `TO-PROVE-appendAddLengths.agda`
by a straightforward induction on the first argument of `appendAddLengths`.
Since the proof is complete, we rename the Agda module into
`PROOF-ListProp-appendAddLengths.agda`.
To see the effect of this proof for program testing, we run CurryCheck again:
> curry-check ListProp
Analyzing module 'ListProp'...
>
Hence, CurryCheck does not perform any test since the property
`appendAddLengths` has been proved and this theorem is used to
simplify the postcondition to `True` so that it trivially holds.
This simplification process can be visualized with option `-v`:
> curry-check ListProp -v2
Analyzing module 'ListProp'...
...
POSTCONDITION: append'post(a, b, c) → ==(+(length(a), length(b)), length(c))
...
SIMPPOSTCOND: append'post(a, b, c) → True
>
-------------------------------------------------------------------------