jml2b.pog.lemma
Class LabeledProofsVector

java.lang.Object
  jml2b.util.Profiler
      jml2b.pog.lemma.LabeledProofsVector

public class LabeledProofsVector

extends Profiler

This class provides a set of LabeledProofs.

Author:

L. Burdy

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

LabeledProofsVector

public LabeledProofsVector()

Constructs an empty set.

Method Detail

searchLabel

public 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. null labels correspond to unlabeled loops.

Parameters:

lab - the search label

Returns:

the proof corresponding to the searched label

Throws:

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.

add

public void add(Formula label,
                Proofs l)

Add a new labeled proof at the beggining of the list.

Parameters:

label - label of the new labeled proof

l - proofs of the new labeled proof

remove

public void remove()

Removes the last added labeled proof from the list.

finallyLab

public LabeledProofsVector finallyLab(IJml2bConfiguration config,
                                      Statement body,
                                      Proofs finishOnReturn,
                                      LabeledProofsVector finishOnBreakLab,
                                      LabeledProofsVector finishOnContinueLab,
                                      ExceptionalBehaviourStack exceptionalBehaviour)
                               throws Jml2bException,
                                      PogException

Applies a WP calculus on all the labeled proofs of the set.

Parameters:

body - statement on which the WP calculus should be applied

finishOnReturn - 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

Returns:

a new set of labeled proofs, each labeled proof corresponds to the proof resulting of the WP calculus taking the old labeled proof as the normal behaviour

Throws:

PogException - (see for more informations)

Jml2bException