Uses of Package
escjava.prover

Packages that use escjava.prover

escjava
escjava.prover
escjava.translate

Classes in escjava.prover used by escjava

Cvc3

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

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

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
SLists represent possibly-empty lists of SExps.