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
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
|
set show timing off .
fmod SORTABLE-LIST-TEST is
inc SORTABLE-LIST{Nat<} .
var N : Nat .
var L : List{Nat<} .
op gen : Nat -> List{Nat<} .
eq gen(N) = gen2(N, nil) .
op gen2 : Nat List{Nat<} -> List{Nat<} .
eq gen2(0, L) = L .
eq gen2(s N, L) = gen2(N, ((s N * s N) rem 100) L) .
endfm
red size(gen(100)) .
red sort(gen(100)) .
red reverse(sort(gen(100))) .
red occurs(5, gen(100)) .
red occurs(24, gen(100)) .
fmod SET-TEST is
inc SET{Nat} .
var N M : Nat .
var A : Set{Nat} .
op gen : Nat Nat -> Set{Nat} .
eq gen(N, M) = gen2(N, M, empty) .
op gen2 : Nat Nat Set{Nat} -> Set{Nat} .
eq gen2(0, M, A) = A .
eq gen2(s N, M, A) = gen2(N, M, insert(s N * M, A)) .
endfm
red intersection(gen(100, 13), gen(100, 4)) .
red union(gen(100, 13), gen(100, 4)) .
red gen(100, 13) \ gen(100, 52) .
red intersection(gen(100, 13), gen(100, 4)) \ gen(100, 52) .
red | gen(100, 13) | .
red delete(3,(4,5,3)) .
red 53 in union(gen(100, 13), gen(100, 4)) .
red 52 in union(gen(100, 13), gen(100, 4)) .
fmod LIST-AND-SET-TEST is
inc LIST-AND-SET{Nat} .
var N : Nat .
var L : List{Nat} .
op gen : Nat -> List{Nat} .
eq gen(N) = gen2(N, nil) .
op gen2 : Nat List{Nat} -> List{Nat} .
eq gen2(0, L) = L .
eq gen2(s N, L) = gen2(N, ((s N * s N) rem 100) L) .
endfm
red gen(100) .
red makeSet(gen(100)) .
red filter(gen(100), makeSet(gen(10))) .
red filterOut(gen(100), makeSet(gen(10))) .
fmod SORTABLE-LIST-AND-SET-TEST is
inc SORTABLE-LIST-AND-SET{Nat<} .
var N : Nat .
var L : List{Nat<} .
op gen : Nat -> List{Nat<} .
eq gen(N) = gen2(N, nil) .
op gen2 : Nat List{Nat<} -> List{Nat<} .
eq gen2(0, L) = L .
eq gen2(s N, L) = gen2(N, ((s N * s N) rem 100) L) .
endfm
red makeList(makeSet(gen(100))) .
fmod LIST*-TEST is
inc LIST*{Nat} .
ops a b : -> List{Nat} .
eq a = [[1 2 3] [] [3 4 5 6]] .
eq b = [[[1] []] 2 [1 2 3]] .
endfm
red append(a, b) .
red size(append(a, b)) .
red reverse(append(a, b)) .
red head(a) .
red tail(a) .
red last(a) .
red front(a) .
red occurs([], a) .
red occurs([2 3], a) .
fmod SET*-TEST is
inc SET*{Nat} .
var N : Nat .
op zf : Nat -> Set{Nat} .
eq zf(0) = {} .
eq zf(s N) = union({zf(N)}, zf(N)) .
endfm
red zf(0) .
red zf(1) .
red zf(2) .
red zf(3) .
red zf(4) .
red | zf(10) | .
red | zf(100) | .
red 2^ zf(4) .
red | 2^ zf(9) | .
fmod MAP-TEST is
inc MAP{String, Nat} .
op a : -> Map{String, Nat} .
eq a = insert("three", 3, insert("two", 2, insert("one", 1, insert("zero", 0, empty)))) .
endfm
red a .
red a["one"] .
fmod ARRAY-TEST is
inc ARRAY{Nat, Nat0} .
var N : Nat .
op gen : Nat -> Array{Nat, Nat0} .
eq gen(0) = empty .
eq gen(s N) = insert(s N, s N rem 10, gen(N)) .
endfm
red gen(100) .
red gen(100)[55] .
red gen(100)[60] .
red gen(100)[1000000000000000000000] .
|
