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