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

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


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