1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
|
module StdSortListTest
/* Test module StdSortList
Voor werken met Gast:
(*) gebruik Environment 'Gast'
(*) zet Project Options op 'Basic Values Only' en '16M' Maximum Heap Size.
*/
import gast
import GenLexOrd
import StdSortList
Start = testn 10000
(\n` n2` m -> let n = lst2slst (cast [A,B,C] n` )
n2 = lst2slst (cast [A,B,C] n2`)
in
leeg_is_leeg /\
count_matches_elems n /\
is_sorted_elems n /\
member_is_member n m /\
member_na_insert n m /\
member_na_remove n m /\
insert_remove_invariant n m /\
minimum_property n /\
maximum_property n /\
merge_additive n n2 /\
merge_member n n2 m /\
True
)
:: Enum = A | B | C
derive bimap []
derive ggen Enum
derive genShow Enum
derive gEq Enum
derive gLexOrd Enum
instance == Enum where (==) x y = gEq{|*|} x y
instance < Enum where (<) x y = gEq{|*|} (gLexOrd{|*|} x y) LT
// clean should have something like this!
cast :: a a -> a
cast _ x = x
leeg_is_leeg :: Property
leeg_is_leeg
= name "leeg_is_leeg"
(count newSortList == 0)
count_matches_elems :: (SortList a) -> Property | Eq, Ord a
count_matches_elems n
= name "count_matches_elems"
(length (elements n) == count n)
is_sorted_elems :: (SortList a) -> Property | Eq, Ord a
is_sorted_elems n
= name "is_sorted_elems"
(isSorted (elements n))
where isSorted lst = and [ x<=y \\ x<-lst & y<-tl lst ]
member_is_member :: (SortList a) a -> Property | Eq, Ord a
member_is_member lst e
= name "member_is_member"
((isMember e (elements lst)) <==> (memberSort e lst))
member_na_insert :: (SortList a) a -> Property | Eq, Ord a
member_na_insert lst e
= name "member_na_insert"
(memberSort e (insertSort e lst))
member_na_remove :: (SortList a) a -> Property | Eq, Ord a
member_na_remove lst e
= name "member_na_remove"
(not (memberSort e (removeAll e lst)))
insert_remove_invariant :: (SortList a) a -> Property | Eq, Ord a
insert_remove_invariant lst e
= name "insert_remove_invariant"
(memberSort e lst <==> memberSort e lst`)
where lst` = removeFirst e (insertSort e lst)
minimum_property :: (SortList a) -> Property | Eq,Ord a
minimum_property n
= name "minimum_property"
(count n > 0 ==> (memberSort min n /\ all ((<=) min) (elements n)))
where min = minimum n
maximum_property :: (SortList a) -> Property | Eq,Ord a
maximum_property n
= name "maximum_property"
(count n > 0 ==> (memberSort max n /\ all ((>=) max) (elements n)))
where max = maximum n
merge_member :: (SortList a) (SortList a) a -> Property | Eq,Ord a
merge_member n m e
= name "merge_member"
(memberSort e nm <==> (memberSort e n \/ memberSort e m))
where nm = mergeSortList n m
merge_additive :: (SortList a) (SortList a) -> Property | Eq,Ord a
merge_additive n m
= name "merge_additive"
(count n + count m == count nm)
where nm = mergeSortList n m
lst2slst :: [a] -> SortList a | Eq,Ord a
lst2slst xs = seq (map insertSort xs) newSortList
|
