--- Verification of average operation
--- The verification requires option `--contract`!

-- This simple definition contains a possible failure:
--
--      average xs = sum xs `div` length xs
--
-- This non-failing definition requires the postcondition of length, i.e.,
-- it can be verified as fail-free with option --contract|-c
average :: [Int] -> Int
average xs = if null xs then 0
                        else sum xs `div` length xs

-- From library `List`:
sum :: [Int] -> Int
sum = foldr (+) 0

-- From the prelude but with a postcondition:
length :: [a] -> Int
length []     = 0
length (_:xs) = 1 + length xs

length'post :: [a] -> Int -> Bool
length'post xs n = (null xs && n==0) || (not (null xs) && n>0)