001 /* Copyright 2000, 2001, Compaq Computer Corporation */ 002 003 package escjava.prover; 004 005 import java.io.*; 006 007 /** 008 * S-Expression datatype for use in interfacing to the ESC Theorem 009 * prover, Simplify. 010 * 011 * <p> Considered as a language, the grammer of s-expressions is as 012 * follows: 013 * <pre> 014 * SExp ::= Atom | int | SList 015 * SList ::= ( SExp* ) 016 * </pre> 017 * 018 * <p> That is, s-expressions consist of either an atom, an integer, 019 * or a possibly-empty list of s-expressions. <code>Atom</code>s are 020 * interned <code>String</code>s used to represent symbols. </p> 021 * 022 * <p> Methods are available to test whether an <code>SExp</code> is 023 * an <code>Atom</code>, an integer, or a list. If the "type" of an 024 * <code>SExp</code> is known, it can be converted into what it 025 * represents. If an attempt is made to convert an <code>SExp</code> 026 * to an incorrect "type", the checked exception 027 * <code>SExpTypeError<code> will be thrown. </p> 028 * 029 * <p> <code>SExp</code>s can be printed onto a 030 * <code>PrintStream</code>. </p> 031 * 032 * @see SExpTypeError 033 * @see Atom 034 * @see SList 035 */ 036 037 public abstract class SExp 038 { 039 // <code>SExp</code> may not be extended outside this package: 040 /* package */ SExp() {}; 041 042 /** 043 * Return an S-expression representing a given integer. 044 * 045 * <p> This is faster than using <code>fancyMake(new 046 * Integer(i))</code>. </p> 047 */ 048 public static /*@ pure non_null @*/ SExp make(int i) { 049 return SInt.fromInt(i); 050 } 051 052 /** 053 * Return an S-expression representing an integer (passed wrapped 054 * in an <code>Integer</code>), an atom (specified via a 055 * <code>String</code>), or an existing S-expression (this case 056 * leaves the argument unchanged). 057 */ 058 //@ public normal_behavior 059 //@ requires \typeof(o) <: \type(String) || \typeof(o) <: \type(Integer) || \typeof(o) <: \type(SExp); 060 //@ requires o != null; 061 //@ ensures \result != null; 062 //@ pure 063 public static SExp fancyMake(Object o) { 064 javafe.util.Assert.precondition(o != null); 065 if (o instanceof SExp) 066 return (SExp)o; 067 else if (o instanceof String) 068 return Atom.fromString((String)o); 069 else if (o instanceof Integer) 070 return SInt.fromInt(((Integer)o).intValue()); 071 else { 072 javafe.util.Assert.fail( 073 "Non-String/Integer/SExp passed to SExp.make"); 074 return null; // make compiler happy... 075 } 076 } 077 078 /** 079 * Do we represent an atom? 080 */ 081 //@ public normal_behavior 082 //@ ensures !\result; 083 public /*@ pure @*/ boolean isAtom() { 084 return false; 085 } 086 087 /** 088 * @return a flag indicating if we represent an integer. 089 */ 090 //@ public normal_behavior 091 //@ ensures !\result; 092 public /*@ pure @*/ boolean isInteger() { 093 return false; 094 } 095 096 /** 097 * Do we represent a list? 098 */ 099 //@ public normal_behavior 100 //@ ensures !\result; 101 public /*@ pure @*/ boolean isList() { 102 return false; 103 } 104 105 /** 106 * If we represent an atom, return it as an <code>Atom</code>; 107 * otherwise, throw {@link SExpTypeError}. 108 */ 109 //@ public exceptional_behavior 110 //@ signals (SExpTypeError) true; 111 public /*@ pure @*/ Atom getAtom() throws SExpTypeError { 112 throw new SExpTypeError(); 113 } 114 115 /** 116 * If we represent an integer, return it as an <code>int</code>; 117 * otherwise, throw an {@link SExpTypeError}. 118 */ 119 //@ public exceptional_behavior 120 //@ signals (SExpTypeError) true; 121 public /*@ pure @*/ int getInteger() throws SExpTypeError { 122 throw new SExpTypeError(); 123 } 124 125 /** 126 * If we represent a list, return it as an <code>SList</code>; 127 * otherwise, throw {@link SExpTypeError}. 128 */ 129 //@ public exceptional_behavior 130 //@ signals (SExpTypeError) true; 131 public /*@ pure @*/ SList getList() throws SExpTypeError { 132 throw new SExpTypeError(); 133 } 134 135 /** 136 * Print a textual representation of us on a given 137 * <code>PrintStream</code>. 138 * 139 * <p> Note: This routine will take a <code>PrintWriter</code> 140 * instead when we switch to a more recent version of JDK. </p> 141 */ 142 public abstract /*@ pure @*/ void print(/*@ non_null @*/ PrintStream out); 143 144 /** 145 * Print a textual representation of us on {@link System#out}. 146 * 147 * <p> (This is a convenience function.) </p> 148 */ 149 public /*@ pure @*/ void print() { 150 print(System.out); 151 } 152 153 /** 154 * Pretty-print a textual representation of us on a given 155 * <code>PrintStream</code>. 156 * 157 * <p> Note: This routine will take a <code>PrintWriter</code> 158 * instead when we switch to a more recent version of JDK. </p> 159 */ 160 public abstract /*@ pure @*/ void prettyPrint(/*@ non_null @*/ PrintStream out); 161 162 /** 163 * @return a textual representation of this s-expression. 164 */ 165 //@ also 166 //@ public normal_behavior 167 //@ ensures \result != null; 168 public /*@ pure @*/ String toString() { 169 ByteArrayOutputStream baos = new ByteArrayOutputStream(); 170 PrintStream ps = new PrintStream(baos); 171 print(ps); 172 String result = baos.toString(); 173 ps.close(); 174 return result; 175 } 176 177 /** 178 * A simple test routine 179 */ 180 public static void main(String[] args) throws SExpTypeError { 181 display(make(14)); 182 183 display(fancyMake("hello")); 184 display(fancyMake(new Integer(42))); 185 186 display(fancyMake(SList.make())); 187 display(fancyMake(SList.make("NOT", make(0)))); 188 display(fancyMake(SList.make("a", "b", "c", "d", "e"))); 189 190 191 System.out.println( 192 SList.make().equals( 193 SList.make())); 194 195 System.out.println( 196 SList.make("a", "b", "c", "d", "e").equals( 197 SList.make("a", "b", "c", "d", "3"))); 198 199 System.out.println( 200 SList.make("a", "b", "c", "d", "e").equals( 201 SList.make("a", "b", "c", "d", "f"))); 202 203 System.out.println( 204 SList.make("NOT", SExp.make(3)).equals( 205 SList.make("NOT", SExp.make(2)))); 206 207 208 System.out.println( 209 SList.make("NOT", SExp.make(3)).equals( 210 SList.make("NOT", SExp.make(3)))); 211 212 213 // Intentionally invoke a SExpTypeError... 214 System.out.println(); 215 System.out.println("Type error case:"); 216 make(14).getAtom(); 217 } 218 219 /** 220 * Display a <code>SExp</code> verbosely, using all its accessor 221 * methods. 222 * 223 * <p> This method is intended for test use. </p> 224 */ 225 //-@ pure 226 public static void display(/*@ non_null @*/ SExp x) throws SExpTypeError { 227 if (x.isAtom()) { 228 System.out.print("[Atom] "+x.getAtom().toString()); 229 } 230 if (x.isInteger()) { 231 System.out.print("[int] "+x.getInteger()); 232 } 233 if (x.isList()) { 234 SList l = x.getList(); 235 int n = l.length(); 236 System.out.print("[" + (l.isEmpty() ? "empty " : "") + 237 n + "-element SList] "); 238 for (int i=0; i<n; i++) { 239 if (i!=0) 240 System.out.print(" "); 241 System.out.print("@" + i + "="); 242 l.at(i).print(System.out); 243 } 244 } 245 246 System.out.print(" => "); 247 x.print(System.out); 248 System.out.println(); 249 } 250 }