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

Package escjava.prover

Class Summary
Atom Atoms 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 SLists represent possibly-empty lists of SExps.
SNil The single SNil instance represents the empty list of SExps.
SPair A SPair is a pair of a SExp and a SList; together with the SNil class, it is used to implement lists of SExps.
SubProcess Instances of this class represent subprocesses.
TeeOutputStream This class is a FilterOutputStream class that forwards its given output to two given OutputStreams.
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

The ESC/Java2 Project Homepage