Uses of Class
jml2b.exceptions.Jml2bException

Packages that use Jml2bException

jml2b
jml2b.exceptions
jml2b.formula	Provides the classes necessary to create and manage formulas.
jml2b.link
jml2b.pog	Provides the classes necessary to generate proof obligations.
jml2b.pog.lemma
jml2b.pog.proofobligation
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 Jml2bException in jml2b

Methods in jml2b that throw Jml2bException

static void

Serializer.loadClass(IJml2bConfiguration config, java.lang.String fqn)

Uses of Jml2bException in jml2b.exceptions

Subclasses of Jml2bException in jml2b.exceptions

class	ClassLoadException
class	LinkException
class	ParseException Exception class used to indicate error during the parsing phase.
class	TokenException A specialisation of the ParseException class that is used when unexpected tokens are encountered.
class	TypeCheckException

Uses of Jml2bException in jml2b.formula

Methods in jml2b.formula that throw Jml2bException

static TerminalForm

TerminalForm.getArraylength(IJml2bConfiguration config)

Uses of Jml2bException in jml2b.link

Methods in jml2b.link that throw Jml2bException

static int	LinkUtils.linkEnumeration(IJml2bConfiguration config, java.util.Enumeration e, LinkContext f) Links all the Linkable elements provided by the enumeration e using LinkContext f.
static int	LinkUtils.linkStatements(IJml2bConfiguration config, java.util.Enumeration e, LinkContext f)
static int	LinkUtils.typeCheckEnumeration(IJml2bConfiguration config, java.util.Enumeration e, LinkContext f)
void	Linkable.link(IJml2bConfiguration config, LinkContext f)
int	Linkable.linkStatements(IJml2bConfiguration config, LinkContext f)
Type	TypeCheckable.typeCheck(IJml2bConfiguration config, LinkContext f)

Uses of Jml2bException in jml2b.pog

Methods in jml2b.pog that throw Jml2bException

static SimpleLemma	Pog.declare(IJml2bConfiguration config, AClass c, java.util.Vector i) Quantifies and skolemizes the member invariant of a class for all instances of this class.
static Formula	Pog.quantify(IJml2bConfiguration config, AClass c, java.util.Vector i) Quantifies the member invariant of a class for all instances of this class.
static void	Pog.init(IJml2bConfiguration config) Initalize the identifier array.
void	Pog.pog(JmlFile file, IJml2bConfiguration config, java.util.Vector addedDepends, java.util.Vector removedDepends, org.eclipse.core.runtime.IProgressMonitor monitor) Generate the proof obligations associated with a JML file, calculate them and prove them with the obvious prover if requested.
void	Pog.pog(JmlFile[] files, IJml2bConfiguration config) Generates the proof obligations for all the JML files, calculate them and prove them with the obvious prover if requested.

Uses of Jml2bException in jml2b.pog.lemma

Methods in jml2b.pog.lemma that throw Jml2bException

static ExceptionalBehaviourStack	ExceptionalBehaviourStack.getFalse(IJml2bConfiguration config)
Proofs	ExceptionalBehaviourStack.throwException(IJml2bConfiguration config, AClass c) Calculates the proof obligation ensuring that the thrown of a runtime exception ensures the current proof.
ExceptionalBehaviourStack	ExceptionalBehaviourStack.finallyOnExceptionalBehaviour(IJml2bConfiguration config, Statement body, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour) Calculate the ExceptionalProofs stack resulting from the application of the body on the current stack (used to proceed a finally).
ExceptionalProofs	ExceptionalProofs.finallyOnExceptionalBehaviour(IJml2bConfiguration config, Statement body, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour) Calculate the ExceptionalProofs stack resulting from the application of the body on the current stack (used to proceed a finally).
LabeledProofsVector	LabeledProofsVector.finallyLab(IJml2bConfiguration config, Statement body, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour) Applies a WP calculus on all the labeled proofs of the set.
void	Proofs.finalize(IJml2bConfiguration config, Formula param, Expression invStaticFinalFields, Formula hyp, Formula req, java.lang.String name, ColoredInfo b, ColoredInfo method) Finalize the proof obligations by adding the parameters typing in hypothesis adding the invariant coming from the final static field initialization in hypothesis adding the invariant in hypothesis adding the requires of the current method in hypothesis assigning a name
Proofs	Proofs.param(IJml2bConfiguration config, java.util.Vector signature, Expression param, ExceptionalBehaviourStack exceptionalBehaviour) Renames the formal parameter of a called method by the calling parameters.
static Theorem	Theorem.getTrue(IJml2bConfiguration config)

