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