Uses of Class
jml2b.util.Profiler

Packages that use Profiler

jack.plugin.compile
jml2b
jml2b.exceptions
jml2b.formula	Provides the classes necessary to create and manage formulas.
jml2b.languages.java
jml2b.link
jml2b.pog	Provides the classes necessary to generate proof obligations.
jml2b.pog.lemma
jml2b.pog.printers
jml2b.pog.proofobligation
jml2b.pog.substitution	Provides the classes necessary to create and manage substitutions.
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.
jml2b.util

Uses of Profiler in jack.plugin.compile

Subclasses of Profiler in jack.plugin.compile

class

PoGeneratorErrorHandler Error handler that adds markers for errors instead of just printing errors to stderr.

Uses of Profiler in jml2b

Subclasses of Profiler in jml2b

class	Jml2b
class	Serializer Simple application loading the java.lang classes and serializing them using the Java serialisation mechanism.

Uses of Profiler in jml2b.exceptions

Subclasses of Profiler in jml2b.exceptions

class	ErrorHandler Interface defining how errors are reported to the user.
class	StderrHandler A simple error handler that displays errors on stderr in the style of gcc: filename:line:message

Uses of Profiler in jml2b.formula

Subclasses of Profiler in jml2b.formula

class	BinaryForm This class implements binary formula.
class	ElementsForm This class implements terminal formulas that correspond to variables xxxelements_n, where xxx can be int, short, byte, boolean, char ou ref and n is a natural number.
class	Formula This class describes a formula.
class	ModifiedFieldForm
class	QuantifiedForm This class implements quantified formula: universal, existential or union.
class	QuantifiedVarForm This class implements a list of quatified variables.
class	TerminalForm This class implements terminal formula: identifiers, literal constants and builtin types.
class	TriaryForm This class implements tri-ary formula, that is conditional formula coming from the Java structure a ? b : c or equals with restricted domains formulas.
class	TTypeForm This class implements type formula.
class	UnaryForm This class implements unary Formula.

Uses of Profiler in jml2b.languages.java

Subclasses of Profiler in jml2b.languages.java

class	JavaBinaryForm
class	JavaModifiedFieldForm
class	JavaQuantifiedForm
class	JavaQuantifiedVarForm
class	JavaTerminalForm
class	JavaTriaryForm
class	JavaTTypeForm
class	JavaType
class	JavaUnaryForm

Uses of Profiler in jml2b.link

Subclasses of Profiler in jml2b.link

class	LinkContext
class	LinkInfo
class	LinkUtils
class	VarStack This class implements a stack containing sets of fields.

Uses of Profiler in jml2b.pog

Subclasses of Profiler in jml2b.pog

class

Pog This class provides static methods allowing to run the proof obligations generation.

Uses of Profiler in jml2b.pog.lemma

Subclasses of Profiler in jml2b.pog.lemma

(package private) class	jml2b.pog.lemma.BehaviourLemma This class defines lemmas resulting from the proof of a method specification with differents cases.
class	ExceptionalBehaviourStack This class describes a stack of proof obligations associated to exceptional behaviours.
class	ExceptionalLemma This class defines lemmas resulting from the proof of an exceptional method specification.
class	ExsuresLemma This class contains the information extracted from an exsures pragma.
class	Goal This class implements a goal.
class	GoalStatus This class provides constants and facilities to manage the status of a goal.
class	LabeledProofsVector This class provides a set of LabeledProofs.
class	Lemma This class defines a lemma.
class	NonObviousGoal This class implements a non obvious goal, that is a goal that will be saved in the JPO file.
class	NormalLemma This class defines lemmas resulting from the proof of a normal method specification.
class	SimpleLemma This class implements a simple lemma, that is a set of goals
class	Theorem This class describes a theorem.
class	TheoremList This class implements a list of theorems
class	VariantLemma
class	VirtualFormula This class implements a formula with its set of colored informations.

