DSDCurry: Declarative Software Development with Curry (Version 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 consists of a precondition describing the accepted inputs and a postcondition relating input values to their intended result values. The pre- and postconditions are constraints (i.e., of type Success).
• The pre- and postcondition of an operation f must have the names f'pre and f'post, respectively.
• Each function with a precondition should also have a postcondition.
• If there is a postcondition f'post but no definition of a function f, the postcondition will be used as a first implementation of f.
• If there is a postcondition f'post but no precondition f'pre, it is assumed that the precondition is defined as (const success).

Example

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

  sort :: [Int] -> [Int]

We start by writing a specification of this operation in the form a contract consisting of the trivial precondition

  sort'pre :: [Int] -> Success
  sort'pre _ = success

  sort'post :: [Int] -> [Int] -> Success
  sort'post x y = (y =:= permute x) & sorted y

The postcondition states that the result of the operation sort should be a permutation of its input and all elements are in ascending order. 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)=:=True & 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 pre- and postconditions are used as a first implementation:

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

  > dsdcurry sort

the pre- and postcondition are now added as run-time assertions 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]

  sortC> sort [5,1,2,6,5,3]
  ERROR: Postcondition of operation 'sort' failed!

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)

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

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(8) 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 dsdcurry2010.tar.gz
  > cd dsdcurry
  > make

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

A Transformation Tool for Functional Logic Program Development (WLP 2010)

This paper describes the basic ideas of declarative software development in Curry and the tool DSDCurry.