Constructors in jml2b.pog.lemma that throw Jml2bException

ExceptionalLemma(IJml2bConfiguration config, Method m, java.util.Vector fields, SimpleLemma l, SimpleLemma sco, SimpleLemma ico)
Creates a set of exsures labelled lemma corresponding to the cases of a method specification corresponding to exceptional behaviours.

ExsuresLemma(IJml2bConfiguration config, Exsures ex, Expression b, GoalOrigin origin)
Constructs an exsures lemma from an exsures clause

ExsuresLemma(IJml2bConfiguration config, Exsures ex, GoalOrigin origin)
Constructs an exsures lemma from an exsures clause

NormalLemma(IJml2bConfiguration config, Method m, SimpleLemma l, SimpleLemma sc, SimpleLemma ic, java.util.Vector fields)
Creates a set of ensures labelled lemma corresponding to the cases of a method specification corresponding to normal behaviours.

SimpleLemma(IJml2bConfiguration config, Expression f, GoalOrigin origin)
Constructs a lemma from an expression.

SimpleLemma(IJml2bConfiguration config, java.util.Vector v, GoalOrigin origin)
Constructs a lemma from a set of expression.

Theorem(IJml2bConfiguration config, java.util.Enumeration e, Expression b, GoalOrigin origin)
Construct a theorem from an enumeration of Exsures.

Theorem(IJml2bConfiguration config, Method m, SimpleLemma l, SimpleLemma sc, SimpleLemma ic, java.util.Vector fields)
Construct a theorem from a method specification corresponding to the proof of its normal behaviours.

VariantLemma(IJml2bConfiguration config, Expression f)

Uses of Jml2bException in jml2b.pog.proofobligation

Methods in jml2b.pog.proofobligation that throw Jml2bException

void	ConstructorPO.pog(IJml2bConfiguration config)
void	MethodPO.pog(IJml2bConfiguration config) Process the WP calculus on the proof obligations.
abstract void	ProofObligation.pog(IJml2bConfiguration config) Process the WP calculus on the proof obligations.
void	StaticInitializationPO.pog(IJml2bConfiguration config) Process the WP calculus on the proof obligations.
void	WellDefinedInvPO.pog(IJml2bConfiguration config)
void	WellDefinedSpecPO.pog(IJml2bConfiguration config)

Constructors in jml2b.pog.proofobligation that throw Jml2bException

WellDefinedInvPO(IJml2bConfiguration config, Class c, java.util.Enumeration invariants)

WellDefinedSpecPO(IJml2bConfiguration config, Class c, Method me)

Uses of Jml2bException in jml2b.pog.util

Methods in jml2b.pog.util that throw Jml2bException

static void

IdentifierResolver.init(IJml2bConfiguration config) Initialize the set of indentifier to the set containing an element corresponding to the length pseudo field

Uses of Jml2bException in jml2b.structure

Methods in jml2b.structure that throw Jml2bException

abstract java.util.Enumeration	AMethod.getSpecCases(IJml2bConfiguration config)
abstract Expression	AMethod.getNormalizedRequires(IJml2bConfiguration config)
abstract Expression	AMethod.getNormalizedEnsures(IJml2bConfiguration config)
boolean	IAParameters.isCompatibleWith(IJml2bConfiguration config, IAParameters params) return true if all the types in this are compatible with the types in params.
boolean	IAParameters.isCompatible(java.util.Vector types) return true if the parameters are compatibles with the given vector of Type.

Constructors in jml2b.structure that throw Jml2bException

