/**
  Design by contract
  
  @see Software links
  @see Download these examples
**/

import java.util.*; 

/**
 * Design By Contract Exception.
 * This exception is thrown only when a contact
 * is violated.
 **/
class DBCException extends RuntimeException
{
  /**
   * @param msg Message to display in stack traces
   **/
  public DBCException(String msg)
  {
    super(msg);
  }
  public DBCException()
  {
    super("Contract violation");
  }
}

/**
 * This class provides several static methods that help
 * to directly implement Design by Contract
 **/
class DBC
{
  private static boolean asserting = false;
  public static void setAsserting(boolean asserting)
  {
    DBC.asserting = asserting;
  }
  public static void assert(boolean cond, String msg)
  {
    if(asserting && !cond)
    {
      throw new DBCException(msg);
    }
  }
  public static void assert(boolean cond)
  {
    assert(cond, "Assertion failed");
  }
  public static void pre(boolean cond, String msg)
  {
    assert(cond, msg);
  }
  public static void pre(boolean cond)
  {
    assert(cond, "Precondition violated");
  }
  public static void post(boolean cond, String msg)
  {
    assert(cond, msg);
  }
  public static void post(boolean cond)
  {
    assert(cond, "Postcondition violated");
  }
  public static void inv(boolean cond, Object obj, String msg)
  {
    if( asserting && !cond )
    {
      System.out.println("state=[" + obj + "]");
    }
    assert(cond, msg);
  }
  public static void inv(boolean cond, Object obj)
  {
    inv(cond, obj, "Invariant violated");
  }
  /**
   * verify that : 'thisImplies' implies 'that'
   * is a correct statement
   **/
  public static boolean implies(boolean thisImplies, boolean that)
  {
    return (thisImplies && that) || (!thisImplies);
  }
  /**
   * Return true if all elements in 'collection' is an instance of 'cls'
   **/
  public static boolean eachInstanceOf(Collection collection, Class cls)
  {
    if( collection == null )
      return false;
    Itertor iter == collection.iterator();
    while(iter.hasNext())
    {
      if( ! cls.isAssignableFrom(iter.next().getClass()) )
        return false;
    }
    return true;
  }
}

/**
 * This class represents a living person.
 *
 * @inv age > 0
 **/
class Person
{
  protected int age;
  
  /**
   * @pre age > 0
   **/
  public Person(int age)
  {
    DBC.pre(age > 0);
    this.age = age;
    invariant();
  }
  
  public int getAge()
  {
    return age;
  }

  protected synchronized void invariant()
  {
    DBC.inv(age > 0, this);
  }
  
  public String toString()
  {
    return "Person(age=" + age + ")";
  }
}

/**
 * This class represents a currently employed person
 *
 * @inv salary > 0
 **/
class Employee extends Person
{
  double salary;
  public Employee(int age, double salary)
  {
    super(age);
    this.salary = salary;
    thisInvariant();
  }
  
  protected synchronized void invariant()
  {
    super.invariant();
    thisInvariant();
  }

  private void thisInvariant()
  {
    DBC.inv(salary > 0, this);
  }
  
  /**
   * @pre salary > 0
   **/
  public void setSalary(double salary)
  {
    DBC.pre(salary > 0);
    this.salary = salary;
    invariant();
  }

  public double getSalary()
  {
    return salary;
  }

  public String toString()
  {
    return "Employee(age=" + age + ",salary=" + salary + ")";
  }
}

/** 
 * simple interface to a stack implemenation
 **/
interface Stack 
{ 
  /** 
   * @pre o != null 
   * @post !isEmpty() 
   * @post top() == o 
   */ 
  void push(Object o); 
 
  /** 
   * @pre !isEmpty()
   * @post result != null
   */ 
  Object pop(); 
 
  /** 
   * @pre !isEmpty()
   * @post result != null
   */ 
  Object top(); 
 
  boolean isEmpty();
}

/** 
 * @inv DBC.implies(isEmpty(), elements.size() == 0)
 */
class StackImpl implements Stack 
{
  protected Vector elements = new Vector();
  
  public StackImpl()
  {
    elements = new Vector();
    
    invariant();
  }
  
  protected synchronized void invariant()
  {
    DBC.inv(DBC.implies(isEmpty(), elements.size()==0), this);
  }
  
  public String toString()
  {
    return "Stack" + elements;
  }
 
  public void push(Object o) 
  {
    DBC.pre( o != null );
 
    elements.addElement(o);
 
    DBC.post( !isEmpty() );
    DBC.post( top() == o );
    invariant();
  } 
 
  public Object pop() 
  {
    DBC.pre(!isEmpty());
 
    Object result = top();
    elements.setSize(elements.size()-1);
    
    DBC.post(result != null);
    invariant();

    return result; 
  } 
 
  public Object top() 
  { 
    DBC.pre(!isEmpty());
    
    Object result = elements.elementAt(elements.size()-1);
    
    DBC.post(result != null);
    invariant();
    
    return result;
  } 
 
  public boolean isEmpty() 
  { 
    return elements.size() == 0; 
  } 
} 

public class Test
{
  public static void main(String[] args) 
  {
    DBC.setAsserting(false);
    test();
    DBC.setAsserting(true);
    test();
  }
  public static void test()
  { 
    try
    {
      Stack s = new StackImpl(); 
      s.push("one"); 
      s.pop(); 
    
      s.push("two"); 
      s.push("three"); 
    
      s.pop(); 
      s.pop(); 
      s.pop(); // causes an assertion to fail 
    }
    catch(Exception exc)
    {
      exc.printStackTrace();
    }
  }
}

/***********************************************************
output:

c:\dbc>java Test
java.lang.ArrayIndexOutOfBoundsException: -1 < 0
        at java/util/Vector.elementAt (Vector.java)
        at StackImpl.top (Test.java:269)
        at StackImpl.pop (Test.java:256)
        at Test.test (Test.java:308)
        at Test.main (Test.java:292)
DBCException: Precondition violated
        at DBC.assert (Test.java:67)
        at DBC.pre (Test.java:81)
        at StackImpl.pop (Test.java:256)
        at Test.test (Test.java:308)
        at Test.main (Test.java:294)
************************************************************/