Container Specs

Containers: Concepts, Issues, and Designs

Container Specs

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