AMethod(JmlFile jf, antlr.collections.AST tree, Modifiers m, Class defining)

AMethod(ParsedItem pi, Modifiers m, Class defining)

Uses of Jml2bException in jml2b.structure.bytecode

Methods in jml2b.structure.bytecode that throw Jml2bException

void	ClassDefaultConstructor.parse(IJml2bConfiguration config)
void	ClassField.parse(IJml2bConfiguration config)
static Type	ClassField.getType(IJml2bConfiguration config, org.apache.bcel.generic.Type t)
antlr.collections.AST	ClassField.parse(JmlFile jmlFile, antlr.collections.AST ast)
void	ClassField.link(IJml2bConfiguration config, LinkContext f)
int	ClassField.linkStatements(IJml2bConfiguration config, LinkContext f)
void	ClassFile.parse(IJml2bConfiguration config)
AMethod	ClassFile.getConstructor(IJml2bConfiguration config, java.util.Vector param_types)
AMethod	ClassFile.lookupMethodCurrentClass(IJml2bConfiguration config, java.lang.String mth_name, java.util.Vector param_types, AMethod candidate)
void	ClassFile.link(IJml2bConfiguration config, LinkContext f)
int	ClassFile.linkStatements(IJml2bConfiguration config, LinkContext f)
void	ClassMethod.parse(IJml2bConfiguration config)
java.util.Enumeration	ClassMethod.getSpecCases(IJml2bConfiguration config)
Expression	ClassMethod.getNormalizedRequires(IJml2bConfiguration config)
Expression	ClassMethod.getNormalizedEnsures(IJml2bConfiguration config)
antlr.collections.AST	ClassMethod.parse(JmlFile jmlFile, antlr.collections.AST ast)
void	ClassMethod.link(IJml2bConfiguration config, LinkContext f)
int	ClassMethod.linkStatements(IJml2bConfiguration config, LinkContext f)

Constructors in jml2b.structure.bytecode that throw Jml2bException

ClassParameters(IJml2bConfiguration config, org.apache.bcel.classfile.Method m)

Uses of Jml2bException in jml2b.structure.java

Methods in jml2b.structure.java that throw Jml2bException

