DSDCurry: Declarative Software Development with Curry (Version 2010) |
|||||||||
|
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] 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 _ = successand the postcondition sort'post :: [Int] -> [Int] -> Success sort'post x y = (y =:= permute x) & sorted y
The postcondition states that the result of the operation 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 > 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 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]However, a further test shows a non-intended behavior: 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)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.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 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. More detailed information can be found in the following paper.
|