Uses of Class
jml2b.structure.java.Method

Packages that use Method

jml2b.link
jml2b.pog.lemma
jml2b.pog.proofobligation
jml2b.structure.java

Uses of Method in jml2b.link

Fields in jml2b.link declared as Method

Method

LinkContext.currentMethod

Uses of Method in jml2b.pog.lemma

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

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.

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 Method in jml2b.pog.proofobligation

Methods in jml2b.pog.proofobligation that return Method

Method

MethodPO.getMethod() Returns the currentmethod.

Methods in jml2b.pog.proofobligation with parameters of type Method

static Formula

MethodPO.parameterDeclaration(Method method) Returns the formula corresponding to the parameter declaration of the method.

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

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

WellDefinedSpecPO(IJml2bConfiguration config, Class c, Method me)

Uses of Method in jml2b.structure.java

Subclasses of Method in jml2b.structure.java

class

Constructor Specialisation of the Method class suitable for representing constructors.

Methods in jml2b.structure.java that return Method

Method

Class.getConstructor(Parameters p)

Methods in jml2b.structure.java with parameters of type Method

boolean

Method.matchWith(IJml2bConfiguration config, Method m)