    001    /* Copyright 2000, 2001, Compaq Computer Corporation */
    002
    003    package javafe.util;
    004
    005    /**
    006     * A class with static methods for checking assertions.
    007     * (Inspired by <cite>Mastering the AWT</code> by David Geary.)
    008     */
    009
    010    // FIXME - which of these can we get rid of as no longer used
    011    // FIXME - the notImplemented features in particular should be handled differently
    012    public class Assert {
    013      //@ ensures false;
    014      //@ signals_only AssertionFailureException;
    015      //@ pure
    016      static public void fail(String msg) {
    017        throw new AssertionFailureException(msg);
    018      } //@ nowarn Exception;
    019
    020      //@   requires b;
    021      //@   ensures true;
    022      //@   signals (Exception) false;
    023      //@ also
    024      //@   requires !b;
    025      //@   ensures false;
    026      //@   signals_only AssertionFailureException;
    027      //@ pure
    028      static public void notFalse(boolean b) {
    029        if (!b) throw new AssertionFailureException();
    030      }
    031
    032      //@   requires b;
    033      //@   ensures true;
    034      //@   signals (Exception) false;
    035      //@ also
    036      //@   requires !b;
    037      //@   ensures false;
    038      //@   signals_only AssertionFailureException;
    039      //@ pure
    040      static public void notFalse(boolean b, String msg) {
    041        if (!b) throw new AssertionFailureException(msg);
    042      }
    043
    044      //@   requires obj != null;
    045      //@   ensures true;
    046      //@   signals (Exception) false;
    047      //@ also
    048      //@   requires obj == null;
    049      //@   ensures false;
    050      //@   signals_only AssertionFailureException;
    051      //@ pure
    052      static public void notNull(Object obj) {
    053        if (obj == null) throw new AssertionFailureException();
    054      }
    055
    056      //@   requires obj != null;
    057      //@   ensures true;
    058      //@   signals (Exception) false;
    059      //@ also
    060      //@   requires obj == null;
    061      //@   ensures false;
    062      //@   signals_only AssertionFailureException;
    063      //@ pure
    064      static public void notNull(Object obj, String msg) {
    065        if (obj == null) throw new AssertionFailureException(msg);
    066      }
    067
    068      //@ ensures false;
    069      //@ signals_only AssertionFailureException;
    070      //@ pure
    071      static public void precondition() {
    072        throw new AssertionFailureException("Precondition violated!");
    073      } //@ nowarn Exception;
    074
    075      //@ ensures false;
    076      //@ signals_only AssertionFailureException;
    077      //@ pure
    078      static public void precondition(String msg) {
    079        throw new AssertionFailureException("Precondition violated: " + msg);
    080      } //@ nowarn Exception;
    081
    082      //@   requires b;
    083      //@   ensures true;
    084      //@   signals (Exception) false;
    085      //@ also
    086      //@   requires !b;
    087      //@   ensures false;
    088      //@   signals_only AssertionFailureException;
    089      //@ pure
    090      static public void precondition(boolean b) {
    091        if (!b) throw new AssertionFailureException("Precondition violated!");
    092      }
    093
    094      //@ ensures false;
    095      //@ signals_only NotImplementedException;
    096      static public void notImplemented() {
    097        throw new NotImplementedException("Hit an unimplemented feature");
    098      }
    099
    100      //@ ensures false;
    101      //@ signals_only NotImplementedException;
    102      static public void notImplemented(String s) {
    103        throw new NotImplementedException("Not implemented: " + s);
    104      }
    105    }