|
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 |
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Objectescjava.prover.Simplify
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.
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 |
private final SubProcess P
readySubProcess()
is called first.
private CECEnum subProcessUser
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 |
public Simplify()
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 |
private void readySubProcess()
Precondition: we are not closed.
Ensures any CECEnum
currently using Simplify
finishes.
public void close()
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.
public void sendCommand(java.lang.String s)
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.
s
- the string containing the command to be sent to
simplify.public void sendCommands(java.lang.String s)
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.
s
- the string containing the commands to be sent to
simplify.public java.util.Enumeration prove(java.lang.String exp)
exp
.
We always return an Enumeration
of
non-null
SimplifyOutput
s. 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.
public void startProve()
public java.util.Enumeration streamProve()
public java.io.PrintStream subProcessToStream()
private void eatPrompt()
Precondition: we are not closed.
public static void main(java.lang.String[] args) throws java.io.IOException
java.io.IOException
static void exhaust(java.util.Enumeration n)
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 |
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |