Uses of Class
escjava.vcGeneration.TNode

Packages that use TNode

escjava.vcGeneration
escjava.vcGeneration.coq
escjava.vcGeneration.pvs
escjava.vcGeneration.sammy
escjava.vcGeneration.simplify
escjava.vcGeneration.xml

Uses of TNode in escjava.vcGeneration

Subclasses of TNode in escjava.vcGeneration

class	TAllocLE
class	TAllocLT
class	TAnyEQ
class	TAnyNE
class	TArrayFresh
class	TArrayLength
class	TArrayShapeMore
class	TArrayShapeOne
class	TAsElems
class	TAsField
class	TAsLockSet
class	TBoolAnd
class	TBoolean
class	TBoolEQ
class	TBoolImplies
class	TBoolNE
class	TBoolNot
(package private) class	TBoolOp
class	TBoolOr
class	TBoolRes
class	TCast
class	TChar
class	TDouble
class	TEClosedTime
class	TExist
class	TFClosedTime
class	TFloat
class	TFloatAdd
class	TFloatDiv
class	TFloatEQ
(package private) class	TFloatFun
class	TFloatGE
class	TFloatGT
class	TFloatLE
class	TFloatLT
class	TFloatMod
class	TFloatMul
class	TFloatNE
(package private) class	TFloatOp
class	TForAll
class	TFunction
class	TInt
class	TIntegralAdd
class	TIntegralDiv
class	TIntegralEQ
class	TIntegralGE
class	TIntegralGT
class	TIntegralLE
class	TIntegralLT
class	TIntegralMod
class	TIntegralMul
class	TIntegralNE
class	TIntegralSub
(package private) class	TIntFun
(package private) class	TIntOp
class	TIs
class	TIsAllocated
class	TIsNewArray
class	TLiteral
class	TLockLE
class	TLockLT
class	TMethodCall The class used to represent method calls for the new Vc gen tree.
class	TName
class	TNull
class	TRefEQ
class	TRefNE
(package private) class	TRefOp
class	TRoot
class	TSelect
class	TStore
class	TString
class	TSum
class	TTypeEQ
class	TTypeLE
class	TTypeNE
class	TTypeOf
(package private) class	TTypeOp
class	TUnset
(package private) class	TVariable

Fields in escjava.vcGeneration declared as TNode

private TNode

VcGenerator.newRootNode

Methods in escjava.vcGeneration that return TNode

TNode	TFunction.getChildAt(int index)
abstract TNode	ProverType.rewrite(TNode tree) This method allows an ESC/Java VC term to be simplified before it is translated to the target prover.

Methods in escjava.vcGeneration with parameters of type TNode

(package private) void	TFunction.addSon(TNode n)
abstract void	ProverType.getProof(java.io.Writer out, java.lang.String name, TNode term) This method allows a VC term (generated by using the visitor pattern), for example, to: be wrapped up as a prover assertion (eg. a lemma or theorem for the prover) universally quantify all free variables in the VC term
abstract TNode	ProverType.rewrite(TNode tree) This method allows an ESC/Java VC term to be simplified before it is translated to the target prover.
void	ProverType.generateDeclarations(java.io.Writer out, TNode term) This convenience method generates the declarations for a given term.
void	ProverType.generateTerm(java.io.Writer out, TNode term) This convenience method uses the visitor pattern to generate a prover specific term.

Uses of TNode in escjava.vcGeneration.coq

Methods in escjava.vcGeneration.coq that return TNode

TNode

CoqProver.rewrite(TNode tree) Tries to simplify the given tree using the class TProofTyperVisitor.

Methods in escjava.vcGeneration.coq with parameters of type TNode

void	TProofSimplifier.simplify(TBoolRes n, TNode m)
void	TProofSimplifier.simplify(TFunction n, TNode m, TNode o)
void	CoqProver.getProof(java.io.Writer out, java.lang.String proofName, TNode term)
TNode	CoqProver.rewrite(TNode tree) Tries to simplify the given tree using the class TProofTyperVisitor.

Uses of TNode in escjava.vcGeneration.pvs

Methods in escjava.vcGeneration.pvs that return TNode

TNode

PvsProver.rewrite(TNode tree) We expect this method to be called with a tree of type TBoolImplies: the hypothesis of the tree is expected to be typing information the conclusion of the tree is expected to be the VC body Since the Pvs prover is a strongly typed logic, we may eliminate this typing information before providing any additional simplifications.

Methods in escjava.vcGeneration.pvs with parameters of type TNode

void	TProofSimplifier.simplify(TBoolRes n, TNode m)
void	TProofSimplifier.simplify(TFunction n, TNode m, TNode o)
void	PvsProver.getProof(java.io.Writer out, java.lang.String proofName, TNode term)
TNode	PvsProver.rewrite(TNode tree) We expect this method to be called with a tree of type TBoolImplies: the hypothesis of the tree is expected to be typing information the conclusion of the tree is expected to be the VC body Since the Pvs prover is a strongly typed logic, we may eliminate this typing information before providing any additional simplifications.

Uses of TNode in escjava.vcGeneration.sammy

Methods in escjava.vcGeneration.sammy that return TNode

TNode

SammyProver.rewrite(TNode tree)

Methods in escjava.vcGeneration.sammy with parameters of type TNode

void	SammyProver.getProof(java.io.Writer out, java.lang.String proofName, TNode term)
TNode	SammyProver.rewrite(TNode tree)

Uses of TNode in escjava.vcGeneration.simplify

Methods in escjava.vcGeneration.simplify that return TNode

TNode

SimplifyProver.rewrite(TNode tree)

Methods in escjava.vcGeneration.simplify with parameters of type TNode

void	SimplifyProver.getProof(java.io.Writer out, java.lang.String proofName, TNode term)
TNode	SimplifyProver.rewrite(TNode tree)

Uses of TNode in escjava.vcGeneration.xml

Methods in escjava.vcGeneration.xml that return TNode

TNode

XmlProver.rewrite(TNode tree) All rewriting is handled by the prover based stylesheet, so we do nothing here.

Methods in escjava.vcGeneration.xml with parameters of type TNode

void	XmlProver.getProof(java.io.Writer out, java.lang.String proofName, TNode term) Here we ensure that the resulting XML term is suitable for writing to an output file.
TNode	XmlProver.rewrite(TNode tree) All rewriting is handled by the prover based stylesheet, so we do nothing here.