AMethod	AClass.lookupMethod(IJml2bConfiguration config, java.lang.String mth_name, java.util.Vector param_types) Search the given method in the class and superclass methods.
abstract AMethod	AClass.getConstructor(IJml2bConfiguration config, java.util.Vector param_types)
AMethod	AClass.lookupMethodInterface(IJml2bConfiguration config, java.lang.String mth_name, java.util.Vector param_types, AMethod candidate) Lookup the given method in the current interface (which is not class).
AMethod	AClass.lookupMethodClass(IJml2bConfiguration config, java.lang.String mth_name, java.util.Vector param_types, AMethod candidate) Lookup the given method in the current class (which is not an interface).
abstract AMethod	AClass.lookupMethodCurrentClass(IJml2bConfiguration config, java.lang.String mth_name, java.util.Vector param_types, AMethod candidate)
antlr.collections.AST	Class.parse(JmlFile jmlFile, antlr.collections.AST tree) Initialise the content of the class from the given AST tree.
void	Class.link(IJml2bConfiguration config, LinkContext f) Link the externally visible parts of the class.
Type	Class.typeCheck(IJml2bConfiguration config, LinkContext f)
int	Class.linkStatements(IJml2bConfiguration config, LinkContext f) Link the parts that cannot be directly referenced from the outside.
AMethod	Class.lookupMethodCurrentClass(IJml2bConfiguration config, java.lang.String mth_name, java.util.Vector param_types, AMethod candidate) Search for a method looking only in the current class (or interface).
AMethod	Class.getConstructor(IJml2bConfiguration config, java.util.Vector param_types) Returns the constructor matching the given parameter types.
Formula	Class.getGlobalMemberInvariant(IJml2bConfiguration config)
SimpleLemma	Class.getGlobalMemberInvariantProof(IJml2bConfiguration config)
static Class	Class.getArray(IJml2bConfiguration config) Return the class that is used to represent arrays.
antlr.collections.AST	Constructor.parse(JmlFile jmlFile, antlr.collections.AST ast)
void	Constructor.completeModifiesWithOwnFields(IJml2bConfiguration config)
abstract antlr.collections.AST	Declaration.parse(JmlFile jmlFile, antlr.collections.AST ast) Parses the content of the declaration.
antlr.collections.AST	Field.parse(JmlFile jmlFile, antlr.collections.AST a) Deprecated. The VarDeclParser class should be used instead of this method.
void	Field.link(IJml2bConfiguration config, LinkContext f)
int	Field.linkStatements(IJml2bConfiguration config, LinkContext f)
static Field[]	Field.parseVarDecl(JmlFile jmlFile, antlr.collections.AST vardecl, Modifiers mods)
LinkInfo	Identifier.linkFieldIdent(IJml2bConfiguration config, LinkContext ctx, ParsedItem ident_box)
antlr.collections.AST	Invariant.parse(JmlFile jmlFile, antlr.collections.AST ast)
void	Invariant.link(IJml2bConfiguration config, LinkContext f)
int	Invariant.linkStatements(IJml2bConfiguration config, LinkContext f)
Type	Invariant.typeCheck(IJml2bConfiguration config, LinkContext f)
void	JmlFile.link(IJml2bConfiguration config)
int	JmlFile.linkStatements(IJml2bConfiguration config) Links the statement parts of the file if needed.
void	JmlFile.typeCheck(IJml2bConfiguration config) Links the statement parts of the file if needed.
static AClass	JmlLoader.loadClass(IJml2bConfiguration config, Package p, java.lang.String name) Returns the class name from package p.
static void	JmlLoader.linkStatements(IJml2bConfiguration config) Links statements for all the remaining files.
static AClass	JmlLoader.loadClass(IJml2bConfiguration config, java.lang.String fqn) Load the given class, creating the package as needed.
Statement	Method.getBody(IJml2bConfiguration config)
antlr.collections.AST	Method.parse(JmlFile jmlFile, antlr.collections.AST a)
void	Method.link(IJml2bConfiguration config, LinkContext f)
int	Method.linkStatements(IJml2bConfiguration config, LinkContext f)
Type	Method.typeCheck(IJml2bConfiguration config, LinkContext f)
Expression	Method.getNormalizedRequires(IJml2bConfiguration config)
Expression	Method.getNormalizedEnsures(IJml2bConfiguration config)
Expression	Method.getExsuresAsExpression(IJml2bConfiguration config)
Expression	Method.getEnsuresAsExpression(IJml2bConfiguration config)
java.util.Enumeration	Method.getSpecCases(IJml2bConfiguration config) Returns the specCases elements.
java.util.Vector	Method.getSpecCasesV(IJml2bConfiguration config) Returns the specCases.
boolean	Method.matchWith(IJml2bConfiguration config, Method m)
void	Method.addAnnotation(IJml2bConfiguration config, Expression req, SpecCase sc)
boolean	Method.addAnnotation(IJml2bConfiguration config, Expression req, Expression ens, ModifiesClause mod)
java.util.Collection	Method.annotate(IJml2bConfiguration config)
boolean	Method.addComputedModifies(IJml2bConfiguration config, ModifiesList ml)
boolean	Method.addComputedRequires(IJml2bConfiguration config, Expression r)
AClass	Package.getAndLoadClass(IJml2bConfiguration config, java.lang.String name) Return a reference to the class name.
antlr.collections.AST	Parameters.parse(JmlFile jmlFile, antlr.collections.AST ast)
void	Parameters.link(IJml2bConfiguration config, LinkContext lc)
int	Parameters.linkStatements(IJml2bConfiguration config, LinkContext lc)
boolean	Parameters.isCompatible(java.util.Vector types) return true if the parameters are compatibles with the given vector of Type.
boolean	Parameters.isCompatibleWith(IJml2bConfiguration config, IAParameters params) return true if all the types in this are compatible with the types in params.
antlr.collections.AST	Type.parse(antlr.collections.AST type_ast) create a type from the given AST.
void	Type.link(IJml2bConfiguration config, LinkContext f)
int	Type.linkStatements(IJml2bConfiguration config, LinkContext f)
static Type	Type.getObject(IJml2bConfiguration config) Returns a type corresponding to the java.lang.Object class.
static Type	Type.addDims(JmlFile jmlFile, antlr.collections.AST dims_ast, Type t) count the number of dimensions in the given ast.
antlr.collections.AST	VarDeclParser.parse(JmlFile jmlFile, antlr.collections.AST ast)
void	VarDeclParser.link(IJml2bConfiguration config, LinkContext f)
int	VarDeclParser.linkStatements(IJml2bConfiguration config, LinkContext f)

