|
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.CECEnum
This class is used privately by Simplify to enumerate the list of counter-example contexts found by Simplify to a given verification condition.
If the enumeration ends with a SimplifyOutput of kind VALID, then Simplify verified the theorem.
This class will eventually be fairly lazy to allow error reporting as each error is found.
Warning: This class uses SubProcess.readSExp(), which does not implement the full grammer for SExps. See that routine for the exact limitations.
Field Summary | |
private SubProcess |
P
The Simplify subprocess. |
private java.util.Vector |
pending
The next results we are to return. |
private boolean |
simplifyDone
Is Simplify done processing our verification request? |
Constructor Summary | |
(package private) |
CECEnum(SubProcess simplify)
|
(package private) |
CECEnum(SubProcess simplify,
java.lang.String exp)
Create an Enumeration of the counter-example contexts for expression exp using Simplify process
simplify . |
Method Summary | |
(package private) void |
finishUsingSimplify()
Ensure that we are done using Simplify. |
boolean |
hasMoreElements()
Returns true iff any more elements exist in this enumeration. |
java.lang.Object |
nextElement()
Returns the next element of the enumeration. |
private void |
readFromSimplify()
Attempt to read another output (for example, a counter-example) from Simplify, then append it to pending . |
private SimplifyResult |
readResultMessage()
|
private SimplifyOutputSentinel |
readSentinel()
|
Methods inherited from class java.lang.Object |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Field Detail |
private final SubProcess P
private boolean simplifyDone
If so, all remaining results must be in pending
.
Otherwise, the remaining results are those in pending
followed by the results we have yet to read from Simplify.
private final java.util.Vector pending
Constructor Detail |
CECEnum(SubProcess simplify, java.lang.String exp)
exp
using Simplify process
simplify
.
We always return an Enumeration of non-null SimplifyOutput's.
If verifying exp
succeeds, the resulting Enumeration
will end with a SimplifyOutput of kind VALID.
Precondition: simplify
is not closed, and
exp
is properly formed according to
Simplify's rules.
Note: This routine should be called *only* from class Simplify.
CECEnum(SubProcess simplify)
Method Detail |
public final boolean hasMoreElements()
hasMoreElements
in interface java.util.Enumeration
public java.lang.Object nextElement()
nextElement
in interface java.util.Enumeration
void finishUsingSimplify()
private void readFromSimplify()
pending
.
private SimplifyOutputSentinel readSentinel()
private SimplifyResult readResultMessage()
|
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 |