stack/abstract-stack/with-exceptions/with-assertions/stack.cs - An abstract class with preconditions and postconditions.

Lecture 13 - slide 26 : 32 Program 1

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