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 CECEnum

java.lang.Object
  extended byescjava.prover.CECEnum
All Implemented Interfaces:
java.util.Enumeration

class CECEnum
extends java.lang.Object
implements java.util.Enumeration

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

P

private final SubProcess P
The Simplify subprocess.


simplifyDone

private boolean simplifyDone
Is Simplify done processing our verification request?

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.


pending

private final java.util.Vector pending
The next results we are to return.

Constructor Detail

CECEnum

CECEnum(SubProcess simplify,
        java.lang.String exp)
Create an Enumeration of the counter-example contexts for expression 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

CECEnum(SubProcess simplify)
Method Detail

hasMoreElements

public final boolean hasMoreElements()
Returns true iff any more elements exist in this enumeration.

Specified by:
hasMoreElements in interface java.util.Enumeration

nextElement

public java.lang.Object nextElement()
Returns the next element of the enumeration. Calls to this method will enumerate successive elements. Throws NoSuchElementException if no more elements are left.

Specified by:
nextElement in interface java.util.Enumeration

finishUsingSimplify

void finishUsingSimplify()
Ensure that we are done using Simplify. We promise not to ever use Simplify again after this routine returns.


readFromSimplify

private void readFromSimplify()
Attempt to read another output (for example, a counter-example) from Simplify, then append it to pending.


readSentinel

private SimplifyOutputSentinel readSentinel()

readResultMessage

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

The ESC/Java2 Project Homepage