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    }