Uses of Package
jml2b.pog.lemma

Packages that use jml2b.pog.lemma

jml2b.languages
jml2b.pog	Provides the classes necessary to generate proof obligations.
jml2b.pog.lemma
jml2b.pog.proofobligation
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.
jpov.structure

Classes in jml2b.pog.lemma used by jml2b.languages

ProverStatus

Classes in jml2b.pog.lemma used by jml2b.pog

ProverStatus

SimpleLemma
This class implements a simple lemma, that is a set of goals

Classes in jml2b.pog.lemma used by jml2b.pog.lemma

ExceptionalBehaviourStack
This class describes a stack of proof obligations associated to exceptional behaviours.

ExceptionalProofs
Class used during the PO generation to treat the proofs corresponding to exceptional behaviours.

Goal
This class implements a goal.

GoalOrigin
This class describes the origin of a goal.

ILemma
This interface defines the different operations that are performed on lemma or on goal.

LabeledProofsVector
This class provides a set of LabeledProofs.

Lemma
This class defines a lemma.

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

VirtualFormula
This class implements a formula with its set of colored informations.

Classes in jml2b.pog.lemma used by jml2b.pog.proofobligation

Theorem
This class describes a theorem.

Classes in jml2b.pog.lemma used by jml2b.structure.java

Proofs
This class describes all the proof obligations associated with a method or with the static initialisation.

SimpleLemma
This class implements a simple lemma, that is a set of goals

Classes in jml2b.pog.lemma used by jml2b.structure.jml

Proofs
This class describes all the proof obligations associated with a method or with the static initialisation.

SimpleLemma
This class implements a simple lemma, that is a set of goals

Classes in jml2b.pog.lemma used by jml2b.structure.statement

ExceptionalBehaviourStack
This class describes a stack of proof obligations associated to exceptional behaviours.

LabeledProofsVector
This class provides a set of LabeledProofs.

Proofs
This class describes all the proof obligations associated with a method or with the static initialisation.

Theorem
This class describes a theorem.

Classes in jml2b.pog.lemma used by jpov.structure

GoalStatus
This class provides constants and facilities to manage the status of a goal.

ProverStatus