|
Class Summary |
| ExceptionalBehaviourStack |
This class describes a stack of proof obligations associated to exceptional
behaviours. |
| ExceptionalLemma |
This class defines lemmas resulting from the proof of an exceptional method
specification. |
| ExceptionalProofs |
Class used during the PO generation to treat the proofs corresponding to
exceptional behaviours. |
| ExsuresLemma |
This class contains the information extracted from an exsures pragma. |
| Goal |
This class implements a goal. |
| GoalOrigin |
This class describes the origin of a goal. |
| GoalStatus |
This class provides constants and facilities to manage the status of a goal. |
| LabeledProofsVector |
This class provides a set of LabeledProofs. |
| Lemma |
This class defines a lemma. |
| NonObviousGoal |
This class implements a non obvious goal, that is a goal that will be saved
in the JPO file. |
| NormalLemma |
This class defines lemmas resulting from the proof of a normal method
specification. |
| Proofs |
This class describes all the proof obligations associated with a method or
with the static initialisation. |
| ProverStatus |
|
| SimpleLemma |
This class implements a simple lemma, that is a set of goals |
| Theorem |
This class describes a theorem. |
| TheoremList |
This class implements a list of theorems |
| VariantLemma |
|
| VirtualFormula |
This class implements a formula with its set of colored informations. |