Uses of Interface
jml2b.formula.IFormToken

Packages that use IFormToken

jml2b.formula	Provides the classes necessary to create and manage formulas.
jml2b.languages.java
jml2b.pog	Provides the classes necessary to generate proof obligations.
jml2b.pog.lemma
jml2b.pog.proofobligation
jml2b.pog.substitution	Provides the classes necessary to create and manage substitutions.
jml2b.pog.util
jml2b.structure.jml	Provides the classes necessary to create and manage jml clauses such that depends, represents, specification cases, modifies and exsures.
jml2b.structure.statement	Provides the classes necessary to create and manage java and jml statements and expressions.
jpov.substitution

Uses of IFormToken in jml2b.formula

Classes in jml2b.formula that implement IFormToken

class	BinaryForm This class implements binary formula.
class	ElementsForm This class implements terminal formulas that correspond to variables xxxelements_n, where xxx can be int, short, byte, boolean, char ou ref and n is a natural number.
class	Formula This class describes a formula.
class	ModifiedFieldForm
class	QuantifiedForm This class implements quantified formula: universal, existential or union.
class	TerminalForm This class implements terminal formula: identifiers, literal constants and builtin types.
class	TriaryForm This class implements tri-ary formula, that is conditional formula coming from the Java structure a ? b : c or equals with restricted domains formulas.
class	TTypeForm This class implements type formula.
class	UnaryForm This class implements unary Formula.

Uses of IFormToken in jml2b.languages.java

Classes in jml2b.languages.java that implement IFormToken

class	JavaBinaryForm
class	JavaModifiedFieldForm
class	JavaQuantifiedForm
class	JavaTerminalForm
class	JavaTriaryForm
class	JavaTTypeForm
class	JavaUnaryForm

Uses of IFormToken in jml2b.pog

Classes in jml2b.pog that implement IFormToken

class

Pog This class provides static methods allowing to run the proof obligations generation.

Uses of IFormToken in jml2b.pog.lemma

Classes in jml2b.pog.lemma that implement IFormToken

(package private) class	jml2b.pog.lemma.BehaviourLemma This class defines lemmas resulting from the proof of a method specification with differents cases.
class	ExceptionalBehaviourStack This class describes a stack of proof obligations associated to exceptional behaviours.
class	ExceptionalLemma This class defines lemmas resulting from the proof of an exceptional method specification.
class	ExceptionalProofs Class used during the PO generation to treat the proofs corresponding to exceptional behaviours.
class	ExsuresLemma This class contains the information extracted from an exsures pragma.
class	Goal This class implements a goal.
class	Lemma This class defines a lemma.
class	NonObviousGoal This class implements a non obvious goal, that is a goal that will be saved in the JPO file.
class	NormalLemma This class defines lemmas resulting from the proof of a normal method specification.
class	Proofs This class describes all the proof obligations associated with a method or with the static initialisation.
class	SimpleLemma This class implements a simple lemma, that is a set of goals
class	Theorem This class describes a theorem.
class	VariantLemma

Uses of IFormToken in jml2b.pog.proofobligation

Classes in jml2b.pog.proofobligation that implement IFormToken

class	ConstructorPO This class describes proof obligations for a constructor and facilities to calculate them.
class	MethodPO This class describes proof obligations for a method and facilities to calculate them.
class	SourceProofObligation This abstract class describes a proof obligation and facilities to calculate them at source level.
class	StaticInitializationPO This class describes a proof obligation for a static initialization and facilities to calculate them.
class	WellDefinedInvPO
class	WellDefinedSpecPO

Uses of IFormToken in jml2b.pog.substitution

Subinterfaces of IFormToken in jml2b.pog.substitution

interface

Substitution This interface describes a substitution.

Classes in jml2b.pog.substitution that implement IFormToken

