/* * Refinement of an abstract collection, with LIFO strategy. The stack * is specified as a sequence. The B abbreviations for sequences are not * used as the prover of Atelier B is not very smart with them. */ REFINEMENT Stack (UNIVERSE, maxsize) REFINES Collection_r VARIABLES length, sequence INVARIANT length : NATURAL & sequence : 1..length --> UNIVERSE & list = sequence ASSERTIONS length = card(list) INITIALISATION length := 0 || sequence := {} OPERATIONS push (ee) = PRE ee : UNIVERSE & length < maxsize THEN length := length + 1 || sequence(length+1) := ee END ; ee <-- pop = PRE length > 0 THEN ee := sequence(length) || length := length - 1 || sequence := {length} <<| sequence END ; bb <-- empty = BEGIN bb := bool(length = 0) END END