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    }