class	SubArrayElement This class corresponds to the substitution of xxxelements with a formula.
class	SubArrayElementSingle This class corresponds to the substitution of xxxelements with a xxxelements <+ {f |-> xxxelements(f) <+ {i |-> v}}.
class	SubArrayLength This class corresponds to the substitution of arraylength with a formula.
class	SubForm This class corresponds to the substitution of a formula by another.
class	SubInstances This class corresponds to the substitution of instances with: instances \/ f instances \/ {f}
class	SubInstancesSingle This class corresponds to the substituion of instances with instances \/ {f} corresponding to an instance creation.
class	SubMemberField This class implements a substitution of a member field a by a <+ { b |-> c } corresponding to an affectation of a new value for a given instance.
class	SubStaticOrLocalField
class	SubTmpVar This class corresponds to the substitution of a tempory variable with a formula.
class	SubTypeof This abstract class describes substitutions applied on typeof
class	SubTypeofSet This interface describes a substitution of typeof by typeof <+ f * {t}
class	SubTypeofSingle This interface describes a substitution of typeof by typeof <+ {f |-> t}

Uses of IFormToken in jml2b.pog.util

Classes in jml2b.pog.util that implement IFormToken

class

ContextFromPureMethod This class contains the context issued from pure method that is used when translating an expression into a formula.

Uses of IFormToken in jml2b.structure.jml

Classes in jml2b.structure.jml that implement IFormToken

class	Modifies This class represents a modified variable.
class	ModifiesClause This class describes the content of a modifies clause.
class	ModifiesDot This class implements a modifies corresponding to a member field.
class	ModifiesEverything This class implements a \everything
class	ModifiesIdent This class corresponds to a modified field.
class	ModifiesLbrack This class implements a modifies corresponding to array elements, that is a[b], a[b..c] or a[*] where a, b and c are expressions.
class	ModifiesList This class describes the modifies clause as a list of Modifies elements.
class	ModifiesNothing This class implements a \nothing modifies clause.
class	SpecArray This class defines the possible indexes set of an array in the modifies clause.
class	SpecArrayDotDot This class represents an indexes interval
class	SpecArrayExpr This class represents an index of an array
class	SpecArrayStar This class describes all the indexes of an array that are declared to be potentially modified.

Uses of IFormToken in jml2b.structure.statement

Classes in jml2b.structure.statement that implement IFormToken

class	ArrayInitializer This class implements an array initializer statement, that is, for instance, { {"car", "house" }, {"dog", "cat", "monkey"} }.
class	BinaryExp This class implements binary expressions.
class	Expression This class defines a Java expression.
class	IsSubtypeOfExp This class implements subtype JML expression, it corresponds to code like a <: b
class	MethodCallExp This class implements a method call expression
class	QuantifiedExp This class implements a quantified expression, that is \forall type var; body or \exists type var; body.
class	QuestionExp This class implements a question expression, that is a ? b :c
class	StAssert
class	Statement This class defines a Java statement.
class	StBlock This class implements a block statement
class	StControlFlowBreak This class implements a control flow break statement, that is a throw, a continue, a break or a return.
class	StDoWhile
class	StFor
class	StIf
class	StImplementsLabel This class implements an implements label statement.
class	StLabel
class	StLoops This abstract class implements a loop statement.
class	StSequence This class implements a sequence of two statements.
class	StSkip This class implements a skip statement.
class	StSpecBlock This class implements a specified block.
class	StSwitch This class implements a switch statement
class	StTry This class implements a try catch finally statement or a try catch or a try finally statement.
class	StVarDecl This class implements a set of local field declaration statement
class	TerminalExp This class implements a terminal expression.
class	TTypeExp This class implements expressions corresponding to types.
class	UnaryExp This class implements unary expressions.
class	WithTypeExp This class implements expression with type, that is object and array creation, casting and instanceof.

Uses of IFormToken in jpov.substitution

Classes in jpov.substitution that implement IFormToken

class

SubInstancesSet This class corresponds to the substituion of instances with: instances \/ f.