001 /* Copyright 2000, 2001, Compaq Computer Corporation */ 002 003 package escjava.prover; 004 005 import java.io.*; 006 import java.util.Enumeration; 007 008 import javafe.util.*; 009 010 /** 011 * <p> The interface to the Simplify theorem prover program using 012 * Strings to send and S-expressions to receive. </p> 013 * 014 * <p> Note that a Java application will not exit normally (i.e., when 015 * its <code>main()</code> method returns) until all subprocesses have 016 * finished. In particular, this implies that all 017 * <code>Simplify</code> instances must be closed before this can 018 * occur. Alternatively, a Java application can just call 019 * <code>java.lang.System.exit</code> to force an exit to occur 020 * without waiting for subprocesses. </p> 021 * 022 * 023 * <p> <strong>Warning:</strong> This class uses {@link 024 * SubProcess#readSExp()}, which does not implement the full grammer 025 * for SExps. See that routine for the exact limitations. </p> 026 * 027 * @see SExp 028 * @see SubProcess 029 * @see escjava.prover.CECEnum 030 */ 031 032 public class Simplify 033 { 034 /** 035 * Our Simplify subprocess; no actions should be taken on this 036 * subprocess unless {@link #readySubProcess()} is called first. 037 */ 038 //@ spec_public 039 private final /*@ non_null @*/ SubProcess P; 040 041 //@ invariant P == null ==> closed; 042 043 /** 044 * This variable holds the {@link CECEnum} that is currently using 045 * Simplify (there can be at most 1 such CECEnum), or 046 * <code>null</code> if there is no such CECEnum. 047 * 048 * <p> Simplify is available for use iff this is 049 * <code>null</code>. Use {@link #readySubProcess()} to make 050 * Simplify available. </p> 051 */ 052 //@ spec_public 053 private CECEnum subProcessUser = null; 054 055 //@ public model boolean closed; 056 //@ represents closed <- (P == null); 057 058 // Multiplexing Simplify 059 060 /** 061 * Prepare Simplify for use. 062 * 063 * <p> Precondition: we are not closed. </p> 064 * 065 * <p> Ensures any {@link CECEnum} currently using Simplify 066 * finishes. </p> 067 */ 068 //@ requires !closed; 069 //@ ensures subProcessUser != null ==> subProcessUser == null; 070 private void readySubProcess() { 071 if (subProcessUser != null) { 072 subProcessUser.finishUsingSimplify(); 073 eatPrompt(); 074 subProcessUser = null; 075 } 076 } 077 078 079 // Creation and destruction 080 081 /** 082 * Create a new invocation of Simplify as a sub-process. 083 * 084 * <p> The resulting invocation is initially open, but may be 085 * closed permanently with the {@link #close()} method. </p> 086 * 087 * <p> This constructor may result in a fatal error if any 088 * problems occur. </p> 089 */ 090 //@ ensures !closed; 091 public Simplify() { 092 P = new SubProcess("Simplify", 093 new String[] { 094 java.lang.System.getProperty("simplify", 095 "/usr/local/escjava/bin/Simplify"), 096 "-noprune", 097 "-noplunge"}, // FIXME - make controllable 098 null); 099 eatPrompt(); 100 } 101 102 /** 103 * Close us. 104 * 105 * <p> This destroys the associated subprocess. Afterwards, none 106 * of our methods should ever be called again. Likewise, no 107 * methods of any {@link Enumeration} we've returned should ever 108 * be called again. </p> 109 * 110 * <p> This method may result in a fatal error if any problems 111 * occur. Our subprocess is guaranteed to be destroyed afterwards, 112 * regardless of which exit is taken. </p> 113 */ 114 //@ ensures closed; 115 public void close() { 116 P.close(); 117 } 118 119 120 // Client operations 121 122 /** 123 * Send a single <code>String</code> command to Simplify. 124 * 125 * <p> A command is something that produces no output other than 126 * whitespace and a prompt. If any other output is produced, a 127 * fatal error will result. </p> 128 * 129 * <p> Precondition: we are not closed. </p> 130 * 131 * @param s the string containing the command to be sent to 132 * simplify. 133 */ 134 //@ requires !closed; 135 public void sendCommand(/*@ non_null @*/ String s) { 136 readySubProcess(); 137 P.resetInfo(); 138 139 if (Info.on) { 140 Info.out("[calling Simplify with command '" + s + "']"); 141 } 142 143 P.send(s); 144 145 eatPrompt(); 146 147 Info.out("[Simplify: command done]"); 148 } 149 150 151 /** 152 * Send a <code>String</code> containing zero-or-more commands to 153 * our Simplify subprocess. 154 * 155 * <p> A command is something that produces no output other than 156 * whitespace and a prompt. If any other output is produced, a 157 * fatal error will result. </p> 158 * 159 * <p> Precondition: we are not closed. </p> 160 * 161 * @param s the string containing the commands to be sent to 162 * simplify. 163 */ 164 //@ requires !closed; 165 public void sendCommands(/*@ non_null @*/ String s) { 166 readySubProcess(); 167 P.resetInfo(); 168 169 if (Info.on) { 170 Info.out("[calling Simplify with commands '" + s + "']"); 171 } 172 173 P.send(s); 174 175 // review kiniry 14 March 2004 - Why is this code block no 176 // longer necessary? 177 178 /* 179 // this is so we can be sure we have resynchronized the stream: 180 P.send(" (LBL |<resync>| (EQ |<A>| |<B>|))"); 181 182 // eat resulting prompts from s: 183 while (P.peekChar() == '>') 184 eatPrompt(); 185 186 // Eat output from synchronization expression: 187 Enumeration results = prove(""); 188 try { 189 while (true) { 190 if (!results.hasMoreElements()) { 191 // get into exception handling code below 192 throw new SExpTypeError(); 193 } 194 SimplifyOutput so = (SimplifyOutput)results.nextElement(); 195 if (so.getKind() == SimplifyOutput.COUNTEREXAMPLE) { 196 SimplifyResult sr = (SimplifyResult)so; 197 if (sr.labels.at(0).getAtom().toString().equals("<resync>")) { 198 // all is well (any remaining results will be eaten 199 // with the next call to readySubProcess) 200 break; 201 } 202 } 203 } 204 } catch (Exception e) { 205 P.handleUnexpected("to have seen the label <resync>"); 206 } 207 */ 208 209 Info.out("[Simplify: commands done]"); 210 } 211 212 /** 213 * Attempt to verify expression <code>exp</code>. 214 * 215 * <p> We always return an {@link Enumeration} of 216 * non-<code>null</code> {@link SimplifyOutput}s. If verifying 217 * <code>exp</code> succeeds, the resulting {@link Enumeration} 218 * will end with a {@link SimplifyOutput} of kind {@link 219 * SimplifyOutput#VALID}. </p> 220 * 221 * <p> Precondition: we are not closed, and <code>exp</code> is 222 * properly formed according to Simplify's rules. </p> 223 */ 224 //@ requires !closed; 225 //@ ensures \result.elementType == \type(SimplifyOutput); 226 //@ ensures !\result.returnsNull; 227 public /*@ non_null @*/ Enumeration prove(/*@ non_null @*/ String exp) { 228 readySubProcess(); 229 subProcessUser = new CECEnum(P, exp); 230 return subProcessUser; 231 } 232 233 /** 234 * Readies the simplify subprocess and sets its user to this, but 235 * send no commands. 236 */ 237 //@ normal_behavior 238 //@ modifies subProcessUser; 239 //@ ensures subProcessUser != null; 240 public void startProve() { 241 readySubProcess(); 242 subProcessUser = new CECEnum(P); 243 } 244 245 //@ ensures \result.elementType == \type(SimplifyOutput); 246 //@ ensures !\result.returnsNull; 247 public /*@ non_null @*/ Enumeration streamProve() { 248 P.ToStream().flush(); 249 while (P.peekChar() == '>') { 250 eatPrompt(); 251 } 252 return subProcessUser; 253 } 254 255 //@ ensures \result == null <==> closed; 256 public PrintStream subProcessToStream() { 257 return P.ToStream(); 258 } 259 260 261 // Utility routines 262 263 /** 264 * Consume the prompt from our Simplify subprocess. If the next 265 * output characters are not exactly the prompt (possibly preceeded 266 * by some whitespace), a fatal error is reported. 267 * 268 * <p> Precondition: we are not closed. </p> 269 */ 270 //@ requires !closed; 271 //@ requires P != null; 272 private void eatPrompt() { 273 P.eatWhitespace(); 274 P.checkChar('>'); 275 P.checkChar('\t'); 276 } 277 278 279 // Test methods 280 281 /** 282 * A simple test routine 283 */ 284 public static void main(String[] args) throws IOException { 285 Info.on = true; // Turn on verbose mode 286 287 Simplify S = new Simplify(); 288 289 exhaust(S.prove("(EQ A B)")); 290 291 exhaust(S.prove("(EQ A A)")); 292 293 S.sendCommand("(BG_PUSH (EQ B A))"); 294 exhaust(S.prove("(EQ A B)")); 295 S.sendCommand("(BG_POP)"); 296 297 exhaust(S.prove("(EQ A B)")); 298 299 S.sendCommands("(BG_PUSH (EQ B A)) (BG_POP)"); 300 301 // The following is not a command and thus should produce 302 // an error: 303 try { 304 S.sendCommand("(EQ A A)"); 305 } finally { 306 S.close(); 307 } 308 } 309 310 /** 311 * Force an {@link Enumeration} to compute all of its elements 312 */ 313 static void exhaust(/*@ non_null @*/ Enumeration n) { 314 while (n.hasMoreElements()) 315 n.nextElement(); 316 } 317 }