Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| 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

## escjava.prover
Class CECEnum

    java.lang.Object
      escjava.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()

Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| 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

The ESC/Java2 Project Homepage