Commit 9affe40c authored by Michael Hanus 's avatar Michael Hanus
Browse files

Examples added and better commented

parent b8c04f91
--- This module contains some specifications of operations from the List
--- module.
--- Since the preprocessor also depends on the list module,
--- Since the Curry preprocessor also depends on the list module,
--- we cannot write these specifications directly into the list module.
---
--- To test it, execute
---
--- > curry-check -e ground ListSpecifications
---
--- Note that the option `-e ground` is only necessary for PAKCS
--- since PAKCS has an incomplete implementation of set functions
--- which results in an intended behavior of default rules.
--- For instance,
---
--- > isPrefixOf ([]::[Int]) failed --> True
--- > isPrefixOf'spec ([]::[Int]) failed --> no value
---
--- whereas both yields in `True` in KiCS2.
{-# OPTIONS_CYMAKE -F --pgmF=currypp --optF=defaultrules #-}
......
--- Example stating the equivalence of an iterative implementation
--- of the factorial function and its recursive specification.
import Test.Prop
---
--- To test it:
---
--- > curry-check Fac
-- Recursive definition of factorial.
-- Requires precondition to avoid infinite loops.
fac'spec :: Int -> Int
fac'spec n = if n==0 then 1 else n * fac (n-1)
fac'spec n = if n==0 then 1 else n * fac'spec (n-1)
fac'spec'pre :: Int -> Bool
fac'spec'pre n = n >= 0
......@@ -14,7 +16,7 @@ fac'spec'pre n = n >= 0
-- An iterative implementation of the factorial function.
-- Note that this implementation delivers 1 for negative numbers.
fac :: Int -> Int
fac n = fac' 1 1
fac n = faci 1 1
where
fac' m p = if m>n then p else fac' (m+1) (m*p)
faci m p = if m>n then p else faci (m+1) (m*p)
\ No newline at end of file
......@@ -3,12 +3,12 @@
import Test.Prop
-- Non-deterministic defined by overlapping rules:
-- Non-deterministic list insertion defined by overlapping rules:
ndinsert1 :: a -> [a] -> [a]
ndinsert1 x ys = x : ys
ndinsert1 x (y:ys) = y : ndinsert1 x ys
-- Non-deterministic defined by non-overlapping rules:
-- Non-deterministic list insertion defined by non-overlapping rules:
ndinsert2 :: a -> [a] -> [a]
ndinsert2 x [] = [x]
ndinsert2 x (y:ys) = x : y : ys ? y : ndinsert2 x ys
......
--- Example stating the correctness of selection sort
---
--- To test it:
---
--- > curry-check SelectionSort
-- Permutations:
perm :: [a] -> [a]
perm [] = []
perm (x:xs) = insert x (perm xs)
where insert x ys = x : ys
insert x (y:ys) = y : insert x ys
-- Is a list sorted?
sorted :: [Int] -> Bool
sorted [] = True
sorted [_] = True
sorted (x:y:ys) = x<=y && sorted (y:ys)
-- Sort specification via sorted permutations:
sort'spec :: [Int] -> [Int]
sort'spec xs | sorted ys = ys where ys = perm xs
-- Implementation of sort as straight selection sort:
sort :: [Int] -> [Int]
sort [] = []
sort (x:xs) = case minRest x [] xs of (m,r) -> m : sort r
-- Note that the following definition would not be correct:
--
-- sort (x:xs) = m : sort r where (m,r) = minRest x [] xs
--
-- This is due to the fact that it is less strict than the
-- specification, e.g., `null (sort (failed:failed))` would yield `False`
-- whereas the specification fails on this expression.
-- Implementations of minRest with a single list traversal:
minRest :: Int -> [Int] -> [Int] -> (Int,[Int])
minRest m rs [] = (m,rs)
minRest m rs (y:ys) = if m<=y then minRest m (y:rs) ys
else minRest y (m:rs) ys
......@@ -37,7 +37,7 @@
"modules": [ "ListProp", "SortSpec" ]
},
{ "src-dir": "examples/equivalent_operations",
"modules": [ "Fac", "SortISortEquiv" ]
"modules": [ "Fac", "SelectionSort", "SortISortEquiv" ]
}
],
"documentation": {
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment