Package jml2b.structure.jml

Provides the classes necessary to create and manage jml clauses such that depends, represents, specification cases, modifies and exsures.

See:
Description

Interface Summary

JmlExpression

The interface defines methods to apply to a JML expression.

Class Summary

Depends	This class implements a depends clause.
Exsures	This class implements an exsures clause, that is an exception type, a field corresponding to the exception and a property.
GuardedModifies	This class implements a guarded modifies clause.
Modifies	This class represents a modified variable.
ModifiesClause	This class describes the content of a modifies clause.
ModifiesDot	This class implements a modifies corresponding to a member field.
ModifiesEverything	This class implements a \everything
ModifiesIdent	This class corresponds to a modified field.
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.
ModifiesList	This class describes the modifies clause as a list of Modifies elements.
ModifiesNothing	This class implements a \nothing modifies clause.
Represents	This abstract class describes a represents clause.
SpecArray	This class defines the possible indexes set of an array in the modifies clause.
SpecArrayDotDot	This class represents an indexes interval
SpecArrayExpr	This class represents an index of an array
SpecArrayStar	This class describes all the indexes of an array that are declared to be potentially modified.
SpecCase	This class implements a specification case, that is a labelled record of requires, modifies, ensures and exsures.

Package jml2b.structure.jml Description

Provides the classes necessary to create and manage jml clauses such that depends, represents, specification cases, modifies and exsures.

Package Specification

Related Documentation