Uses of Class
jml2b.exceptions.PogException

Packages that use PogException

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

Methods in jml2b.formula that throw PogException

Formula

Formula.renameParam(IAParameters signature, java.util.Vector newSignature) Renames the fields belonging to the parameter list with new names.

Uses of PogException in jml2b.pog

Methods in jml2b.pog that throw PogException

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.
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 PogException in jml2b.pog.lemma

Methods in jml2b.pog.lemma that throw PogException

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 PogException

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 PogException in jml2b.pog.proofobligation

Methods in jml2b.pog.proofobligation that throw PogException

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 PogException

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

WellDefinedSpecPO(IJml2bConfiguration config, Class c, Method me)

Uses of PogException in jml2b.structure

Methods in jml2b.structure that throw PogException

abstract java.util.Enumeration	AMethod.getSpecCases(IJml2bConfiguration config)
abstract Expression	AMethod.getNormalizedRequires(IJml2bConfiguration config)
abstract Expression	AMethod.getNormalizedEnsures(IJml2bConfiguration config)

Uses of PogException in jml2b.structure.bytecode

Methods in jml2b.structure.bytecode that throw PogException

java.util.Enumeration	ClassMethod.getSpecCases(IJml2bConfiguration config)
Expression	ClassMethod.getNormalizedRequires(IJml2bConfiguration config)
Expression	ClassMethod.getNormalizedEnsures(IJml2bConfiguration config)

Uses of PogException in jml2b.structure.java

Methods in jml2b.structure.java that throw PogException

Formula	Class.getGlobalMemberInvariant(IJml2bConfiguration config)
SimpleLemma	Class.getGlobalMemberInvariantProof(IJml2bConfiguration config)
void	Constructor.completeModifiesWithOwnFields(IJml2bConfiguration config)
Statement	Method.getBody(IJml2bConfiguration config)
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.
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)

Uses of PogException in jml2b.structure.jml

Methods in jml2b.structure.jml that throw PogException

Formula	JmlExpression.predToForm(IJml2bConfiguration config) Translates the expression into a formula
abstract void	ModifiesClause.instancie(IJml2bConfiguration config) Instancie the modifies clause.
abstract void	ModifiesClause.instancie(Expression b, IJml2bConfiguration config) Replace this with the parameter in the modifies clause.
abstract ModifiesClause	ModifiesClause.renameParam(IJml2bConfiguration config, Parameters signature, java.util.Vector newSignature) Renames the parameter in the modifies clause.
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.
abstract SimpleLemma	ModifiesClause.modifiesLemmas(IJml2bConfiguration config, java.util.Vector fields, java.util.Vector nonModifiedFields, Formula[] nonModifiedxxxElements) Returns the lemmas concerning the proof of the modifies clause for the current method.
abstract void	ModifiesClause.addDepends(IJml2bConfiguration config, Class c) Complete the modifies with modified store-ref issued from depends clauses.
Proofs	ModifiesList.modifies(IJml2bConfiguration config, IModifiesField m, Proofs s) Quantifies lemmas and add hypothesis depending on the modified variable list.
ModifiesClause	ModifiesList.renameParam(IJml2bConfiguration config, Parameters signature, java.util.Vector newSignature)
void	ModifiesList.instancie(IJml2bConfiguration config)
void	ModifiesList.instancie(Expression b, IJml2bConfiguration config)
SimpleLemma	ModifiesList.modifiesLemmas(IJml2bConfiguration config, java.util.Vector fields, java.util.Vector nonModifiedFields, Formula[] nonModifiedxxxElements)
void	ModifiesList.addDepends(IJml2bConfiguration config, Class c)
SimpleLemma	ModifiesNothing.modifiesLemmas(IJml2bConfiguration config, java.util.Vector fields, java.util.Vector nonModifiedFields, Formula[] nonModifiedxxxElements) Returns the lemma corresponding to proof that all the fields and all the array elements have not been modified.
void	SpecCase.jmlNormalize(IJml2bConfiguration config, Class definingClass) Normalize the specification case.
void	SpecCase.renameParam(IJml2bConfiguration config, Parameters signature, Parameters newSignature)
SimpleLemma	SpecCase.modifiesLemmas(IJml2bConfiguration config, java.util.Vector fields) Returns the lemmas concerning the proof of the modifies clause.

Uses of PogException in jml2b.structure.statement

Methods in jml2b.structure.statement that throw PogException

void	ArrayInitializer.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
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)
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.
Proofs	IsSubtypeOfExp.wp(IJml2bConfiguration config, java.lang.String result, Proofs normalProof, ExceptionalBehaviourStack exceptionalProof)
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)
Proofs	QuantifiedExp.wp(IJml2bConfiguration config, java.lang.String result, Proofs normalProof, ExceptionalBehaviourStack exceptionalProof)
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)
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.
Statement	StBlock.jmlNormalize(IJml2bConfiguration config, Class definingClass)
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)
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)
Statement	StDoWhile.jmlNormalize(IJml2bConfiguration config, Class definingClass)
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)
Statement	StFor.jmlNormalize(IJml2bConfiguration config, Class definingClass)
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)
Statement	StIf.jmlNormalize(IJml2bConfiguration config, Class definingClass)
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)
Proofs	StImplementsLabel.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour) Selects in the lemmas corresponding to normal behaviour, the cases corresponding to the set of implemented labels.
Statement	StLabel.jmlNormalize(IJml2bConfiguration config, Class definingClass)
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)
Statement	StLoops.jmlNormalize(IJml2bConfiguration config, Class definingClass)
Statement	StSequence.jmlNormalize(IJml2bConfiguration config, Class definingClass)
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)
Statement	StSpecBlock.jmlNormalize(IJml2bConfiguration config, Class definingClass)
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)
Statement	StSwitch.jmlNormalize(IJml2bConfiguration config, Class definingClass)
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)
Statement	StTry.jmlNormalize(IJml2bConfiguration config, Class definingClass)
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)
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)
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)
abstract Statement	Statement.jmlNormalize(IJml2bConfiguration config, Class definingClass) Collects all the indentifier of the statement to give them an index in the identifer array.
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)
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.
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.
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)
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)