Michael Hanus committed Mar 27, 2017 1 2 3 4 5 6 ``````Combining Testing and Verification ================================== This directory contains some examples demonstrating the combination of testing and verification. `````` Michael Hanus committed Oct 31, 2018 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 committed Mar 27, 2017 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: `````` Michael Hanus committed Oct 31, 2018 34 `````` > curry-check ListProp `````` Michael Hanus committed Mar 27, 2017 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. `````` Michael Hanus committed Oct 31, 2018 49 `````` ... `````` Michael Hanus committed Mar 27, 2017 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 `````` Michael Hanus committed Oct 31, 2018 55 ```````PROOF-ListProp-appendAddLengths.agda`. `````` Michael Hanus committed Mar 27, 2017 56 57 58 `````` To see the effect of this proof for program testing, we run CurryCheck again: `````` Michael Hanus committed Oct 31, 2018 59 `````` > curry-check ListProp `````` Michael Hanus committed Mar 27, 2017 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`: `````` Michael Hanus committed Oct 31, 2018 68 `````` > curry-check ListProp -v2 `````` Michael Hanus committed Mar 27, 2017 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 > -------------------------------------------------------------------------``````