Uses of Class
jml2b.pog.lemma.Lemma

Packages that use Lemma

jml2b.pog.lemma

Uses of Lemma in jml2b.pog.lemma

Subclasses of Lemma in jml2b.pog.lemma

(package private) class	jml2b.pog.lemma.BehaviourLemma This class defines lemmas resulting from the proof of a method specification with differents cases.
class	ExceptionalLemma This class defines lemmas resulting from the proof of an exceptional method specification.
class	ExsuresLemma This class contains the information extracted from an exsures pragma.
class	NormalLemma This class defines lemmas resulting from the proof of a normal method specification.
class	SimpleLemma This class implements a simple lemma, that is a set of goals
class	VariantLemma

Methods in jml2b.pog.lemma that return Lemma

Lemma	ExceptionalLemma.throwException(Formula vv, Formula c)
Lemma	ExceptionalLemma.throwException(java.lang.String vv, AClass c)
Lemma	ExsuresLemma.throwException(java.lang.String vv, AClass c)
Lemma	ExsuresLemma.throwException(Formula vv, Formula c)
Lemma	Lemma.throwException(Formula vv, Formula c) Returns the lemma to prove to ensure that the thrown of an exception ensures the current lemma.
Lemma	Lemma.throwException(java.lang.String vv, AClass c) Returns the lemma to prove to ensure that the thrown of an exception ensures the current lemma.
Lemma	Lemma.catchException(Type type, Field catchParam) Returns the lemma corresponding to the current lemma encapsulated in the fact that it corresponds to a catch of an exception.
Lemma	NormalLemma.catchException(Type type, Field catchParam) Creates an exceptional lemma set from the current one and a catched type with a catched parameter.
Lemma	SimpleLemma.catchException(Type type, Field catchParam) Returns an exsures lemma

Constructors in jml2b.pog.lemma with parameters of type Lemma

Proofs(Lemma l)
Construct a proof from a lemma

SimpleLemma(Lemma l)
Constructs a simple lemma containing only non obvious goals from a lemma.

Theorem(Lemma l)
Construct a theorem containing one lemma