DSDCurry is a transformation tool which generates from a Curry module containing pre/postconditions and specifications of operations a new Curry module where assertions are added to check these pre/postconditions and specifications.
The ideas of this tool and declarative software development with specifications and pre/postconditions in Curry are described in this paper:
Sergio Antoy, Michael Hanus: Contracts and Specifications for Functional Logic Programming, Proc. of the 14th International Symposium on Practical Aspects of Declarative Languages (PADL 2012), Springer LNCS 7149, pp. 33-47, 2012
| How to use the tool: |
| After installing the tool with |
| > cpm install dsdcurry |
(which installs the binary dsdcurry in ~/.cpm/bin), you can use it as follows: |
If Mod.curry contains your Curry module with pre/postconditions, execute |
| > dsdcurry mod |
to generate new module ModC.curry where assertions are added. |
| Load the new module into PAKCS and run it by |
| > pakcs :load ModC |
| You can also transform and load the module into PAKCS in one step by |
| > dsdcurry -r Mod |
Assumptions:
f,f'pref'postits 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.
If there is a postcondition f'post but no precondition f'pre, it is assumed that the precondition is defined as
f'pre ... = True
If a function f is defined by
f :: ...
it will be considered as "to be implemented", i.e., an implementation will be generated from a specification or postcondition (see below). Providing such an "unknown" definition might be necessary in larger programs where one wants to apply a function without having its final implementation.
If there is a specification f'spec but no implementation of a function f, the specification will be used as a first implementation of f.
If there is a postcondition f'post but neither a specification f'spec nor an implementation of function f, the postcondition will be used (by narrowing) as an initial implementation for f. One can select via option "-pcs" whether only one or all values generated from the postcondition should be take for the implementation.
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.
Pre- and postconditions can be checked in a strict, lazy, or (lazy) enforecable manner (this can be specified by command-line arguments, see below).
| Command-line arguments: |
| Usage: dsdcurry [-s|-f|-l|-e|-pcs|-r|-d] |
| -s : generate strict assertions (default) -l : generate lazy assertions -f : generate lazy enforceable assertions -e : encapsulate nondeterminism of assertions (see examples/ndassertion.curry) -pcs : take single result of funcs generated from postconditions -r : load the transformed program into PAKCS -d : show assertion results during execution (with -r) |
Examples:
See programs in the directory examples
| Known problems: |
| - Sometimes the type signatures of the generated functions are too general if the type signature of pre/postconditions are more general than the type of the generated function that is required by the later use of the function. |
Solution: add restrictive type signature to pre/postconditions in your program or add a type signature for the function with a body f = unknown |
| - Strict assertions make operations stricter, thus, changing the run-time behavior. |
Solution: use lazy assertions (option -l), but this has the risk that some assertions will never be checked |
Better solution: use enforceable assertions (option -f), i.e., evaluate assertion lazily but enforce their evaluation at the end by evaluating the main expression e by enforce e (or enforceIO e if e is an I/O action). |