Uses of Class
jml2b.structure.AField

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