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