Constructors in jml2b.structure.java that throw Jml2bException

Method(JmlFile jf, antlr.collections.AST tree, Modifiers m, Class defining)

Method(ParsedItem pi, Modifiers m, Class defining)

Type(IJml2bConfiguration config, Type t)
Creates a new array class containing the given elements.

Uses of Jml2bException in jml2b.structure.jml

Methods in jml2b.structure.jml that throw Jml2bException

antlr.collections.AST	Depends.parse(JmlFile jmlFile, antlr.collections.AST ast)
void	Depends.link(IJml2bConfiguration config, LinkContext f)
int	Depends.linkStatements(IJml2bConfiguration config, LinkContext f)
static void	Exsures.getExsures(java.lang.String str, java.util.Vector v) Stores the exsures clauses corresponding to str into v.
void	Exsures.link(IJml2bConfiguration config, LinkContext c)
int	Exsures.linkStatements(IJml2bConfiguration config, LinkContext c)
Type	Exsures.typeCheck(IJml2bConfiguration config, LinkContext c)
Type	GuardedModifies.typeCheck(IJml2bConfiguration config, LinkContext f)
Formula	JmlExpression.predToForm(IJml2bConfiguration config) Translates the expression into a formula
static ModifiesClause	ModifiesClause.create(JmlFile jf, antlr.collections.AST a) Create a concrete modifies clause depending of the AST content
abstract LinkInfo	ModifiesClause.linkStatements(IJml2bConfiguration config, LinkContext f) Links the content of the clause.
Type	ModifiesDot.typeCheck(IJml2bConfiguration config, LinkContext f)
LinkInfo	ModifiesEverything.linkStatements(IJml2bConfiguration config, LinkContext f)
Type	ModifiesEverything.typeCheck(IJml2bConfiguration config, LinkContext f)
Type	ModifiesLbrack.typeCheck(IJml2bConfiguration config, LinkContext f)
LinkInfo	ModifiesList.linkStatements(IJml2bConfiguration config, LinkContext f)
Type	ModifiesList.typeCheck(IJml2bConfiguration config, LinkContext f)
LinkInfo	ModifiesNothing.linkStatements(IJml2bConfiguration config, LinkContext f)
Type	ModifiesNothing.typeCheck(IJml2bConfiguration config, LinkContext f)
static Represents	Represents.create(JmlFile jf, antlr.collections.AST tree, Modifiers m, Class defining) Creates an empty represent clause from a loaded file.
antlr.collections.AST	Represents.parse(JmlFile jmlFile, antlr.collections.AST ast)
void	Represents.link(IJml2bConfiguration config, LinkContext f)
int	Represents.linkStatements(IJml2bConfiguration config, LinkContext f)
Type	Represents.typeCheck(IJml2bConfiguration config, LinkContext f)
Type	SpecArrayDotDot.typeCheck(IJml2bConfiguration config, LinkContext f)
Type	SpecArrayExpr.typeCheck(IJml2bConfiguration config, LinkContext f)
Type	SpecArrayStar.typeCheck(IJml2bConfiguration config, LinkContext f)
static void	SpecCase.parseLabel(java.util.Vector labels, antlr.collections.AST a, JmlFile jmlFile) Parses the label clause of a specification case.
antlr.collections.AST	SpecCase.parseSpecBlock(JmlFile file, antlr.collections.AST tree) Parses the content of a lightweight spec case.
void	SpecCase.completeSpecCase(IJml2bConfiguration config, Expression req, java.util.Vector labels, Modifiers mods, Modifiers methodMods, int type) Completes the modifies, if no modifies were declared, the modifies becomes a modifies \everything
void	SpecCase.link(IJml2bConfiguration config, LinkContext f)
int	SpecCase.linkStatements(IJml2bConfiguration config, LinkContext f)
Type	SpecCase.typeCheck(IJml2bConfiguration config, LinkContext f)
int	SpecCase.parseExsures(JmlFile jmlFile, antlr.collections.AST a, int first_line) Parse the content of an exsures clause, returning the new value for first_line.
int	SpecCase.parseEnsures(JmlFile jmlFile, antlr.collections.AST a, int first_line) Parses the content of the ensures clause, and returns the new value for first_line.
int	SpecCase.parseModifies(JmlFile jmlFile, antlr.collections.AST a, int first_line) Parses the modifies clause, and returns the updated value of first_line.

