/** * A simple implementation of the ADT Stack */ public class Stack implements Cloneable { /** * positions where to store next element */ protected int top = -1; /** * the internal storage */ protected Object[] storage; /** * create an empty Stack with capacity */ public Stack(int capacity) { /** require capacity > 0; **/ storage = new Object[capacity]; /** ensure [empty_after_creation] isEmpty(); **/ } /** * is the stack empty? */ public boolean isEmpty() { return top < 0; /** ensure changeonly{}; **/ } /** * is the stack full? */ public boolean isFull() { return top == storage.length - 1; /** ensure changeonly{}; **/ } /** * push a real (non-null) object to the stack */ public Stack push(Object o) { /** require [valid_object] o != null; [stack_not_full] !isFull(); **/ top++; storage[top] = o; return this; /** ensure changeonly{top,storage}; [nonempty_after_push] !isEmpty(); [push_increments_top] Old.top == top - 1; **/ } /** * take an object from the stack */ public Object pop() { /** require [stack_not_empty] !isEmpty(); **/ Object o = storage[top]; top--; return o; /** ensure changeonly{top}; [valid_object] Result != null; **/ } /** * does the stack contain the object */ public boolean contains(Object o) { /** require o != null; **/ int i = 0; while (i <= top && !storage[i].equals(o)) /** invariant 0 <= i && i <= top + 1; **/ /** variant top + 1 - i **/ { i++; } return i <= top; /** ensure changeonly{}; **/ } protected Object clone() { /* Use the Objects clone method. This is enough cause only top is refered with Old expressions. */ Object b = null; try { b = super.clone(); } catch (CloneNotSupportedException e){} return b; } /** invariant [range] -1 <= top && top < storage.length; [valid_content] storage.length == 0 || (forall i : {0 .. top} # storage[i] != null); [LIFO] isFull() || push("neco").pop().equals("neco"); **/ }