Bounded Specs
Bounded Specs: Concepts, Issues, and Designs
In bounded specs constraints are placed on the constructors. For example,
in size bound specs, size constraints are placed on the empty and/or the
update constructor. For total maps or arrays, the constraint is on the
empty constructor: only arrays of bounded size can be allocated.
For partial maps, the constraint is on the update (shadow) constructor:
once the size reaches the bound, update just returns its map arg.
In each case, the bounded objects (size equal to K or size leq F)K should be
considered a subsort of objects (for objects = Partial-Maps, Arrays, Sets, etc).
A general theory that contains the union of the subsorts can be specified
by pairing objects and bounds.(Actually, via fibrations.) For example, the general
theory of the union of K-bounded Partial-Maps is obtained as a subsort of
(Map, Bound) via the subsort predicate
unk-bounded? where
(iff (unk-bounded? M B) (leq (size M) B))
In both cases, for each K, the general theory can be specialized via subsorting
to obtain the subsort bounded objects of size K. For
example, the general theory (i.e., the union theory) for bounded Partial-Maps
can be subsorted to: K-bounded Partial-Maps (i.e., single fixed K);
"unbounded" Partial-Maps (bound is actually omega--hence, any finite size is
ok); union K-bounded Partial-Maps for K leq some fixed K0; etc.
- Simple Bounds Theory
-
Basically a place holder in the current version: Bounds = Nat
Bounds spec is in:
bounds.re
- Bounded Arrays: ARRAY-K
-
In the case of Arrays (and total maps), the size and the bound coincide:
each array hase size K. See the specs in
array-k.re and
bitvector-k.re .
Note that the general theory is the standard ARRAY spec; i.e., Arrays of
all finite sizes. The domain of an Array is an initial segment of the Nats
(i.e., a finite ordinal). It is really this domain that is being constrained:
it is expressed in terms of the size of the Array, but that is equivalent to
a constraint on the domain.
Somewhat more generally, Arrays can be formulated over (products of) ordinals.
- Bounded Containers (Bags, Sets, Seqs)
-
Essentially bounded partial objects similar to bounded partial maps:
all sets etc whose size is leq K.
Use the empty, insert constructors and define join only
when both args are in the same subsort.
- Bounded Partial Maps
-
k-bounded-partial-map-axm.re
k-bounded-partial-map-def.re
unk-bounded-partial-maps.re
SpecWeb Index
Specs