Constructors in jml2b.structure.jml that throw Jml2bException

SpecCase(IJml2bConfiguration config, Modifiers mods)

SpecCase(IJml2bConfiguration config, LinkContext f)
Construct and link an empty by default spec case.

Uses of Jml2bException in jml2b.structure.statement

Methods in jml2b.structure.statement that throw Jml2bException

antlr.collections.AST	ArrayInitializer.parse(antlr.collections.AST tree)
LinkInfo	ArrayInitializer.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	ArrayInitializer.typeCheck(IJml2bConfiguration config, LinkContext f)
void	ArrayInitializer.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
antlr.collections.AST	BinaryExp.parse(antlr.collections.AST tree)
LinkInfo	BinaryExp.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	BinaryExp.typeCheck(IJml2bConfiguration config, LinkContext f)
Proofs	BinaryExp.wp(IJml2bConfiguration config, java.lang.String result, Proofs normalProof, ExceptionalBehaviourStack exceptionalProof)
void	BinaryExp.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
static Expression	Expression.getFromString(java.lang.String expression)
static Expression	Expression.createE(JmlFile jf, antlr.collections.AST tree) Creates an expression from an AST node.
void	Expression.linkParameters(IJml2bConfiguration config, LinkContext f, java.util.Vector parameters) Links the parameters list of a method call and the resulting type to the parameters vector.
LinkInfo	Expression.linkMethod(IJml2bConfiguration config, LinkContext f, java.util.Vector parameters) Links a method call.
Formula	Expression.exprToForm(IJml2bConfiguration config) Converts the expression into a formula.
Formula	Expression.predToForm(IJml2bConfiguration config) Converts the expression, considered as a predicate into a formula
Proofs	Expression.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour)
abstract Proofs	Expression.wp(IJml2bConfiguration config, java.lang.String result, Proofs normalBehaviour, ExceptionalBehaviourStack exceptionalBehaviour) Returns the proofs resulting where the WP calculus apply on this expression.
antlr.collections.AST	IsSubtypeOfExp.parse(antlr.collections.AST tree)
LinkInfo	IsSubtypeOfExp.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	IsSubtypeOfExp.typeCheck(IJml2bConfiguration config, LinkContext f)
Proofs	IsSubtypeOfExp.wp(IJml2bConfiguration config, java.lang.String result, Proofs normalProof, ExceptionalBehaviourStack exceptionalProof)
antlr.collections.AST	MethodCallExp.parse(antlr.collections.AST tree)
LinkInfo	MethodCallExp.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	MethodCallExp.typeCheck(IJml2bConfiguration config, LinkContext f)
Proofs	MethodCallExp.wp(IJml2bConfiguration config, java.lang.String result, Proofs normalBehaviour, ExceptionalBehaviourStack exceptionalBehaviour)
void	MethodCallExp.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
antlr.collections.AST	QuantifiedExp.parse(antlr.collections.AST tree)
LinkInfo	QuantifiedExp.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	QuantifiedExp.typeCheck(IJml2bConfiguration config, LinkContext f)
Proofs	QuantifiedExp.wp(IJml2bConfiguration config, java.lang.String result, Proofs normalProof, ExceptionalBehaviourStack exceptionalProof)
antlr.collections.AST	QuestionExp.parse(antlr.collections.AST tree)
LinkInfo	QuestionExp.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	QuestionExp.typeCheck(IJml2bConfiguration config, LinkContext f)
Proofs	QuestionExp.wp(IJml2bConfiguration config, java.lang.String result, Proofs normalBehaviour, ExceptionalBehaviourStack exceptionalBehaviour)
void	QuestionExp.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
antlr.collections.AST	StAssert.parse(antlr.collections.AST tree) Parses the assert statement.
LinkInfo	StAssert.linkStatement(IJml2bConfiguration config, LinkContext f) Links the asserted predicate
Type	StAssert.typeCheck(IJml2bConfiguration config, LinkContext f)
Proofs	StAssert.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour) Adds the asserted predicate in hypothesis of the current normal behaviour proof and adds a new proof corresponding to the proof of the assertion.
antlr.collections.AST	StBlock.parse(antlr.collections.AST tree)
LinkInfo	StBlock.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	StBlock.typeCheck(IJml2bConfiguration config, LinkContext f)
Proofs	StBlock.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour) Applies the encapsulated statement on the current proof context.
void	StBlock.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
antlr.collections.AST	StControlFlowBreak.parse(antlr.collections.AST tree)
LinkInfo	StControlFlowBreak.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	StControlFlowBreak.typeCheck(IJml2bConfiguration config, LinkContext f)
Proofs	StControlFlowBreak.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour)
void	StControlFlowBreak.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
antlr.collections.AST	StDoWhile.parse(antlr.collections.AST tree)
LinkInfo	StDoWhile.linkStatement(IJml2bConfiguration config, LinkContext f)
Proofs	StDoWhile.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour)
void	StDoWhile.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
antlr.collections.AST	StFor.parse(antlr.collections.AST tree)
LinkInfo	StFor.linkStatement(IJml2bConfiguration config, LinkContext f)
Proofs	StFor.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour)
void	StFor.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
antlr.collections.AST	StIf.parse(antlr.collections.AST tree)
LinkInfo	StIf.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	StIf.typeCheck(IJml2bConfiguration config, LinkContext f)
Proofs	StIf.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour) Calculates the proof corresponding to each branch and guard each of them by the fact that the condition is respectively true or false.
void	StIf.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
antlr.collections.AST	StImplementsLabel.parse(antlr.collections.AST tree)
Type	StImplementsLabel.typeCheck(IJml2bConfiguration config, LinkContext f)
antlr.collections.AST	StLabel.parse(antlr.collections.AST tree)
LinkInfo	StLabel.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	StLabel.typeCheck(IJml2bConfiguration config, LinkContext f)
Proofs	StLabel.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour) If the encapsulated statement is a loop, the finishOnContinueLab proofs is changed during its evaluation.
void	StLabel.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
LinkInfo	StLoops.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	StLoops.typeCheck(IJml2bConfiguration config, LinkContext f)
void	StLoops.parseModifies(JmlFile jmlFile, antlr.collections.AST a) Parses a modifies clause.
void	StLoops.parseLoopInvariant(antlr.collections.AST subtree) Parses a loop invariant clause.
void	StLoops.parseLoopVariant(antlr.collections.AST subtree) Parses a loop variant clause.
void	StLoops.parseLoopExsures(antlr.collections.AST subtree) Parses a loop exsures clause.
antlr.collections.AST	StSequence.parse(antlr.collections.AST tree)
LinkInfo	StSequence.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	StSequence.typeCheck(IJml2bConfiguration config, LinkContext f)
Proofs	StSequence.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour) Calculates the second statement on the proof context and then the first with the resulting proof as normal behaviour.
void	StSequence.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
LinkInfo	StSkip.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	StSkip.typeCheck(IJml2bConfiguration config, LinkContext f)
antlr.collections.AST	StSpecBlock.parse(antlr.collections.AST tree)
LinkInfo	StSpecBlock.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	StSpecBlock.typeCheck(IJml2bConfiguration config, LinkContext f)
Proofs	StSpecBlock.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour)
void	StSpecBlock.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
antlr.collections.AST	StSwitch.parse(antlr.collections.AST tree)
LinkInfo	StSwitch.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	StSwitch.typeCheck(IJml2bConfiguration config, LinkContext f)
Proofs	StSwitch.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour)
void	StSwitch.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
antlr.collections.AST	StTry.parse(antlr.collections.AST tree)
LinkInfo	StTry.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	StTry.typeCheck(IJml2bConfiguration config, LinkContext f)
Proofs	StTry.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour)
void	StTry.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
antlr.collections.AST	StVarDecl.parse(antlr.collections.AST tree)
LinkInfo	StVarDecl.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	StVarDecl.typeCheck(IJml2bConfiguration config, LinkContext f)
Proofs	StVarDecl.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour)
void	StVarDecl.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
static Statement	Statement.createS(JmlFile jf, antlr.collections.AST tree) Creates a statement from an AST.
Proofs	Statement.ensures(IJml2bConfiguration config, Theorem phi1, ExceptionalBehaviourStack phi7, java.util.Vector signature) Returns the proofs resulting where the WP calculus apply on this statement.
Proofs	Statement.ensures(IJml2bConfiguration config, Proofs phi1, ExceptionalBehaviourStack phi7)
void	Statement.link(IJml2bConfiguration config, LinkContext f)
int	Statement.linkStatements(IJml2bConfiguration config, LinkContext f)
abstract antlr.collections.AST	Statement.parse(antlr.collections.AST tree) Parses an AST tree in order to instanciate the statement fields.
abstract LinkInfo	Statement.linkStatement(IJml2bConfiguration config, LinkContext f) Links the statement.
abstract Proofs	Statement.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour) Returns the proofs resulting where the WP calculus apply on this statement.
abstract void	Statement.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
antlr.collections.AST	TTypeExp.parse(antlr.collections.AST tree)
LinkInfo	TTypeExp.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	TTypeExp.typeCheck(IJml2bConfiguration config, LinkContext f)
Proofs	TTypeExp.wp(IJml2bConfiguration config, java.lang.String result, Proofs normalBehaviour, ExceptionalBehaviourStack exceptionalBehaviour) Substitute in the normal behaviour proof the resulting temporary variable with the type.
LinkInfo	TerminalExp.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	TerminalExp.typeCheck(IJml2bConfiguration config, LinkContext f)
Proofs	TerminalExp.wp(IJml2bConfiguration config, java.lang.String result, Proofs normalBehaviour, ExceptionalBehaviourStack exceptionalBehaviour) Returns the normal behaviour proof where the resulting variable has been substituted with the current expression.
antlr.collections.AST	UnaryExp.parse(antlr.collections.AST tree)
LinkInfo	UnaryExp.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	UnaryExp.typeCheck(IJml2bConfiguration config, LinkContext f)
Proofs	UnaryExp.wp(IJml2bConfiguration config, java.lang.String result, Proofs normalProof, ExceptionalBehaviourStack exceptionalProof)
void	UnaryExp.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
antlr.collections.AST	WithTypeExp.parse(antlr.collections.AST tree)
LinkInfo	WithTypeExp.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	WithTypeExp.typeCheck(IJml2bConfiguration config, LinkContext f)
Proofs	WithTypeExp.wp(IJml2bConfiguration config, java.lang.String result, Proofs normalBehaviour, ExceptionalBehaviourStack exceptionalBehaviour)
void	WithTypeExp.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)

Uses of Jml2bException in jml2b.util

Methods in jml2b.util that throw Jml2bException

void	JmlClassEntryFile.loadClass(IJml2bConfiguration config, boolean defaultExternalFile)
abstract void	JmlFileEntry.loadClass(IJml2bConfiguration config, boolean defaultExternalFile)
void	JmlSourceEntryFile.loadClass(IJml2bConfiguration config, boolean defaultExternalFile)