Uploaded at Nov 12 16:44:51 2023 (UTC)

Curry Package dsdcurry

DSDCurry: A tool for Declarative Software Development

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:

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

  • 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 :: ...... f = unknown

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

Download

Checkout with CPM:
cypm checkout dsdcurry 1.0.0
Package source:
dsdcurry-1.0.0.tar.gz [browse]
Source repository:
https://github.com/curry-packages/dsdcurry.git