Uses of Class
escjava.vcGeneration.TVisitor

Packages that use TVisitor

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

Uses of TVisitor in escjava.vcGeneration

Subclasses of TVisitor in escjava.vcGeneration

(package private) class

TDotVisitor

Methods in escjava.vcGeneration that return TVisitor

protected abstract TVisitor

ProverType.visitor(java.io.Writer out) The visitor pattern is used to map an ESC/Java VC term to a prover term.

Methods in escjava.vcGeneration with parameters of type TVisitor

void	TUnset.accept(TVisitor v)
void	TTypeOf.accept(TVisitor v)
void	TTypeNE.accept(TVisitor v)
void	TTypeLE.accept(TVisitor v)
void	TTypeEQ.accept(TVisitor v)
void	TSum.accept(TVisitor v)
void	TString.accept(TVisitor v)
void	TStore.accept(TVisitor v)
void	TSelect.accept(TVisitor v)
void	TRoot.accept(TVisitor v)
void	TRefNE.accept(TVisitor v)
void	TRefEQ.accept(TVisitor v)
void	TNull.accept(TVisitor v)
abstract void	TNode.accept(TVisitor v)
void	TName.accept(TVisitor v)
void	TMethodCall.accept(TVisitor v)
void	TLockLT.accept(TVisitor v)
void	TLockLE.accept(TVisitor v)
void	TIsNewArray.accept(TVisitor v)
void	TIsAllocated.accept(TVisitor v)
void	TIs.accept(TVisitor v)
void	TIntegralSub.accept(TVisitor v)
void	TIntegralNE.accept(TVisitor v)
void	TIntegralMul.accept(TVisitor v)
void	TIntegralMod.accept(TVisitor v)
void	TIntegralLT.accept(TVisitor v)
void	TIntegralLE.accept(TVisitor v)
void	TIntegralGT.accept(TVisitor v)
void	TIntegralGE.accept(TVisitor v)
void	TIntegralEQ.accept(TVisitor v)
void	TIntegralDiv.accept(TVisitor v)
void	TIntegralAdd.accept(TVisitor v)
void	TInt.accept(TVisitor v)
void	TForAll.accept(TVisitor v)
void	TFloatNE.accept(TVisitor v)
void	TFloatMul.accept(TVisitor v)
void	TFloatMod.accept(TVisitor v)
void	TFloatLT.accept(TVisitor v)
void	TFloatLE.accept(TVisitor v)
void	TFloatGT.accept(TVisitor v)
void	TFloatGE.accept(TVisitor v)
void	TFloatEQ.accept(TVisitor v)
void	TFloatDiv.accept(TVisitor v)
void	TFloatAdd.accept(TVisitor v)
void	TFloat.accept(TVisitor v)
void	TFClosedTime.accept(TVisitor v)
void	TExist.accept(TVisitor v)
void	TEClosedTime.accept(TVisitor v)
void	TDouble.accept(TVisitor v)
void	TChar.accept(TVisitor v)
void	TCast.accept(TVisitor v)
void	TBoolOr.accept(TVisitor v)
void	TBoolNot.accept(TVisitor v)
void	TBoolNE.accept(TVisitor v)
void	TBoolImplies.accept(TVisitor v)
void	TBoolEQ.accept(TVisitor v)
void	TBoolean.accept(TVisitor v)
void	TBoolAnd.accept(TVisitor v)
void	TAsLockSet.accept(TVisitor v)
void	TAsField.accept(TVisitor v)
void	TAsElems.accept(TVisitor v)
void	TArrayShapeOne.accept(TVisitor v)
void	TArrayShapeMore.accept(TVisitor v)
void	TArrayLength.accept(TVisitor v)
void	TArrayFresh.accept(TVisitor v)
void	TAnyNE.accept(TVisitor v)
void	TAnyEQ.accept(TVisitor v)
void	TAllocLT.accept(TVisitor v)
void	TAllocLE.accept(TVisitor v)

Uses of TVisitor in escjava.vcGeneration.coq

Subclasses of TVisitor in escjava.vcGeneration.coq

class	TCoqBoolVisitor In the Coq extension, we differentiate Boolean value and variables from usual Prop.
(package private) class	TCoqVisitor In the Coq extension, we differentiate Boolean value and variables from usual Prop.
class	TProofSimplifier Stolen from the PVS extension.
class	TProofTyperVisitor Coq extension needs 'clear' typing.

Methods in escjava.vcGeneration.coq that return TVisitor

TVisitor

CoqProver.visitor(java.io.Writer out)

Uses of TVisitor in escjava.vcGeneration.coq.visitor

Subclasses of TVisitor in escjava.vcGeneration.coq.visitor

class	escjava.vcGeneration.coq.visitor.AArrayOpsVisitor
class	escjava.vcGeneration.coq.visitor.ABasicCoqVisitor
class	escjava.vcGeneration.coq.visitor.AFloatVisitor
class	escjava.vcGeneration.coq.visitor.AIntegralVisitor
class	escjava.vcGeneration.coq.visitor.ANotHandledVisitor This class implements all the functions that are not handled by the Coq visitor.

Uses of TVisitor in escjava.vcGeneration.pvs

Subclasses of TVisitor in escjava.vcGeneration.pvs

class

TPvsVisitor

Methods in escjava.vcGeneration.pvs that return TVisitor

TVisitor

PvsProver.visitor(java.io.Writer out)

Uses of TVisitor in escjava.vcGeneration.sammy

Methods in escjava.vcGeneration.sammy that return TVisitor

TVisitor

SammyProver.visitor(java.io.Writer out)

Uses of TVisitor in escjava.vcGeneration.simplify

Subclasses of TVisitor in escjava.vcGeneration.simplify

(package private) class

TSimplifyVisitor

Methods in escjava.vcGeneration.simplify that return TVisitor

TVisitor

SimplifyProver.visitor(java.io.Writer out)

Uses of TVisitor in escjava.vcGeneration.xml

Subclasses of TVisitor in escjava.vcGeneration.xml

(package private) class

TXmlVisitor Visitor implementation that generates an XML string conforming to the DTD escjava/vcGeneration/xml/xmlprover.dtd.

Methods in escjava.vcGeneration.xml that return TVisitor

TVisitor

XmlProver.visitor(java.io.Writer out)