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