--------------------------------------------------------------------- -- Haskell: The Craft of Functional Programming -- Simon Thompson -- (c) Addison-Wesley, 1999. -- -- Chapter 8 --------------------------------------------------------------------- -- Reasoning about programs -- ^^^^^^^^^^^^^^^^^^^^^^^^ module Chapter8 where import Prelude hiding (sum,length,(++),reverse,unzip) -- Testing and verification -- ^^^^^^^^^^^^^^^^^^^^^^^^ -- A function supposed to give the maximum of three (integer) values. mysteryMax :: Int -> Int -> Int -> Int mysteryMax x y z | x > y && x > z = x | y > x && y > z = y | otherwise = z -- Definedness and termination -- ^^^^^^^^^^^^^^^^^^^^^^^^^^^ -- A factorial function, giving an undefined result on negative integers. fact :: Int -> Int fact n | n==0 = 1 | otherwise = n * fact (n-1) -- An infinite list posInts :: [Int] posInts = [1, 2 .. ] -- Induction -- ^^^^^^^^^ -- The sum function, defined recursively. sum :: [Int] -> Int sum [] = 0 -- (sum.1) sum (x:xs) = x + sum xs -- (sum.2) -- Double every element of an integer list. doubleAll :: [Int] -> [Int] doubleAll [] = [] -- (doubleAll.1) doubleAll (z:zs) = 2*z : doubleAll zs -- (doubleAll.2) -- The property linking the two: -- sum (doubleAll xs) = 2 * sum xs -- (sum+dblAll) -- Other functions used in the examples -- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -- The definitions given here use explicit recursion, rather than applying -- higher-order functions as may happen in the Prelude definitions. length :: [a] -> Int length [] = 0 -- (length.1) length (z:zs) = 1 + length zs -- (length.2) (++) :: [a] -> [a] -> [a] [] ++ zs = zs -- (++.1) (w:ws) ++ zs = w:(ws++zs) -- (++.2) reverse :: [a] -> [a] reverse [] = [] -- (reverse.1) reverse (z:zs) = reverse zs ++ [z] -- (reverse.2) unzip :: [(a,b)] -> ([a],[b]) unzip [] = ([],[]) unzip ((x,y):ps) = (x:xs,y:ys) where (xs,ys) = unzip ps -- Generalizing the proof goal -- ^^^^^^^^^^^^^^^^^^^^^^^^^^^ -- The shunting function shunt :: [a] -> [a] -> [a] shunt [] ys = ys -- (shunt.1) shunt (x:xs) ys = shunt xs (x:ys) -- (shunt.2) rev :: [a] -> [a] rev xs = shunt xs [] -- (rev.1) -- An alternative definition of the factorial function. fac2 :: Int -> Int fac2 n = facAux n 1 facAux :: Int -> Int -> Int facAux 0 p = p facAux n p = facAux (n-1) (n*p)