Container Specs
Containers: Concepts, Issues, and Designs
Container Specs
The following specs are included in the file:
simpler-containers.re
- CONTAINER
-
Two sorts: E (element) and C (container).
Core operations are:
op empty : C
op singleton : E -> C
op join : C, C -> C
Defined operations are:
op empty? : C -> Boolean
op nonempty? : C -> Boolean
op in : E, C -> Boolean
op insert : E, C -> C
There are two constructor sets:
- empty, singleton, and join
- empty, insert
- PROTO-SEQ
-
CONTAINER + empty, join form a monoid
- PROTO-BAG
-
PROTO-SEQ + join (bag-union) is commutative
- PROTO-SET
-
PROTO-BAG + join (union) is idempotent
- BASIC-SEQ
-
PROTO-SEQ + seq-equality-reduction axiom:
(iff (equal (concat (singleton x) S1) (concat (singleton y) S2))
(and (equal x y) (equal S1 S2)))
- BASIC-BAG
-
PROTO-BAG + bag-equality-reduction axiom:
(iff (equal (concat S S1) (concat S S2))
(equal S1 S2))
- BASIC-SET
-
is PROTO-SET
- SEQ
-
BASIC-SEQ + head, tail, and size
Defined-Dom, valid-index?, nth,
exists, forall, reduce, image, filter
- BAG
-
BASIC-BAG + occs (number of occurrences of x in B)
delete, subbag
- SET
-
BASIC-SET + delete, size subset
exists, forall, reduce, image, filter