Uses of Class
jml2b.pog.lemma.SimpleLemma

Packages that use SimpleLemma

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

Uses of SimpleLemma in jml2b.pog

Methods in jml2b.pog that return SimpleLemma

static SimpleLemma

Pog.declare(IJml2bConfiguration config, AClass c, java.util.Vector i) Quantifies and skolemizes the member invariant of a class for all instances of this class.

Uses of SimpleLemma in jml2b.pog.lemma

Subclasses of SimpleLemma in jml2b.pog.lemma

class

VariantLemma

Methods in jml2b.pog.lemma that return SimpleLemma

SimpleLemma	ExsuresLemma.getLemma() Returns the lemma.
SimpleLemma	Proofs.getLemma(int i)
SimpleLemma	TheoremList.getLemma(int i) Returns a lemma of a theorem of the list

Methods in jml2b.pog.lemma with parameters of type SimpleLemma

void	Proofs.addHyp(SimpleLemma sl, byte origin) Adds the goals of a lemme to the hypothesis.
void	SimpleLemma.addGoals(SimpleLemma l) Concats two simple lemmas

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

ExceptionalLemma(IJml2bConfiguration config, Method m, java.util.Vector fields, SimpleLemma l, SimpleLemma sco, SimpleLemma ico)
Creates a set of exsures labelled lemma corresponding to the cases of a method specification corresponding to exceptional behaviours.

ExsuresLemma(Type t, Field f, SimpleLemma p)
Constructs an exsures lemma

NormalLemma(IJml2bConfiguration config, Method m, SimpleLemma l, SimpleLemma sc, SimpleLemma ic, java.util.Vector fields)
Creates a set of ensures labelled lemma corresponding to the cases of a method specification corresponding to normal behaviours.

Theorem(IJml2bConfiguration config, Method m, SimpleLemma l, SimpleLemma sc, SimpleLemma ic, java.util.Vector fields)
Construct a theorem from a method specification corresponding to the proof of its normal behaviours.

Uses of SimpleLemma in jml2b.structure.java

Methods in jml2b.structure.java that return SimpleLemma

SimpleLemma

Class.getGlobalMemberInvariantProof(IJml2bConfiguration config)

Uses of SimpleLemma in jml2b.structure.jml

Methods in jml2b.structure.jml that return SimpleLemma

abstract SimpleLemma	ModifiesClause.modifiesLemmas(IJml2bConfiguration config, java.util.Vector fields, java.util.Vector nonModifiedFields, Formula[] nonModifiedxxxElements) Returns the lemmas concerning the proof of the modifies clause for the current method.
SimpleLemma	ModifiesEverything.modifiesLemmas(IJml2bConfiguration config, java.util.Vector fields, java.util.Vector nonModifiedFields, Formula[] nonModifiedxxxElements)
SimpleLemma	ModifiesList.modifiesLemmas(IJml2bConfiguration config, java.util.Vector fields, java.util.Vector nonModifiedFields, Formula[] nonModifiedxxxElements)
SimpleLemma	ModifiesNothing.modifiesLemmas(IJml2bConfiguration config, java.util.Vector fields, java.util.Vector nonModifiedFields, Formula[] nonModifiedxxxElements) Returns the lemma corresponding to proof that all the fields and all the array elements have not been modified.
SimpleLemma	SpecCase.modifiesLemmas(IJml2bConfiguration config, java.util.Vector fields) Returns the lemmas concerning the proof of the modifies clause.