$11.5 PRECONDITIONS AND POSTCONDITIONS 339 indexing description:"Stacks:Dispenser structures with a Last-In,First-Out %access policy" class STACKI [G]feature Access count:INTEGER --Number of stack elements item:G is --Top element require not empty do end feature --Status report empty:BOOLEAN is -Is stack empty? do...end full:BOOLEAN is --Is stack representation full? do end feature--Element change put (x:G)is --Add x on top. require not full do ensure not empty item=x count old count +I end remove is --Remove top element. require not empry do ensure not full cout old count-I end end§11.5 PRECONDITIONS AND POSTCONDITIONS 339 indexing description: "Stacks: Dispenser structures with a Last-In, First-Out % %access policy" class STACK1 [G] feature -- Access count: INTEGER -- Number of stack elements item: G is -- Top element require not empty do … end feature -- Status report empty: BOOLEAN is -- Is stack empty? do … end full: BOOLEAN is -- Is stack representation full? do … end feature -- Element change put (x: G) is -- Add x on top. require not full do … ensure not empty item = x count = old count + 1 end remove is -- Remove top element. require not empty do … ensure not full count = old count – 1 end end