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 }