README 2.57 KB
Newer Older
Michael Hanus 's avatar
Michael Hanus committed
1 2 3 4 5 6
Combining Testing and Verification
==================================

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

7 8
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
Michael Hanus 's avatar
Michael Hanus committed
9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33
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:

34
    > curry-check ListProp
Michael Hanus 's avatar
Michael Hanus committed
35 36 37 38 39 40 41 42 43 44 45 46 47 48
    ...
    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.
49
    ...
Michael Hanus 's avatar
Michael Hanus committed
50 51 52 53 54

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
55
`PROOF-ListProp-appendAddLengths.agda`.
Michael Hanus 's avatar
Michael Hanus committed
56 57 58

To see the effect of this proof for program testing, we run CurryCheck again:

59
    > curry-check ListProp
Michael Hanus 's avatar
Michael Hanus committed
60 61 62 63 64 65 66 67
    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`:

68
    > curry-check ListProp -v2
Michael Hanus 's avatar
Michael Hanus committed
69 70 71 72 73 74 75 76
    Analyzing module 'ListProp'...
    ...
    POSTCONDITION: append'post(a, b, c) → ==(+(length(a), length(b)), length(c))
    ...
    SIMPPOSTCOND:  append'post(a, b, c) → True
    >

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