DSDCurry: Declarative Software Development with Curry

o  Documentation
o  Download
o  PAKCS
o  Curry
o  Old tool (2010)

Description

DSDCurry is a transformation tool to support the development of reliable declarative programs written in the multi-paradigm declarative language Curry. The current implementation of DSDCurry is a prototype to test this framework with respect to the Curry implementation PAKCS.

This development framework exploits the expressive power of functional logic programming to write specifcations as well as programs implementing them in the same language. Specifications written in Curry are executable. Thus, they can be used as an initial prototypical implementation of the program. When the specification is tested so that one is convinced that it specifies the intended problem correctly, one can implement a more efficient program, if necessary. In this case, the specification is used as an assertion that is being checked during execution of the program.

The DSDCurry transformation tool supports this development process by generating the auxiliary code in a module. For this purpose, DSDCurry is based on the following requirements:

  • A specification for an operation f has the name f'spec and the same type as the operation. Basically, it should be some comprehensible but not necessarily efficient formulation of the problem.
  • In addition to a specification, one can also provide a precondition describing the acceptable inputs and a postcondition relating input values to their intended result values. An additional postcondition could be reasonable to check some simpler properties that are logical consequences of a specification. The pre- and postconditions are Boolean operations and must have the names f'pre and f'post, respectively.
  • 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.
  • If there is a specification f'spec, it will be used as a postcondition for an implementation of 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. Violations, i.e., evaluations of a pre- or postcondition to False, will be reported.
  • Pre- and postconditions can be checked in a strict, lazy, or (lazy) enforecable manner. In addition, one can also add an observation function f'post'observe to check only some part of the result computed by f instead of the complete result. This could be reasonable for operations that compute infinite structures.

Example

Consider you need an operation sort to sort a list of integers, i.e., it should have the type

  sort :: [Int] -> [Int]

Since there are no further requirements on the input, the precondition is trivial (it could be also omitted):

  sort'pre :: [Int] -> Bool
  sort'pre _ = success
In the postcondition we require that the length of the input and output lists must be equal:
  sort'post :: [Int] -> [Int] -> Bool
  sort'post xs ys = length xs == length ys
A precise specification states that the result of the operation sort should be a permutation of its input and all elements are in ascending order:
  sort'spec :: [Int] -> [Int]
  sort'spec x | sorted ys = ys
    where ys = permute xs

The definition of permutations and ordered lists is a straightforward task in Curry:

  permute []     = []
  permute (x:xs) = ndinsert x (permute xs)
   where ndinsert x ys     = x : ys
         ndinsert x (y:ys) = y : ndinsert x ys

  sorted []       = success
  sorted [_]      = success
  sorted (x:y:ys) = x<=:y & sorted (y:ys)

If we put this code into a module sort.curry, we can transform it by the command

  > dsdcurry sort

and obtain a new module sortC.curry where the specification is used as a first implementation and the pre- and postconditions are added as assertions:

  > pakcs -l sortC
  ...
  sortC> sort [5,1,2,6,3]
  Result: [1,2,3,5,6]

Now we take our computer science education into account and remember the quicksort algorithm that is based on sorting separately the elements that are smaller and larger as some pivot element. We can implement this idea by adding the following definition to the module sort.curry:

  sort :: [Int] -> [Int]
  sort []     = []
  sort (x:xs) = sort (filter (<x) xs) ++ [x] ++ sort (filter (>x) xs)
If we transform this modified module again by
  > dsdcurry sort

the specification is transformed into a postcondition that is added as a run-time assertion to check the behavior of the implemented sort operation. The first test looks fine:

  > pakcs -l sortC
  ...
  sortC> sort [5,1,2,6,3]
  Result: [1,2,3,5,6]
However, a further test reveals a non-intended behavior:
  sortC> sort [5,1,2,6,5,3]
  Postcondition of operation 'sort' violated for:
  [5,1,2,6,5,3] -> [1,2,3,5,6]
  ERROR: Execution aborted due to contract violation!

After looking at (and maybe debugging) our implementation, we spot the error that we forget the elements equal to the pivot element. Thus, we change the definition to

  sort :: [Int] -> [Int]
  sort []     = []
  sort (x:xs) = sort (filter (<x) xs) ++ [x] ++ sort (filter (>=x) xs)
and transform and execute the resulting program again:
  > pakcs -l sortC
  ...
  sortC> sort [5,1,2,6,5,3]
  Result: [1,2,3,5,5,6]

When we are convinced by several tests that the implementation seems right, we can try to prove its correctness using the specification as a proof obligation. However, this is not supported by DSDCurry so that you have to use your brain...

Download

The implementation of DSDCurry is freely available. DSDCurry is implemented in Curry and uses various libraries available in the Curry implementation PAKCS. Thus, you should have PAKCS (Version 1.9.2(10) or higher) installed in order to use DSDCurry. The implementation is available as a gzipped tar file (see the README file in the distribution for further instructions how to install and use the system). After downloading, the following commands should be sufficient to install it:

  > tar xvzf dsdcurry.tar.gz
  > cd dsdcurry
  > make

This should install the executable dsdcurry provided that pakcs is in your path (otherwise, modify the Makefile).

Documentation

Sorry, apart from this web page and the README in the distribution, there is no separate user manual for DSDCurry. However, it is easy to use so that we hope you enjoy it. Some details about the ideas of this tool and its implementation can be found in the following (preliminary) paper.

Contracts and Specifications for Functional Logic Programming
This paper describes the basic ideas of declarative software development with Curry and the tool DSDCurry.

Michael Hanus
Fri Sep 16 09:54:59 CEST 2011

Valid XHTML 1.0 Transitional