DSDCurry: Declarative Software Development with Curry |
|||||||||||
|
DescriptionDSDCurry 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:
Example
Consider you need an operation 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 _ = successIn 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 ysA 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 > dsdcurry sort
and obtain a new module > 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 :: [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... DownloadThe 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 DocumentationSorry, 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.
|