Uses of Class
jml2b.structure.java.Field

Packages that use Field

jml2b.formula	Provides the classes necessary to create and manage formulas.
jml2b.link
jml2b.pog.lemma
jml2b.pog.util
jml2b.structure.java
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.

Uses of Field in jml2b.formula

Methods in jml2b.formula with parameters of type Field

static Formula	Formula.declarField(Field f) Returns the formula corresponding to a field declaration.
Formula	Formula.sub(Field a, Field b, boolean subInCalledOld) Applies a substitution on a formula.

Uses of Field in jml2b.link

Methods in jml2b.link that return Field

Field

VarStack.getField(java.lang.String name) Return the field with the given name.

Methods in jml2b.link with parameters of type Field

void	VarStack.add(Field f) Add a field to the set on the top of the stack.

Uses of Field in jml2b.pog.lemma

Methods in jml2b.pog.lemma that return Field

Field

ExsuresLemma.getExceptionField()

Methods in jml2b.pog.lemma with parameters of type Field

Lemma	Lemma.catchException(Type type, Field catchParam) Returns the lemma corresponding to the current lemma encapsulated in the fact that it corresponds to a catch of an exception.
Lemma	NormalLemma.catchException(Type type, Field catchParam) Creates an exceptional lemma set from the current one and a catched type with a catched parameter.
Lemma	SimpleLemma.catchException(Type type, Field catchParam) Returns an exsures lemma

Constructors in jml2b.pog.lemma with parameters of type Field

ExceptionalProofs(Type type, Field catchParam, Proofs proofs)
Constructs an exceptional proof from a proof catched by an exception

ExsuresLemma(Type t, Field f, SimpleLemma p)
Constructs an exsures lemma

Uses of Field in jml2b.pog.util

Subclasses of Field in jml2b.pog.util

class

TemporaryField This class provides services to create and use temporary fields that are usefull during the proof obligation calculation.

Uses of Field in jml2b.structure.java

Methods in jml2b.structure.java that return Field

static Field[]	Field.parseVarDecl(JmlFile jmlFile, antlr.collections.AST vardecl, Modifiers mods)
Field	Parameters.getField(int i)
Field[]	VarDeclParser.getArray() Returns the parsed variables as an array of fields.

Methods in jml2b.structure.java with parameters of type Field

void	Class.addGhost(Field f)
void	Class.addFields(Field fi)

Uses of Field in jml2b.structure.jml

Methods in jml2b.structure.jml that return Field

Field

Exsures.getField() Returns the field declared into the exsures clause.

Uses of Field in jml2b.structure.statement

Methods in jml2b.structure.statement that return Field

Field

QuantifiedVar.getField() Returns the current field.

Methods in jml2b.structure.statement with parameters of type Field

Expression	ArrayInitializer.subField(Field f, Field newF)
Expression	BinaryExp.subField(Field f, Field newF)
abstract Expression	Expression.subField(Field f, Field newF)
Expression	IsSubtypeOfExp.subField(Field f, Field newF)
Expression	MethodCallExp.subField(Field f, Field newF)
Expression	QuantifiedExp.subField(Field f, Field newF)
Expression	QuestionExp.subField(Field f, Field newF)
Expression	TTypeExp.subField(Field f, Field newF)
Expression	TerminalExp.subField(Field f, Field newF)
Expression	UnaryExp.subField(Field f, Field newF)
Expression	WithTypeExp.subField(Field f, Field newF)

Constructors in jml2b.structure.statement with parameters of type Field

QuantifiedVar(ParsedItem pi, Field f, QuantifiedVar n)
Constructs a quantified fields list form another one.