Set Specs

Sets: Concepts, Issues, and Designs

Set Specs

Basic Sets

The basic sets (no apply or size) are constructed from containers; see containers for the full construction
Two sorts: E (element) and Set (container).
Core operations are:
op empty-set : Set
op singleton : E -> Set
op union : Set, Set -> Set
Defined operations are:
op empty? : Set -> Boolean
op nonempty? : Set -> Boolean
op in : E, Set -> Boolean
op insert : E, Set -> Set

There are two constructor sets:
- empty, singleton, and union
- empty, insert

Sets

Sets import BASIC-SET and NAT. They add the operations: delete, size, subset, exists, forall, reduce, image, filter
See containers

SpecWeb Index

Specs