Combining Testing and Verification
==================================

This directory contains some examples demonstrating the
combination of testing and verification.

If there is a property `p` in a module `M` for which
a proof exists, i.e., a file named `proof-M-p.abc` (the name
is case independent and the suffix and all non-alpha-numberic characters
in the file name are ignored), 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
    >

-------------------------------------------------------------------------