-- Example for a Curry program with contracts (pre/postcondition):
-- sum up all numbers from 0 to n

-- Precondition: the argument is not negative
sum'pre :: Int -> Bool
sum'pre n = n>=0

-- Postcondition: the result satisfies the Gauss sum formula
sum'post :: Int -> Int -> Bool
sum'post n f = f == n * (n+1) `div` 2

sum :: Int -> Int
sum n = if n==0 then 0 else n + sum (n-1)

main1 :: Int
main1 = sum 100

-- The contract prover for such programs can be installed by
--
--     > cypm install contract-prover
--
-- If `~/.cpm/bin` is in the path, the contracts in this program
-- can be verified (provided that the SMT solver Z3 is installed) by
--
--     > curry-contracts Sum
-- 
-- Hence, the contract prover actually verified the
-- (partial) correctness of `sum`.