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");
}
}
|