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

SpecWeb Index Specs