ESC/Java2
© 2003,2004,2005 David Cok and Joseph Kiniry
© 2005 UCD Dublin
© 2003,2004 Radboud University Nijmegen
© 1999,2000 Compaq Computer Corporation
© 1997,1998,1999 Digital Equipment Corporation
All Rights Reserved

escjava.prover
Class Simplify

java.lang.Object
  extended byescjava.prover.Simplify

public class Simplify
extends java.lang.Object

The interface to the Simplify theorem prover program using Strings to send and S-expressions to receive.

Note that a Java application will not exit normally (i.e., when its main() method returns) until all subprocesses have finished. In particular, this implies that all Simplify instances must be closed before this can occur. Alternatively, a Java application can just call java.lang.System.exit to force an exit to occur without waiting for subprocesses.

Warning: This class uses SubProcess.readSExp(), which does not implement the full grammer for SExps. See that routine for the exact limitations.

See Also:
SExp, SubProcess, CECEnum

Field Summary
private  SubProcess P
          Our Simplify subprocess; no actions should be taken on this subprocess unless readySubProcess() is called first.
private  CECEnum subProcessUser
          This variable holds the CECEnum that is currently using Simplify (there can be at most 1 such CECEnum), or null if there is no such CECEnum.
 
Constructor Summary
Simplify()
          Create a new invocation of Simplify as a sub-process.
 
Method Summary
 void close()
          Close us.
private  void eatPrompt()
          Consume the prompt from our Simplify subprocess.
(package private) static void exhaust(java.util.Enumeration n)
          Force an Enumeration to compute all of its elements
static void main(java.lang.String[] args)
          A simple test routine
 java.util.Enumeration prove(java.lang.String exp)
          Attempt to verify expression exp.
private  void readySubProcess()
          Prepare Simplify for use.
 void sendCommand(java.lang.String s)
          Send a single String command to Simplify.
 void sendCommands(java.lang.String s)
          Send a String containing zero-or-more commands to our Simplify subprocess.
 void startProve()
          Readies the simplify subprocess and sets its user to this, but send no commands.
 java.util.Enumeration streamProve()
           
 java.io.PrintStream subProcessToStream()
           
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

P

private final SubProcess P
Our Simplify subprocess; no actions should be taken on this subprocess unless readySubProcess() is called first.


subProcessUser

private CECEnum subProcessUser
This variable holds the CECEnum that is currently using Simplify (there can be at most 1 such CECEnum), or null if there is no such CECEnum.

Simplify is available for use iff this is null. Use readySubProcess() to make Simplify available.

Constructor Detail

Simplify

public Simplify()
Create a new invocation of Simplify as a sub-process.

The resulting invocation is initially open, but may be closed permanently with the close() method.

This constructor may result in a fatal error if any problems occur.

Method Detail

readySubProcess

private void readySubProcess()
Prepare Simplify for use.

Precondition: we are not closed.

Ensures any CECEnum currently using Simplify finishes.


close

public void close()
Close us.

This destroys the associated subprocess. Afterwards, none of our methods should ever be called again. Likewise, no methods of any Enumeration we've returned should ever be called again.

This method may result in a fatal error if any problems occur. Our subprocess is guaranteed to be destroyed afterwards, regardless of which exit is taken.


sendCommand

public void sendCommand(java.lang.String s)
Send a single String command to Simplify.

A command is something that produces no output other than whitespace and a prompt. If any other output is produced, a fatal error will result.

Precondition: we are not closed.

Parameters:
s - the string containing the command to be sent to simplify.

sendCommands

public void sendCommands(java.lang.String s)
Send a String containing zero-or-more commands to our Simplify subprocess.

A command is something that produces no output other than whitespace and a prompt. If any other output is produced, a fatal error will result.

Precondition: we are not closed.

Parameters:
s - the string containing the commands to be sent to simplify.

prove

public java.util.Enumeration prove(java.lang.String exp)
Attempt to verify expression exp.

We always return an Enumeration of non-null SimplifyOutputs. If verifying exp succeeds, the resulting Enumeration will end with a SimplifyOutput of kind SimplifyOutput.VALID.

Precondition: we are not closed, and exp is properly formed according to Simplify's rules.


startProve

public void startProve()
Readies the simplify subprocess and sets its user to this, but send no commands.


streamProve

public java.util.Enumeration streamProve()

subProcessToStream

public java.io.PrintStream subProcessToStream()

eatPrompt

private void eatPrompt()
Consume the prompt from our Simplify subprocess. If the next output characters are not exactly the prompt (possibly preceeded by some whitespace), a fatal error is reported.

Precondition: we are not closed.


main

public static void main(java.lang.String[] args)
                 throws java.io.IOException
A simple test routine

Throws:
java.io.IOException

exhaust

static void exhaust(java.util.Enumeration n)
Force an Enumeration to compute all of its elements


ESC/Java2
© 2003,2004,2005 David Cok and Joseph Kiniry
© 2005 UCD Dublin
© 2003,2004 Radboud University Nijmegen
© 1999,2000 Compaq Computer Corporation
© 1997,1998,1999 Digital Equipment Corporation
All Rights Reserved

The ESC/Java2 Project Homepage