1
2
3
4
5
6
7
8
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
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
|
------------------------------------------------------------------------
A transformation tool to generate a Curry module with
assertion checking from pre/postconditions and specifications.
Sergio Antoy, Michael Hanus
August 12, 2016
------------------------------------------------------------------------
How to use the tool:
The tool is integrated into the Curry Preprocessor (currypp). Hence,
to activate the transformation, put the following line into the
beginning of your Curry module:
{-# OPTIONS_CYMAKE -F --pgmF=currypp --optF=contracts #-}
If postconditions or specifications are nondeterministic,
it is better that they will be evaluated via encapsulated search
(see Examples/NDAssertion.curry for a discussion).
For this purpose use the option "-e" as follows:
{-# OPTIONS_CYMAKE -F --pgmF=currypp --optF=contracts --optF=-e #-}
------------------------------------------------------------------------
Options:
The contract preprocessor accepts the following options:
-o : write the transformed Curry program into file <prog>.curry.CURRYPP
-e : encapsulate nondeterminism of assertions
-t : assert contracts only to top-level (but not to direct recursive) calls;
this might lead to a faster execution but less (incomplete!)
contract checking
------------------------------------------------------------------------
Assumptions:
- Naming conventions: for an operation f,
* its precondition must have the name f'pre
* its postcondition must have the name f'post
* its specification must have the name f'spec (or f'specd if the
specification is deterministic which provides for stronger checking)
- Pre/postconditions or specifications are not required and could be
omitted. However, if they are present, there must also be a defined
operation to which they refer.
- If there is a postcondition f'post but no precondition f'pre,
it is assumed that the precondition is defined as (const True).
- If there is a specification f'spec and an implementation of function f,
the specification will be used as a postcondition for f.
- Any pre- or postcondition for a function f will be added to the
implementation of f so that it will be checked at run-time.
- As a default, the complete computed value of a function will be
checked in a postcondition. Alternatively, one can also check
only some observed part of the computed result. For this purpose,
one can define a function f'post'observe that maps each computed
result into some observed part (see Examples/FibInfinite.curry
for an example of this use).
- Pre- and postconditions are always checked in a strict manner,
i.e., they might influence the evaluation of the original program.
In a future version, a lazy assertion checking might be supported.
------------------------------------------------------------------------
Examples:
See programs in the directory Examples
------------------------------------------------------------------------
Known problems:
- Strict assertions make operations stricter, thus, changing the run-time
behavior.
------------------------------------------------------------------------
|
