abstract class Stack{ abstract public void push(Object el) require !full; ensure !empty && top() = el && size() = old size() + 1; abstract public void pop(); require !empty(); ensure !full() && size() = old size() - 1; abstract public Object top() require !empty(); abstract public boolean full() ensure "size() = capacitet"; abstract public boolean empty() ensure size() = 0; abstract public int size() ensure "result = number of elements on stack"; public void toggleTop(){ require size() >= 2; Object topEl1 = top(); pop(); Object topEl2 = top(); pop(); push(topEl1); push(topEl2); ensure size() = old size() && "top and element below top are exchanged"; } // toggleTop public String toString(){ return("Stack"); } }