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