|
|||||||||||
| PREV NEXT | FRAMES NO FRAMES | ||||||||||
| Packages that use Proofs | |
| jml2b.pog.lemma | |
| 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 Proofs in jml2b.pog.lemma |
| Subclasses of Proofs in jml2b.pog.lemma | |
class |
ExceptionalProofs
Class used during the PO generation to treat the proofs corresponding to exceptional behaviours. |
| Methods in jml2b.pog.lemma that return Proofs | |
Proofs |
ExceptionalBehaviourStack.throwException(Formula vv,
Formula c)
Returns the proof to prove to ensure that the thrown of an exception ensures the current proof. |
Proofs |
ExceptionalBehaviourStack.throwException(java.lang.String vv,
AClass c)
Returns the proof obligation ensuring that the thrown of an exception ensures the current proof. |
Proofs |
ExceptionalBehaviourStack.throwException(IJml2bConfiguration config,
AClass c)
Calculates the proof obligation ensuring that the thrown of a runtime exception ensures the current proof. |
Proofs |
ExsuresLemma.impliesExceptional(ExceptionalBehaviourStack ebs)
Returns the proof that the exsures lemma implies an exceptionnal behaviour. |
Proofs |
LabeledProofsVector.searchLabel(Formula lab)
Search in the list of labeled proofs, the proof with the corresponding label or with a null label if the searched label is
null. |
Proofs |
Proofs.sub(Substitution s)
Apply a substitution to the content of the proof. |
Proofs |
Proofs.suppressSpecialOld(int token)
Suppress the Called Old expressions in the proof. |
Proofs |
Proofs.renameParam(IAParameters signature,
java.util.Vector newSignature)
Rename the fields belonging to the parameter list with new names. |
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 |
Proofs.quantify(java.lang.String var,
Type type,
ColoredInfo b)
Quantifies the proof whith a variable. |
Proofs |
Proofs.quantify(java.lang.String var,
Formula type)
Quantifies the proof whith a variable. |
Proofs |
Proofs.quantify(java.lang.String var,
Formula type,
ColoredInfo b)
Quantifies the proof whith a variable. |
Proofs |
Proofs.quantify(Formula var,
Formula type)
|
Proofs |
Proofs.quantify(Formula var,
Formula type,
ColoredInfo b)
Quantifies the proof whith a variable. |
Proofs |
Proofs.addBox(ColoredInfo b)
Adds a colored info to the theorems. |
Proofs |
Proofs.selectLabel(java.util.Vector labels)
Selects in the lemmas corresponding to behaviours, the cases corresponding to labels. |
Proofs |
Theorem.impliesExceptional(ExceptionalBehaviourStack ebs)
Returns the proof that an exsures proof proof implies an exceptionnal behaviour. |
| Methods in jml2b.pog.lemma with parameters of type Proofs | |
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). |
void |
LabeledProofsVector.add(Formula label,
Proofs l)
Add a new labeled proof at the beggining of the list. |
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.addAll(Proofs l)
Concats two proofs. |
| Constructors in jml2b.pog.lemma with parameters of type Proofs | |
ExceptionalProofs(Type type,
Field catchParam,
Proofs proofs)
Constructs an exceptional proof from a proof catched by an exception |
|
| Uses of Proofs in jml2b.structure.java |
| Fields in jml2b.structure.java declared as Proofs | |
Proofs |
Class.staticInitLemmas
|
Proofs |
Class.wellDefInvLemmas
|
Proofs |
Method.lemmas
|
Proofs |
Method.wellDefinednessLemmas
|
| Methods in jml2b.structure.java that return Proofs | |
Proofs |
Class.getStaticInitLemmas()
|
Proofs |
Class.getWellDefInvLemmas()
|
Proofs |
Method.getLemmas()
|
Proofs |
Method.getWellDefinednessLemmas()
|
| Constructors in jml2b.structure.java with parameters of type Proofs | |
Class(java.lang.String name,
Proofs lemmas,
Proofs wellDefInvLemmas,
java.util.Vector constructors,
java.util.Vector methods)
Creates a new class. |
|
| Uses of Proofs in jml2b.structure.jml |
| Methods in jml2b.structure.jml that return Proofs | |
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. |
Proofs |
ModifiesEverything.modifies(IJml2bConfiguration config,
IModifiesField m,
Proofs s)
|
Proofs |
ModifiesList.modifies(IJml2bConfiguration config,
IModifiesField m,
Proofs s)
Quantifies lemmas and add hypothesis depending on the modified variable list. |
Proofs |
ModifiesNothing.modifies(IJml2bConfiguration config,
IModifiesField m,
Proofs s)
Returns the proofs s, till no fields are modified |
| Methods in jml2b.structure.jml with parameters of type Proofs | |
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. |
Proofs |
ModifiesEverything.modifies(IJml2bConfiguration config,
IModifiesField m,
Proofs s)
|
Proofs |
ModifiesList.modifies(IJml2bConfiguration config,
IModifiesField m,
Proofs s)
Quantifies lemmas and add hypothesis depending on the modified variable list. |
Proofs |
ModifiesNothing.modifies(IJml2bConfiguration config,
IModifiesField m,
Proofs s)
Returns the proofs s, till no fields are modified |
| Uses of Proofs in jml2b.structure.statement |
| Methods in jml2b.structure.statement that return Proofs | |
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)
|
| Methods in jml2b.structure.statement with parameters of type Proofs | |
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,
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)
|
|
|||||||||||
| PREV NEXT | FRAMES NO FRAMES | ||||||||||