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()