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

-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