Uses of Interface
jml2b.formula.IModifiesField

Packages that use IModifiesField

jml2b.formula	Provides the classes necessary to create and manage formulas.
jml2b.structure
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.
jml2b.structure.statement	Provides the classes necessary to create and manage java and jml statements and expressions.

Uses of IModifiesField in jml2b.formula

Constructors in jml2b.formula with parameters of type IModifiesField

ModifiedFieldForm(AField f, IModifiesField m)

Uses of IModifiesField in jml2b.structure

Classes in jml2b.structure that implement IModifiesField

class

AMethod

Uses of IModifiesField in jml2b.structure.bytecode

Classes in jml2b.structure.bytecode that implement IModifiesField

class	ClassDefaultConstructor
class	ClassMethod

Uses of IModifiesField in jml2b.structure.java

Classes in jml2b.structure.java that implement IModifiesField

class	Constructor Specialisation of the Method class suitable for representing constructors.
class	Method

Uses of IModifiesField in jml2b.structure.jml

Methods in jml2b.structure.jml with parameters of type IModifiesField

abstract Proofs	ModifiesClause.modifies(IJml2bConfiguration config, IModifiesField m, Proofs s) Returns the proof modified in manner to take into account the modifies clause of a called method.
Proofs	ModifiesEverything.modifies(IJml2bConfiguration config, IModifiesField m, Proofs s)
Proofs	ModifiesList.modifies(IJml2bConfiguration config, IModifiesField m, Proofs s) Quantifies lemmas and add hypothesis depending on the modified variable list.
Proofs	ModifiesNothing.modifies(IJml2bConfiguration config, IModifiesField m, Proofs s) Returns the proofs s, till no fields are modified

Uses of IModifiesField in jml2b.structure.statement

Classes in jml2b.structure.statement that implement IModifiesField

class	StDoWhile
class	StFor
class	StLoops This abstract class implements a loop statement.
class	StSpecBlock This class implements a specified block.