|
|||||||||||
PREV NEXT | FRAMES NO FRAMES |
Packages that use AField | |
jml2b.formula | Provides the classes necessary to create and manage formulas. |
jml2b.pog.lemma | |
jml2b.pog.util | |
jml2b.structure.bytecode | |
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. |
Uses of AField in jml2b.formula |
Constructors in jml2b.formula with parameters of type AField | |
ModifiedFieldForm(AField f,
IModifiesField m)
|
Uses of AField in jml2b.pog.lemma |
Constructors in jml2b.pog.lemma with parameters of type AField | |
GoalOrigin(byte origin,
AField f)
Constructs a goal origin for a modifies |
Uses of AField in jml2b.pog.util |
Subclasses of AField in jml2b.pog.util | |
class |
TemporaryField
This class provides services to create and use temporary fields that are usefull during the proof obligation calculation. |
Methods in jml2b.pog.util with parameters of type AField | |
static int |
IdentifierResolver.addIdent(AField f)
Adds a field identifier in the set of identifier. |
Uses of AField in jml2b.structure.bytecode |
Subclasses of AField in jml2b.structure.bytecode | |
class |
ClassField
|
Methods in jml2b.structure.bytecode that return AField | |
AField |
ClassFile.getField(java.lang.String name,
AClass from)
|
Uses of AField in jml2b.structure.java |
Subclasses of AField in jml2b.structure.java | |
class |
Field
Class representing fields. |
Fields in jml2b.structure.java declared as AField | |
AField |
Identifier.field
|
Methods in jml2b.structure.java that return AField | |
AField |
AClass.getField(java.lang.String name)
Returns the field with the given name |
abstract AField |
AClass.getField(java.lang.String name,
AClass from)
|
AField |
Class.getField(java.lang.String name,
AClass from)
Gets the field named name if it is visible from the given class. |
Constructors in jml2b.structure.java with parameters of type AField | |
Identifier(AField f)
Creates a field identifier. |
Uses of AField in jml2b.structure.jml |
Methods in jml2b.structure.jml that return AField | |
AField |
ModifiesIdent.getField()
Returns the field. |
Constructors in jml2b.structure.jml with parameters of type AField | |
ModifiesIdent(AField f,
Identifier i)
Constructs a modifies corresponding to an identifier |
|
|||||||||||
PREV NEXT | FRAMES NO FRAMES |