using System;
public abstract class Stack{
abstract public void Push(Object el);
require !full;
ensure !empty && top() = el && size() = old size() + 1 &&
"all elements below el are unaffected";
abstract public void Pop();
require !empty();
ensure !full() && size() = old size() - 1 &&
"all elements remaining are unaffected";
abstract public Object Top
require !empty();
ensure nochange && Top = "the most recently pushed element"; {
get; }
abstract public bool Full
require true;
ensure nochange && Full = (size() = capacity); {
get; }
abstract public bool Empty
require true;
ensure nochange && Empty = (size() = 0); {
get;}
abstract public int Size
require true;
ensure nochange && Size = "number of elements on stack"; {
get;}
public void ToggleTop()
require size() >= 2; {
if (Size >= 2){
Object topEl1 = Top; Pop();
Object topEl2 = Top; Pop();
Push(topEl1); Push(topEl2);
}
ensure size() = old size() &&
"top and element below top have been exchanged" &&
"all other elements are unaffected";
}
public override String ToString(){
return("Stack");
}
} |