Class Example

class IntStack {  
    // Specification Fields:  
    // top = top element of the stack public: 
    IntStack(); 
      // ensures: initializes this to an empty stack 

    ~IntStack(); 
      // modifies: this 
      // ensures: this no longer exists; memory is deallocated 

    void push (int elem); 
      // modifies: this 
      // ensures: this = this@pre appended with elem; top == elem 

    void pop (); 
      // modifies: this 
      // ensures: if this@pre is empty, then this is empty 
      //          else this = this@pre with top removed 

    int top(); 
      // requires: this is not empty 
      // returns: top
}