    001    /* Copyright 2000, 2001, Compaq Computer Corporation */
    002
    003    package escjava.prover;
    004
    005    import java.io.*;
    006
    007    /**
    008     * <code>SInt</code>s are S-expressions representing integers.
    009     */
    010
    011    /**
    012     * @design unknown author - The "public" below was added so that stuff
    013     * in the sexpgrep package can know about SInt (for the conversion
    014     * between the two kinds of s-expressions).
    015     */
    016
    017    final /* was package */ public class SInt extends SExp
    018    {
    019        /**
    020         * The <code>int</code> we represent.
    021         */
    022        private int value;
    023
    024        /**
    025         * Create a <code>SInt</code> representing a given
    026         * <code>int</code>.  Clients are allowed to create
    027         * <code>SInt</code>s only by calling <code>fromInt</code> so we
    028         * can choose later to intern if we wish.
    029         */
    030        //@ private normal_behavior
    031        //@   modifies value;
    032        //@   ensures value == i;
    033        private SInt(int i) {
    034            value = i;
    035        }
    036
    037        /**
    038         * Create a <code>SInt</code> representing a given
    039         * <code>int</code>.
    040         */
    041        static /*@ pure non_null @*/ SInt fromInt(int i) {
    042            return new SInt(i);
    043        }
    044
    045        /**
    046         * @return a flag indicating if we represent an integer, which is
    047         * always <code>true</code>.
    048         */
    049        //@ also
    050        //@ public normal_behavior
    051        //@   ensures \result;
    052        public /*@ pure @*/ boolean isInteger() {
    053            return true;
    054        }
    055
    056        /**
    057         * If we represent an integer, return it as an <code>int</code>;
    058         * otherwise, throw SExpTypeError.
    059         */
    060        //@ also
    061        //@ private normal_behavior
    062        //@   ensures \result == value;
    063        public /*@ pure @*/ int getInteger() {
    064            return value;
    065        }
    066
    067        /**
    068         * @return <code>true</code> iff parameter <code>o</code> is an
    069         * <code>SInt</code> with the same value as <code>this</code>.
    070         */
    071        public /*@ pure @*/ boolean equals(Object o) {
    072            if (!(o instanceof SInt)) return false;
    073            SInt a = (SInt)o;
    074            return this.value == a.value;
    075        }
    076
    077        /**
    078         * Print a textual representation of us on a given
    079         * <code>PrintStream</code>.
    080         *
    081         * <p> Note: This routine will take a <code>PrintWriter</code>
    082         * instead when we switch to a more recent version of JDK. </p>
    083         */
    084        public /*@ pure @*/ void print(/*@ non_null @*/ PrintStream out) {
    085            out.print(value);
    086        }
    087
    088        /**
    089         * Pretty-print a textual representation of us on a given
    090         * <code>PrintStream</code>.
    091         *
    092         * <p> Note: This routine will take a <code>PrintWriter</code>
    093         * instead when we switch to a more recent version of JDK. </p>
    094         */
    095        public /*@ pure @*/ void prettyPrint(/*@ non_null @*/ PrintStream out) {
    096            out.print(value);
    097        }
    098    }