Uses of Interface
jml2b.link.Linkable

Packages that use Linkable

jml2b.languages.java
jml2b.pog.util
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 Linkable in jml2b.languages.java

Classes in jml2b.languages.java that implement Linkable

class

JavaType

Uses of Linkable in jml2b.pog.util

Classes in jml2b.pog.util that implement Linkable

class

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

Uses of Linkable in jml2b.structure

Classes in jml2b.structure that implement Linkable

class	AField
class	AMethod

Uses of Linkable in jml2b.structure.bytecode

Classes in jml2b.structure.bytecode that implement Linkable

class	ClassDefaultConstructor
class	ClassField
class	ClassFile
class	ClassMethod

Uses of Linkable in jml2b.structure.java

Classes in jml2b.structure.java that implement Linkable

class	AClass
class	Class Internal representation of classes.
class	Constraint
class	Constructor Specialisation of the Method class suitable for representing constructors.
class	Declaration Base class for representing declarations.
class	Field Class representing fields.
class	Invariant class representing invariants.
class	Method
class	Parameters
class	Type Class representing types.
class	VarDeclParser Parser used for parsing VAR_DECL clauses.

Uses of Linkable in jml2b.structure.jml

Classes in jml2b.structure.jml that implement Linkable

class	Depends This class implements a depends clause.
class	Exsures This class implements an exsures clause, that is an exception type, a field corresponding to the exception and a property.
class	Represents This abstract class describes a represents clause.
class	SpecCase This class implements a specification case, that is a labelled record of requires, modifies, ensures and exsures.

Uses of Linkable in jml2b.structure.statement

Classes in jml2b.structure.statement that implement Linkable

class	ArrayInitializer This class implements an array initializer statement, that is, for instance, { {"car", "house" }, {"dog", "cat", "monkey"} }.
class	BinaryExp This class implements binary expressions.
class	Expression This class defines a Java expression.
class	IsSubtypeOfExp This class implements subtype JML expression, it corresponds to code like a <: b
class	MethodCallExp This class implements a method call expression
class	QuantifiedExp This class implements a quantified expression, that is \forall type var; body or \exists type var; body.
class	QuestionExp This class implements a question expression, that is a ? b :c
class	StAssert
class	Statement This class defines a Java statement.
class	StBlock This class implements a block statement
class	StControlFlowBreak This class implements a control flow break statement, that is a throw, a continue, a break or a return.
class	StDoWhile
class	StFor
class	StIf
class	StImplementsLabel This class implements an implements label statement.
class	StLabel
class	StLoops This abstract class implements a loop statement.
class	StSequence This class implements a sequence of two statements.
class	StSkip This class implements a skip statement.
class	StSpecBlock This class implements a specified block.
class	StSwitch This class implements a switch statement
class	StTry This class implements a try catch finally statement or a try catch or a try finally statement.
class	StVarDecl This class implements a set of local field declaration statement
class	TerminalExp This class implements a terminal expression.
class	TTypeExp This class implements expressions corresponding to types.
class	UnaryExp This class implements unary expressions.
class	WithTypeExp This class implements expression with type, that is object and array creation, casting and instanceof.