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 PACKAGE NEXT PACKAGE | FRAMES NO FRAMES

## Package escjava.prover

Class Summary
Atom | `Atom`s are S-expressions representing symbols.
CECEnum | This class is used privately by Simplify to enumerate the list of counter-example contexts found by Simplify to a given verification condition.
Formula |
Harvey |
HarveyResponse |
NewProver |
PPOutputStream | This class is a FilterOutputStream class designed for LISP-like input; it pretty prints the output by inserting spaces and newlines into the stream.
ProverResponse |
Sammy |
SammyResponse |
SExp | S-Expression datatype for use in interfacing to the ESC Theorem prover, Simplify.
Signature |
Simplify | The interface to the Simplify theorem prover program using Strings to send and S-expressions to receive.
SimplifyComment | An object of this class represent a progress comment produced by Simplify.
SimplifyOutput | Objects of this class represent possible normal outputs from Simplify.
SimplifyOutputSentinel | Objects of this class represent the summary part of the normal output from Simplify: valid, invalid, or unknown.
SimplifyResult | An object of this class represent a "result" produced by Simplify.
SInt |
SList | `SList`s represent possibly-empty lists of `SExp`s.
SNil | The single `SNil` instance represents the empty list of `SExp`s.
SPair | A `SPair` is a pair of a `SExp` and a `SList`; together with the `SNil` class, it is used to implement lists of `SExp`s.
SubProcess | Instances of this class represent subprocesses.
TeeOutputStream | This class is a `FilterOutputStream` class that forwards its given output to two given `OutputStream`s.
TriggerlessQuantWarning | An object of this class represent a "result" produced by Simplify.

Exception Summary
SExpTypeError | This checked exception is used to signal a dynamic "type error" in the use of S-expressions.
SubProcess.Died |

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 PACKAGE NEXT PACKAGE | FRAMES NO FRAMES

The ESC/Java2 Project Homepage