Uses of Class
jml2b.pog.lemma.Theorem

Packages that use Theorem

jml2b.pog.lemma
jml2b.pog.proofobligation
jml2b.structure.statement	Provides the classes necessary to create and manage java and jml statements and expressions.

Uses of Theorem in jml2b.pog.lemma

Methods in jml2b.pog.lemma that return Theorem

Theorem	Proofs.getTheorem(int i)
static Theorem	Theorem.getTrue(IJml2bConfiguration config)
Theorem	Theorem.renameParam(IAParameters signature, java.util.Vector newSignature) Renames the parameter of a method with new identifier in the theorem
Theorem	TheoremList.getTheorem(int i) Returns a theoram of the list

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

ExceptionalProofs(Theorem t)
Constructs a proof from a theorem

Proofs(Theorem t)
Construct a proof from a theorem

Uses of Theorem in jml2b.pog.proofobligation

Constructors in jml2b.pog.proofobligation with parameters of type Theorem

ConstructorPO(Class c, java.lang.String s, Method m, Formula h1, Formula h2, ColoredInfo box, Statement b, Theorem p1, Theorem p7)
Constructs a proof obligation

MethodPO(Class c, Method m, Formula h1, Formula h2, ColoredInfo box, Statement b, Theorem p1, Theorem p7)
Constructs a proof obligation

StaticInitializationPO(Class c, Statement b, Theorem p1, Theorem p7)
Constructs a proof obligation

Uses of Theorem in jml2b.structure.statement

Methods in jml2b.structure.statement with parameters of type Theorem

Proofs

Statement.ensures(IJml2bConfiguration config, Theorem phi1, ExceptionalBehaviourStack phi7, java.util.Vector signature) Returns the proofs resulting where the WP calculus apply on this statement.