Uses of Class
jml2b.pog.lemma.ExceptionalBehaviourStack

Packages that use ExceptionalBehaviourStack

jml2b.pog.lemma
jml2b.structure.statement	Provides the classes necessary to create and manage java and jml statements and expressions.

Uses of ExceptionalBehaviourStack in jml2b.pog.lemma

Methods in jml2b.pog.lemma that return ExceptionalBehaviourStack

static ExceptionalBehaviourStack	ExceptionalBehaviourStack.getFalse(IJml2bConfiguration config)
ExceptionalBehaviourStack	ExceptionalBehaviourStack.push(ExceptionalProofs eb) Push an element on top of the stack
ExceptionalBehaviourStack	ExceptionalBehaviourStack.pop(int i) Pop elements from the stack
ExceptionalBehaviourStack	ExceptionalBehaviourStack.addAll(ExceptionalBehaviourStack ebs) Concats two stacks.
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).

Methods in jml2b.pog.lemma with parameters of type ExceptionalBehaviourStack

ExceptionalBehaviourStack	ExceptionalBehaviourStack.addAll(ExceptionalBehaviourStack ebs) Concats two stacks.
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).
Proofs	ExsuresLemma.impliesExceptional(ExceptionalBehaviourStack ebs) Returns the proof that the exsures lemma implies an exceptionnal behaviour.
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.
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.
Proofs	Theorem.impliesExceptional(ExceptionalBehaviourStack ebs) Returns the proof that an exsures proof proof implies an exceptionnal behaviour.

Uses of ExceptionalBehaviourStack in jml2b.structure.statement

Methods in jml2b.structure.statement with parameters of type ExceptionalBehaviourStack

Proofs	ArrayInitializer.wp(IJml2bConfiguration config, java.lang.String result, Proofs normalBehaviour, ExceptionalBehaviourStack exceptionalBehaviour)
Proofs	BinaryExp.wp(IJml2bConfiguration config, java.lang.String result, Proofs normalProof, ExceptionalBehaviourStack exceptionalProof)
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)
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)
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.
Proofs	StBlock.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour) Applies the encapsulated statement on the current proof context.
Proofs	StControlFlowBreak.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour)
Proofs	StDoWhile.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour)
Proofs	StFor.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour)
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.
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.
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.
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.
Proofs	StSkip.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour) Returns the normal behaviour, till skip has no effect.
Proofs	StSpecBlock.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour)
Proofs	StSwitch.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour)
Proofs	StTry.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour)
Proofs	StVarDecl.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour)
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 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.
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)
Proofs	WithTypeExp.wp(IJml2bConfiguration config, java.lang.String result, Proofs normalBehaviour, ExceptionalBehaviourStack exceptionalBehaviour)