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 with the tool `curry-verify`
(see Curry package
[verify](https://www-ps.informatik.uni-kiel.de/~cpm/pkgs/verify.html)):

    > curry-verify 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
    >

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