/* * Refinement of an abstract collection, with FIFO strategy. The queue * is specified as a sliding window. */ REFINEMENT Queue (UNIVERSE, maxsize) REFINES Collection_r VARIABLES start, end, window INVARIANT start : NATURAL & end : NATURAL & start <= end & window : start..(end-1) --> UNIVERSE & list = window ASSERTIONS end - start = card(list) INITIALISATION start := 0 || end := 0 || window := {} OPERATIONS push (ee) = PRE ee : UNIVERSE & (end - start) < maxsize THEN end := end + 1 || window(end) := ee END ; ee <-- pop = PRE start < end THEN ee := window(start) || start := start + 1 || window := {start} <<| window END ; bb <-- empty = BEGIN bb := bool(start = end) END END