/* * Intermediate refinement of bounded collection. The bag is refined by * a list of elements. This list is modeled as a partial function from * the set of natural numbers to the universe. */ REFINEMENT Collection_r (UNIVERSE, maxsize) REFINES Collection VARIABLES list INVARIANT list : NATURAL +-> UNIVERSE & dom(list) : FIN(NATURAL) & !ee . (ee : UNIVERSE => bag(ee) = card(list~[{ee}])) & bagsize = card(dom(list)) INITIALISATION list := {} OPERATIONS push (ee) = PRE ee : UNIVERSE & card(list) < maxsize THEN ANY nn WHERE nn : NATURAL & nn /: dom(list) THEN list(nn) := ee END END ; ee <-- pop = PRE list /= {} THEN ANY nn WHERE nn : NATURAL & nn : dom(list) THEN ee := list(nn) || list := {nn} <<| list END END ; bb <-- empty = BEGIN bb := bool(list = {}) END END