Uses of Profiler in jml2b.pog.printers

Subclasses of Profiler in jml2b.pog.printers

class

ClassResolver

Uses of Profiler in jml2b.pog.proofobligation

Subclasses of Profiler in jml2b.pog.proofobligation

class	ConstructorPO This class describes proof obligations for a constructor and facilities to calculate them.
class	MethodPO This class describes proof obligations for a method and facilities to calculate them.
class	ProofObligation This abstract class describes a proof obligation and facilities to calculate them.
class	SourceProofObligation This abstract class describes a proof obligation and facilities to calculate them at source level.
class	StaticInitializationPO This class describes a proof obligation for a static initialization and facilities to calculate them.
class	WellDefinedInvPO
class	WellDefinedSpecPO

Uses of Profiler in jml2b.pog.substitution

Subclasses of Profiler in jml2b.pog.substitution

class	SubArrayElement This class corresponds to the substitution of xxxelements with a formula.
class	SubArrayElementSingle This class corresponds to the substitution of xxxelements with a xxxelements <+ {f |-> xxxelements(f) <+ {i |-> v}}.
class	SubArrayLength This class corresponds to the substitution of arraylength with a formula.
class	SubForm This class corresponds to the substitution of a formula by another.
class	SubInstances This class corresponds to the substitution of instances with: instances \/ f instances \/ {f}
class	SubInstancesSet This class corresponds to the substituion of instances with instances \/ f.
class	SubInstancesSingle This class corresponds to the substituion of instances with instances \/ {f} corresponding to an instance creation.
class	SubMemberField This class implements a substitution of a member field a by a <+ { b |-> c } corresponding to an affectation of a new value for a given instance.
class	SubStaticOrLocalField
class	SubTmpVar This class corresponds to the substitution of a tempory variable with a formula.
class	SubTypeof This abstract class describes substitutions applied on typeof
class	SubTypeofSet This interface describes a substitution of typeof by typeof <+ f * {t}
class	SubTypeofSingle This interface describes a substitution of typeof by typeof <+ {f |-> t}

Uses of Profiler in jml2b.pog.util

Subclasses of Profiler in jml2b.pog.util

class	ColoredInfo This class defines informations associated to formula in order to color the code in the viewer.
class	ContextFromPureMethod This class contains the context issued from pure method that is used when translating an expression into a formula.
class	IdentifierResolver This class provides utilities for the treatment of identifiers.
class	TemporaryField This class provides services to create and use temporary fields that are usefull during the proof obligation calculation.

Uses of Profiler in jml2b.structure

Subclasses of Profiler in jml2b.structure

class	AField
class	AMethod

Uses of Profiler in jml2b.structure.bytecode

Subclasses of Profiler in jml2b.structure.bytecode

class	ClassDefaultConstructor
class	ClassField
class	ClassFile
class	ClassMethod

Uses of Profiler in jml2b.structure.java

Subclasses of Profiler in jml2b.structure.java

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	Identifier class representing Java/Jml identifiers.
class	Invariant class representing invariants.
class	JmlLoader class used to load classes.
class	Method
class	Modifiers Class used to represent Java modifiers .
class	NamedNode
class	Package class representing packages.
class	ParsedItem This class provides features to store informations that allow to locate a parsed items.
class	Type Class representing types.
class	VarDeclParser Parser used for parsing VAR_DECL clauses.

Uses of Profiler in jml2b.structure.jml

Subclasses of Profiler in jml2b.structure.jml

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

Uses of Profiler in jml2b.structure.statement

Subclasses of Profiler in jml2b.structure.statement

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	QuantifiedVar This class implements a list of quantified fields.
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.

Uses of Profiler in jml2b.util

Subclasses of Profiler in jml2b.util

class	StatementUtils Utility class for handling statement operations
class	Tabs Simple class that simplifies handling tabs.
class	TestSerialize
class	Util Class containing utility functions.