|
|||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES All Classes | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Objectjml2b.util.Profiler
jml2b.pog.lemma.LabeledProofsVector
This class provides a set of LabeledProofs
.
Constructor Summary | |
LabeledProofsVector()
Constructs an empty set. |
Method Summary | |
void |
add(Formula label,
Proofs l)
Add a new labeled proof at the beggining of the list. |
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 |
remove()
Removes the last added labeled proof from the list. |
Proofs |
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 . |
Methods inherited from class jml2b.util.Profiler |
runGC |
Methods inherited from class java.lang.Object |
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Constructor Detail |
public LabeledProofsVector()
Method Detail |
public Proofs searchLabel(Formula lab)
null
label if the searched label is
null
. null
labels correspond to unlabeled loops.
lab
- the search label
InternalError
- when the label is not found.
This corresponds to a bug because the Java compiler ensures that the
labels used in the break
or continue
statements
are defined.public void add(Formula label, Proofs l)
label
- label of the new labeled proofl
- proofs of the new labeled proofpublic void remove()
public LabeledProofsVector finallyLab(IJml2bConfiguration config, Statement body, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour) throws Jml2bException, PogException
body
- statement on which the WP calculus should be appliedfinishOnReturn
- proofs to ensure when the statement finish on a
return
finishOnBreakLab
- set of labeled proofs to ensure when the
statement finish on a break
finishOnContinueLab
- set of labeled proofs to ensure when the
statement finish on a continue
exceptionalBehaviour
- exceptional proofs stack to ensures when the
statement finish on an exception thrown
PogException
- (see for
more informations
)
Jml2bException
|
|||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES All Classes | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |