Smap

Choose the version you want to view.

Current version:Version message:

Program created.

Click on a tag to show all related programs.

recursion contract verification

Click on the badge to open the comment window for viewing and writing comments.

No comments yet.

Created by mh on September 4, 2020

0 users favorited this

Description: Show declarative programming, contracts, and possibilities for verification of Curry programs

Source code (Latest version):

-- Example discussion the declarative nature of Curry.

-- Curry is a declarative language, i.e., the value computed
-- for some expression is independent of the time and order
-- of evaluation. For instance, the following function
-- computes the sum of all integers up to a given number:
sum :: Int -> Int
sum n = if n==0 then 0
                else n + sum (n-1)

main = sum 100

-- The result does not depend on the order of the computation.
-- This simplifies the reasoning on programs.
-- Actually, we can state that the result always satisfies
-- the Gauss sum formula as a postcondition which relates
-- the argument `n` to the computed result `f` for any call to `sum`:
sum'post :: Int -> Int -> Bool
sum'post n f = f == n * (n+1) `div` 2

-- Of course, the input must be non-negative to avoid an infinite
-- recursion. This requirement could be stated as a precondition,
-- i.e., a predicate on the argument for any call to `sum`:
sum'pre :: Int -> Bool
sum'pre n = n>=0

-- There are automatic tools which exploit the declarative nature
-- of Curry. For instance, there is a tool for Curry ("contract checker")
-- which is able to verify that the postcondition above always
-- holds, i.e., our definition of sum is correct. For details, see
-- https://www-ps.informatik.uni-kiel.de/~cpm/pkgs/contract-prover.html
-- for the tool and the paper explaining the details behind this tool:
-- http://dx.doi.org/10.3233/FI-2020-1925

Options

Versions

1 version

Tags

3 tags

Comments

0 comments »

Declarative programming with contracts

implemented in Curry