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

## Uses of Package
escjava.prover

Packages that use escjava.prover
escjava |
escjava.prover |
escjava.translate |

Classes in escjava.prover used by escjava
Sammy
Simplify The interface to the Simplify theorem prover program using Strings to send and S-expressions to receive.

Classes in escjava.prover used by escjava.prover
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
NewProver
ProverResponse
SExp S-Expression datatype for use in interfacing to the ESC Theorem prover, Simplify.
SExpTypeError This checked exception is used to signal a dynamic "type error" in the use of S-expressions.
Signature
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.
SubProcess.Died

Classes in escjava.prover used by escjava.translate
SExpTypeError This checked exception is used to signal a dynamic "type error" in the use of S-expressions.
SList `SList`s represent possibly-empty lists of `SExp`s.

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

The ESC/Java2 Project Homepage