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. */ >>> To Be Completed <<< OPERATIONS /* * Add an element to the collection, unless the collection is full. */ push (ee) = PRE ee : UNIVERSE & bagsize < maxsize THEN >>> To Be Completed <<< END ; /* * Get an element from the collection, and remove it, unless the * collection is empty. */ ee <-- pop = PRE (bag |>> {0}) /= {} & bagsize > 0 THEN >>> To Be Completed <<< END ; /* * Return a boolean telling whether the collection is empty or not. */ bb <-- empty = BEGIN bb := bool((bag |>> {0}) = {}) END END