/* * Specification of an abstract collection, similar to what is found in * standard libraries of usual programming languages. * * The collection is required to remain bounded by the given parameter. * * Note: there is, in principle, no need for a new variable counting the * number of elements in the bag. This number is: * * SIGMA ee . (ee : UNIVERSE | bag(ee)) * * But the prover seems incapable of dealing with such sums. So a new * variable bagsize is introduced, and no correlation is expressed between * the bag's size and this variable. Still, it is easily seen (by a manual * analysis) that this variable is always equal to the bag's size. */ MACHINE Collection (UNIVERSE, maxsize) CONSTRAINTS maxsize : NAT1 VARIABLES bag, bagsize INVARIANT bag : UNIVERSE --> NATURAL & bagsize : NATURAL & bagsize <= maxsize /* * This equality should be left commented (for simplicity). But, * still, the variable bagsize must always satisfy: * * bagsize = SIGMA ee . (ee : UNIVERSE | bag(ee)) */ INITIALISATION /* * The collection is initially empty. */ bag := UNIVERSE * {0} || bagsize := 0 OPERATIONS /* * Add an element to the collection, unless the collection is full. */ push (ee) = PRE ee : UNIVERSE & bagsize < maxsize THEN bag(ee) := bag(ee) + 1 || bagsize := bagsize + 1 END ; /* * Get an element from the collection, and remove it, unless the * collection is empty. */ ee <-- pop = PRE (bag |>> {0}) /= {} & bagsize > 0 THEN ANY element WHERE element : UNIVERSE & bag(element) > 0 THEN ee := element || bag(element) := bag(element) - 1 || bagsize := bagsize - 1 END END ; /* * Return a boolean telling whether the collection is empty or not. */ bb <-- empty = BEGIN bb := bool((bag |>> {0}) = {}) END END