DSDCurry: Declarative Software Development with Curry

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

  sort'post :: [Int] -> [Int] -> Bool
  sort'post xs ys = length xs == length ys

  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)

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

  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)

  > 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.14.0 or higher) installed in order to use this version of 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).

Contracts and Specifications for Functional Logic Programming

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