Uses of Interface
jml2b.IJml2bConfiguration

Packages that use IJml2bConfiguration

jack.plugin
jack.plugin.source
jml2b
jml2b.formula	Provides the classes necessary to create and manage formulas.
jml2b.link
jml2b.pog	Provides the classes necessary to generate proof obligations.
jml2b.pog.lemma
jml2b.pog.proofobligation
jml2b.pog.substitution	Provides the classes necessary to create and manage substitutions.
jml2b.pog.util
jml2b.structure
jml2b.structure.bytecode
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.
jml2b.util
jpov
jpov.structure
jpov.substitution
jpov.viewer.lemma

Uses of IJml2bConfiguration in jack.plugin

Classes in jack.plugin that implement IJml2bConfiguration

class

JackJml2bConfiguration This class represents a configuration extracted from the Jack plugin and used to compile, edit and prove jml files.

Uses of IJml2bConfiguration in jack.plugin.source

Constructors in jack.plugin.source with parameters of type IJml2bConfiguration

JmlClauseGenerator(IJml2bConfiguration configuration, org.eclipse.swt.widgets.Shell shell, JmlFile f)

ModifiesGenerator(IJml2bConfiguration configuration, org.eclipse.swt.widgets.Shell shell, JmlFile f)

RequiresGenerator(IJml2bConfiguration config, org.eclipse.swt.widgets.Shell shell, JmlFile jf, boolean reqNullPointer, boolean reqArryOutOfBounds)

Uses of IJml2bConfiguration in jml2b

Classes in jml2b that implement IJml2bConfiguration

class

Jml2bConfig

Methods in jml2b with parameters of type IJml2bConfiguration

static JmlFile[]	Jml2b.loadFiles(IJml2bConfiguration config, java.lang.String[] args) Loads files from args.
static JmlFile[]	Jml2b.loadFiles(IJml2bConfiguration config, java.lang.String[] args, int file_count) Loads the file_count files from args.
static JmlFile[]	Jml2b.loadAstImage(IJml2bConfiguration config, java.lang.String astFile)
static void	Serializer.loadClass(IJml2bConfiguration config, java.lang.String fqn)

Uses of IJml2bConfiguration in jml2b.formula

Methods in jml2b.formula with parameters of type IJml2bConfiguration

void	BinaryForm.save(IJml2bConfiguration config, IOutputStream s, IJmlFile jf)
void	ElementsForm.save(IJml2bConfiguration config, IOutputStream s, IJmlFile jf)
static Formula	Formula.create(IJml2bConfiguration config, JpoInputStream s, IJmlFile fi) Create a formula from a token read into a stream.
abstract void	Formula.save(IJml2bConfiguration config, IOutputStream s, IJmlFile jf) Saves the formula in a .jpo file
void	QuantifiedForm.save(IJml2bConfiguration config, IOutputStream s, IJmlFile jf)
void	TTypeForm.save(IJml2bConfiguration config, IOutputStream s, IJmlFile jf)
static TerminalForm	TerminalForm.getArraylength(IJml2bConfiguration config)
void	TerminalForm.save(IJml2bConfiguration config, IOutputStream s, IJmlFile jf)
void	TriaryForm.save(IJml2bConfiguration config, IOutputStream s, IJmlFile jf)
void	UnaryForm.save(IJml2bConfiguration config, IOutputStream s, IJmlFile jf)

Uses of IJml2bConfiguration in jml2b.link

Methods in jml2b.link with parameters of type IJml2bConfiguration

static int	LinkUtils.linkEnumeration(IJml2bConfiguration config, java.util.Enumeration e, LinkContext f) Links all the Linkable elements provided by the enumeration e using LinkContext f.
static int	LinkUtils.linkStatements(IJml2bConfiguration config, java.util.Enumeration e, LinkContext f)
static int	LinkUtils.typeCheckEnumeration(IJml2bConfiguration config, java.util.Enumeration e, LinkContext f)
void	Linkable.link(IJml2bConfiguration config, LinkContext f)
int	Linkable.linkStatements(IJml2bConfiguration config, LinkContext f)
Type	TypeCheckable.typeCheck(IJml2bConfiguration config, LinkContext f)

Uses of IJml2bConfiguration in jml2b.pog

Methods in jml2b.pog with parameters of type IJml2bConfiguration

void	IObviousProver.prove(IJml2bConfiguration config, JmlFile file) Prove and save the status of a jpo file.
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.
static Formula	Pog.quantify(IJml2bConfiguration config, AClass c, java.util.Vector i) Quantifies the member invariant of a class for all instances of this class.
static void	Pog.init(IJml2bConfiguration config) Initalize the identifier array.
void	Pog.pog(JmlFile file, IJml2bConfiguration config, java.util.Vector addedDepends, java.util.Vector removedDepends, org.eclipse.core.runtime.IProgressMonitor monitor) Generate the proof obligations associated with a JML file, calculate them and prove them with the obvious prover if requested.
static void	Pog.saveFiles(IJml2bConfiguration config, JmlFile file, org.eclipse.core.runtime.IProgressMonitor monitor, java.util.Vector addedDepends, java.util.Vector removedDepends, IClassResolver printer)
void	Pog.pog(JmlFile[] files, IJml2bConfiguration config) Generates the proof obligations for all the JML files, calculate them and prove them with the obvious prover if requested.

Uses of IJml2bConfiguration in jml2b.pog.lemma

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

static ExceptionalBehaviourStack	ExceptionalBehaviourStack.getFalse(IJml2bConfiguration config)
Proofs	ExceptionalBehaviourStack.throwException(IJml2bConfiguration config, AClass c) Calculates the proof obligation ensuring that the thrown of a runtime exception ensures the current proof.
ExceptionalBehaviourStack	ExceptionalBehaviourStack.finallyOnExceptionalBehaviour(IJml2bConfiguration config, Statement body, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour) Calculate the ExceptionalProofs stack resulting from the application of the body on the current stack (used to proceed a finally).
ExceptionalProofs	ExceptionalProofs.finallyOnExceptionalBehaviour(IJml2bConfiguration config, Statement body, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour) Calculate the ExceptionalProofs stack resulting from the application of the body on the current stack (used to proceed a finally).
LabeledProofsVector	LabeledProofsVector.finallyLab(IJml2bConfiguration config, Statement body, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour) Applies a WP calculus on all the labeled proofs of the set.
void	NonObviousGoal.save(IJml2bConfiguration config, JpoOutputStream s, JmlFile jf) Saves the goal in a .jpo file
void	Proofs.finalize(IJml2bConfiguration config, Formula param, Expression invStaticFinalFields, Formula hyp, Formula req, java.lang.String name, ColoredInfo b, ColoredInfo method) Finalize the proof obligations by adding the parameters typing in hypothesis adding the invariant coming from the final static field initialization in hypothesis adding the invariant in hypothesis adding the requires of the current method in hypothesis assigning a name
Proofs	Proofs.param(IJml2bConfiguration config, java.util.Vector signature, Expression param, ExceptionalBehaviourStack exceptionalBehaviour) Renames the formal parameter of a called method by the calling parameters.
void	Proofs.gc(IJml2bConfiguration config, boolean force) Tries to suppress obvious goals, lemmas, theorems.
void	Proofs.saveThl(IJml2bConfiguration config, JpoOutputStream s, JmlFile jf)
void	Proofs.save(IJml2bConfiguration config, JpoOutputStream s, JmlFile jf) Saves the proof in the a .jpo file
void	SimpleLemma.save(IJml2bConfiguration config, JpoOutputStream s, JmlFile jf)
static Theorem	Theorem.getTrue(IJml2bConfiguration config)
void	VirtualFormula.save(IJml2bConfiguration config, JpoOutputStream s, int index, JmlFile jf) Saves the virtual formula into a .jpo file

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

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(IJml2bConfiguration config, Exsures ex, Expression b, GoalOrigin origin)
Constructs an exsures lemma from an exsures clause

ExsuresLemma(IJml2bConfiguration config, Exsures ex, GoalOrigin origin)
Constructs an exsures lemma from an exsures clause

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.

SimpleLemma(IJml2bConfiguration config, Expression f, GoalOrigin origin)
Constructs a lemma from an expression.

SimpleLemma(IJml2bConfiguration config, java.util.Vector v, GoalOrigin origin)
Constructs a lemma from a set of expression.

Theorem(IJml2bConfiguration config, java.util.Enumeration e, Expression b, GoalOrigin origin)
Construct a theorem from an enumeration of Exsures.

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.

VariantLemma(IJml2bConfiguration config, Expression f)

Uses of IJml2bConfiguration in jml2b.pog.proofobligation

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

void	ConstructorPO.pog(IJml2bConfiguration config)
void	MethodPO.pog(IJml2bConfiguration config) Process the WP calculus on the proof obligations.
abstract void	ProofObligation.pog(IJml2bConfiguration config) Process the WP calculus on the proof obligations.
void	StaticInitializationPO.pog(IJml2bConfiguration config) Process the WP calculus on the proof obligations.
void	WellDefinedInvPO.pog(IJml2bConfiguration config)
void	WellDefinedSpecPO.pog(IJml2bConfiguration config)

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

WellDefinedInvPO(IJml2bConfiguration config, Class c, java.util.Enumeration invariants)

WellDefinedSpecPO(IJml2bConfiguration config, Class c, Method me)

Uses of IJml2bConfiguration in jml2b.pog.substitution

Methods in jml2b.pog.substitution with parameters of type IJml2bConfiguration

void	SubArrayElement.save(IJml2bConfiguration config, JpoOutputStream s, IJmlFile jf)
void	SubArrayElementSingle.save(IJml2bConfiguration config, JpoOutputStream s, IJmlFile jf)
void	SubArrayLength.save(IJml2bConfiguration config, JpoOutputStream s, IJmlFile jf)
void	SubForm.save(IJml2bConfiguration config, JpoOutputStream s, IJmlFile jf)
void	SubInstances.save(IJml2bConfiguration config, JpoOutputStream s, IJmlFile jf)
void	SubInstancesSet.save(IJml2bConfiguration config, JpoOutputStream s, IJmlFile jf)
void	SubInstancesSingle.save(IJml2bConfiguration config, JpoOutputStream s, IJmlFile jf)
void	SubMemberField.save(IJml2bConfiguration config, JpoOutputStream s, IJmlFile jf)
void	SubTmpVar.save(IJml2bConfiguration config, JpoOutputStream s, IJmlFile jf)
void	SubTypeof.save(IJml2bConfiguration config, JpoOutputStream s, IJmlFile jf)
void	SubTypeofSet.save(IJml2bConfiguration config, JpoOutputStream s, IJmlFile jf)
void	SubTypeofSingle.save(IJml2bConfiguration config, JpoOutputStream s, IJmlFile jf)
void	Substitution.save(IJml2bConfiguration config, JpoOutputStream s, IJmlFile jf) Saves the substitution in a .jpo file

Uses of IJml2bConfiguration in jml2b.pog.util

Methods in jml2b.pog.util with parameters of type IJml2bConfiguration

static void

IdentifierResolver.init(IJml2bConfiguration config) Initialize the set of indentifier to the set containing an element corresponding to the length pseudo field

Uses of IJml2bConfiguration in jml2b.structure

Methods in jml2b.structure with parameters of type IJml2bConfiguration

abstract java.util.Enumeration	AMethod.getSpecCases(IJml2bConfiguration config)
abstract Expression	AMethod.getNormalizedRequires(IJml2bConfiguration config)
abstract Expression	AMethod.getNormalizedEnsures(IJml2bConfiguration config)
boolean	IAParameters.isCompatibleWith(IJml2bConfiguration config, IAParameters params) return true if all the types in this are compatible with the types in params.

Uses of IJml2bConfiguration in jml2b.structure.bytecode

Methods in jml2b.structure.bytecode with parameters of type IJml2bConfiguration

void	ClassDefaultConstructor.parse(IJml2bConfiguration config)
void	ClassField.parse(IJml2bConfiguration config)
static Type	ClassField.getType(IJml2bConfiguration config, org.apache.bcel.generic.Type t)
void	ClassField.link(IJml2bConfiguration config, LinkContext f)
int	ClassField.linkStatements(IJml2bConfiguration config, LinkContext f)
void	ClassFile.parse(IJml2bConfiguration config)
void	ClassFile.link(IJml2bConfiguration config)
AMethod	ClassFile.getConstructor(IJml2bConfiguration config, java.util.Vector param_types)
AMethod	ClassFile.lookupMethodCurrentClass(IJml2bConfiguration config, java.lang.String mth_name, java.util.Vector param_types, AMethod candidate)
void	ClassFile.link(IJml2bConfiguration config, LinkContext f)
int	ClassFile.linkStatements(IJml2bConfiguration config, LinkContext f)
void	ClassMethod.parse(IJml2bConfiguration config)
java.util.Enumeration	ClassMethod.getSpecCases(IJml2bConfiguration config)
Expression	ClassMethod.getNormalizedRequires(IJml2bConfiguration config)
Expression	ClassMethod.getNormalizedEnsures(IJml2bConfiguration config)
void	ClassMethod.link(IJml2bConfiguration config, LinkContext f)
int	ClassMethod.linkStatements(IJml2bConfiguration config, LinkContext f)

Constructors in jml2b.structure.bytecode with parameters of type IJml2bConfiguration

ClassParameters(IJml2bConfiguration config, org.apache.bcel.classfile.Method m)

Uses of IJml2bConfiguration in jml2b.structure.java

Methods in jml2b.structure.java that return IJml2bConfiguration

IJml2bConfiguration

JmlFile.getConfig()

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

AMethod	AClass.lookupMethod(IJml2bConfiguration config, java.lang.String mth_name, java.util.Vector param_types) Search the given method in the class and superclass methods.
abstract AMethod	AClass.getConstructor(IJml2bConfiguration config, java.util.Vector param_types)
AMethod	AClass.lookupMethodInterface(IJml2bConfiguration config, java.lang.String mth_name, java.util.Vector param_types, AMethod candidate) Lookup the given method in the current interface (which is not class).
AMethod	AClass.lookupMethodClass(IJml2bConfiguration config, java.lang.String mth_name, java.util.Vector param_types, AMethod candidate) Lookup the given method in the current class (which is not an interface).
abstract AMethod	AClass.lookupMethodCurrentClass(IJml2bConfiguration config, java.lang.String mth_name, java.util.Vector param_types, AMethod candidate)
void	Class.link(IJml2bConfiguration config, LinkContext f) Link the externally visible parts of the class.
Type	Class.typeCheck(IJml2bConfiguration config, LinkContext f)
int	Class.linkStatements(IJml2bConfiguration config, LinkContext f) Link the parts that cannot be directly referenced from the outside.
AMethod	Class.lookupMethodCurrentClass(IJml2bConfiguration config, java.lang.String mth_name, java.util.Vector param_types, AMethod candidate) Search for a method looking only in the current class (or interface).
AMethod	Class.getConstructor(IJml2bConfiguration config, java.util.Vector param_types) Returns the constructor matching the given parameter types.
Formula	Class.getGlobalMemberInvariant(IJml2bConfiguration config)
SimpleLemma	Class.getGlobalMemberInvariantProof(IJml2bConfiguration config)
static Class	Class.getArray(IJml2bConfiguration config) Return the class that is used to represent arrays.
java.lang.String	Class.emit(IJml2bConfiguration config)
void	Class.save(IJml2bConfiguration config, JpoOutputStream s, JmlFile jf) .jpo file
void	Constructor.completeModifiesWithOwnFields(IJml2bConfiguration config)
void	Field.link(IJml2bConfiguration config, LinkContext f)
int	Field.linkStatements(IJml2bConfiguration config, LinkContext f)
LinkInfo	Identifier.linkFieldIdent(IJml2bConfiguration config, LinkContext ctx, ParsedItem ident_box)
void	Invariant.link(IJml2bConfiguration config, LinkContext f)
int	Invariant.linkStatements(IJml2bConfiguration config, LinkContext f)
Type	Invariant.typeCheck(IJml2bConfiguration config, LinkContext f)
int	JmlFile.parse(IJml2bConfiguration config) Parse the file fills the package and import structures.
void	JmlFile.link(IJml2bConfiguration config)
int	JmlFile.linkStatements(IJml2bConfiguration config) Links the statement parts of the file if needed.
void	JmlFile.typeCheck(IJml2bConfiguration config) Links the statement parts of the file if needed.
java.lang.String	JmlFile.emit(IJml2bConfiguration config)
void	JmlFile.save(IJml2bConfiguration config, JpoOutputStream s) .jpo file
static AClass	JmlLoader.loadClass(IJml2bConfiguration config, Package p, java.lang.String name) Returns the class name from package p.
static JmlFileEntry	JmlLoader.searchCandidateFile(IJml2bConfiguration config, Package p, java.lang.String name) Search a candidate file for the class name located in the package relative path pkg_path.
static boolean	JmlLoader.checkDirectory(IJml2bConfiguration config, java.lang.String dir_name) Checks that the given directory exists within the search path.
static void	JmlLoader.linkStatements(IJml2bConfiguration config) Links statements for all the remaining files.
static AClass	JmlLoader.loadClass(IJml2bConfiguration config, java.lang.String fqn) Load the given class, creating the package as needed.
static void	JmlLoader.loadDefaultClasses(IJml2bConfiguration config) Loads the default classes (ensures that they are loaded)
Statement	Method.getBody(IJml2bConfiguration config)
void	Method.link(IJml2bConfiguration config, LinkContext f)
int	Method.linkStatements(IJml2bConfiguration config, LinkContext f)
Type	Method.typeCheck(IJml2bConfiguration config, LinkContext f)
Expression	Method.getNormalizedRequires(IJml2bConfiguration config)
Expression	Method.getNormalizedEnsures(IJml2bConfiguration config)
Expression	Method.getExsuresAsExpression(IJml2bConfiguration config)
Expression	Method.getEnsuresAsExpression(IJml2bConfiguration config)
java.util.Enumeration	Method.getSpecCases(IJml2bConfiguration config) Returns the specCases elements.
java.util.Vector	Method.getSpecCasesV(IJml2bConfiguration config) Returns the specCases.
java.lang.String	Method.emitSpecCase(IJml2bConfiguration config)
boolean	Method.matchWith(IJml2bConfiguration config, Method m)
void	Method.addAnnotation(IJml2bConfiguration config, Expression req, SpecCase sc)
boolean	Method.addAnnotation(IJml2bConfiguration config, Expression req, Expression ens, ModifiesClause mod)
java.util.Collection	Method.annotate(IJml2bConfiguration config)
boolean	Method.addComputedModifies(IJml2bConfiguration config, ModifiesList ml)
boolean	Method.addComputedRequires(IJml2bConfiguration config, Expression r)
void	Method.save(IJml2bConfiguration config, JpoOutputStream s, JmlFile jf) .jpo file
Package	Package.createAndCheckSubPackage(IJml2bConfiguration config, java.lang.String name) Check that the package name exists and create the subpackage if it does.
AClass	Package.getAndLoadClass(IJml2bConfiguration config, java.lang.String name) Return a reference to the class name.
void	Parameters.link(IJml2bConfiguration config, LinkContext lc)
int	Parameters.linkStatements(IJml2bConfiguration config, LinkContext lc)
boolean	Parameters.isCompatibleWith(IJml2bConfiguration config, IAParameters params) return true if all the types in this are compatible with the types in params.
void	Type.link(IJml2bConfiguration config, LinkContext f)
int	Type.linkStatements(IJml2bConfiguration config, LinkContext f)
static Type	Type.getObject(IJml2bConfiguration config) Returns a type corresponding to the java.lang.Object class.
void	VarDeclParser.link(IJml2bConfiguration config, LinkContext f)
int	VarDeclParser.linkStatements(IJml2bConfiguration config, LinkContext f)

Constructors in jml2b.structure.java with parameters of type IJml2bConfiguration

Type(IJml2bConfiguration config, Type t)
Creates a new array class containing the given elements.

Uses of IJml2bConfiguration in jml2b.structure.jml

Methods in jml2b.structure.jml with parameters of type IJml2bConfiguration

void	Depends.link(IJml2bConfiguration config, LinkContext f)
int	Depends.linkStatements(IJml2bConfiguration config, LinkContext f)
void	Exsures.link(IJml2bConfiguration config, LinkContext c)
int	Exsures.linkStatements(IJml2bConfiguration config, LinkContext c)
Type	Exsures.typeCheck(IJml2bConfiguration config, LinkContext c)
Type	GuardedModifies.typeCheck(IJml2bConfiguration config, LinkContext f)
boolean	GuardedModifies.equals(IJml2bConfiguration config, GuardedModifies gm)
Formula	JmlExpression.predToForm(IJml2bConfiguration config) Translates the expression into a formula
abstract boolean	Modifies.equals(IJml2bConfiguration config, Modifies m)
abstract void	ModifiesClause.instancie(IJml2bConfiguration config) Instancie the modifies clause.
abstract void	ModifiesClause.instancie(Expression b, IJml2bConfiguration config) Replace this with the parameter in the modifies clause.
abstract ModifiesClause	ModifiesClause.renameParam(IJml2bConfiguration config, Parameters signature, java.util.Vector newSignature) Renames the parameter in the modifies clause.
abstract LinkInfo	ModifiesClause.linkStatements(IJml2bConfiguration config, LinkContext f) Links the content of the clause.
abstract Proofs	ModifiesClause.modifies(IJml2bConfiguration config, IModifiesField m, Proofs s) Returns the proof modified in manner to take into account the modifies clause of a called method.
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.
abstract void	ModifiesClause.addDepends(IJml2bConfiguration config, Class c) Complete the modifies with modified store-ref issued from depends clauses.
Type	ModifiesDot.typeCheck(IJml2bConfiguration config, LinkContext f)
boolean	ModifiesDot.equals(IJml2bConfiguration config, Modifies m)
void	ModifiesEverything.instancie(IJml2bConfiguration config)
void	ModifiesEverything.instancie(Expression b, IJml2bConfiguration config)
LinkInfo	ModifiesEverything.linkStatements(IJml2bConfiguration config, LinkContext f)
Type	ModifiesEverything.typeCheck(IJml2bConfiguration config, LinkContext f)
SimpleLemma	ModifiesEverything.modifiesLemmas(IJml2bConfiguration config, java.util.Vector fields, java.util.Vector nonModifiedFields, Formula[] nonModifiedxxxElements)
ModifiesClause	ModifiesEverything.renameParam(IJml2bConfiguration config, Parameters signature, java.util.Vector newSignature)
void	ModifiesEverything.addDepends(IJml2bConfiguration config, Class c) Performs no action
Proofs	ModifiesEverything.modifies(IJml2bConfiguration config, IModifiesField m, Proofs s)
Type	ModifiesIdent.typeCheck(IJml2bConfiguration config, LinkContext f)
boolean	ModifiesIdent.equals(IJml2bConfiguration config, Modifies m)
Type	ModifiesLbrack.typeCheck(IJml2bConfiguration config, LinkContext f)
boolean	ModifiesLbrack.equals(IJml2bConfiguration config, Modifies m)
boolean	ModifiesList.addWithoutDoublon(IJml2bConfiguration config, ModifiesList ml)
boolean	ModifiesList.addModifiesWithoutDoublon(IJml2bConfiguration config, GuardedModifies gm)
LinkInfo	ModifiesList.linkStatements(IJml2bConfiguration config, LinkContext f)
Type	ModifiesList.typeCheck(IJml2bConfiguration config, LinkContext f)
Proofs	ModifiesList.modifies(IJml2bConfiguration config, IModifiesField m, Proofs s) Quantifies lemmas and add hypothesis depending on the modified variable list.
ModifiesClause	ModifiesList.renameParam(IJml2bConfiguration config, Parameters signature, java.util.Vector newSignature)
void	ModifiesList.instancie(IJml2bConfiguration config)
void	ModifiesList.instancie(Expression b, IJml2bConfiguration config)
SimpleLemma	ModifiesList.modifiesLemmas(IJml2bConfiguration config, java.util.Vector fields, java.util.Vector nonModifiedFields, Formula[] nonModifiedxxxElements)
void	ModifiesList.addDepends(IJml2bConfiguration config, Class c)
void	ModifiesNothing.instancie(IJml2bConfiguration config)
void	ModifiesNothing.instancie(Expression b, IJml2bConfiguration config)
LinkInfo	ModifiesNothing.linkStatements(IJml2bConfiguration config, LinkContext f)
Type	ModifiesNothing.typeCheck(IJml2bConfiguration config, LinkContext f)
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.
ModifiesClause	ModifiesNothing.renameParam(IJml2bConfiguration config, Parameters signature, java.util.Vector newSignature)
void	ModifiesNothing.addDepends(IJml2bConfiguration config, Class c) Performs no action
Proofs	ModifiesNothing.modifies(IJml2bConfiguration config, IModifiesField m, Proofs s) Returns the proofs s, till no fields are modified
void	Represents.link(IJml2bConfiguration config, LinkContext f)
int	Represents.linkStatements(IJml2bConfiguration config, LinkContext f)
Type	Represents.typeCheck(IJml2bConfiguration config, LinkContext f)
Type	SpecArrayDotDot.typeCheck(IJml2bConfiguration config, LinkContext f)
Type	SpecArrayExpr.typeCheck(IJml2bConfiguration config, LinkContext f)
Type	SpecArrayStar.typeCheck(IJml2bConfiguration config, LinkContext f)
void	SpecCase.completeSpecCase(IJml2bConfiguration config, Expression req, java.util.Vector labels, Modifiers mods, Modifiers methodMods, int type) Completes the modifies, if no modifies were declared, the modifies becomes a modifies \everything
void	SpecCase.link(IJml2bConfiguration config, LinkContext f)
int	SpecCase.linkStatements(IJml2bConfiguration config, LinkContext f)
Type	SpecCase.typeCheck(IJml2bConfiguration config, LinkContext f)
void	SpecCase.jmlNormalize(IJml2bConfiguration config, Class definingClass) Normalize the specification case.
void	SpecCase.renameParam(IJml2bConfiguration config, Parameters signature, Parameters newSignature)
SimpleLemma	SpecCase.modifiesLemmas(IJml2bConfiguration config, java.util.Vector fields) Returns the lemmas concerning the proof of the modifies clause.
java.lang.String	SpecCase.emit(IJml2bConfiguration config)
void	SpecCase.addAnnotation(IJml2bConfiguration config, SpecCase sc)
boolean	SpecCase.addAnnotation(IJml2bConfiguration config, Expression ens, ModifiesClause mod)
boolean	SpecCase.addComputedModifies(IJml2bConfiguration config, ModifiesList ml)

Constructors in jml2b.structure.jml with parameters of type IJml2bConfiguration

SpecCase(IJml2bConfiguration config, Modifiers mods)

SpecCase(IJml2bConfiguration config)
Construct an empty spec case.

SpecCase(IJml2bConfiguration config, LinkContext f)
Construct and link an empty by default spec case.

Uses of IJml2bConfiguration in jml2b.structure.statement

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

LinkInfo	ArrayInitializer.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	ArrayInitializer.typeCheck(IJml2bConfiguration config, LinkContext f)
Proofs	ArrayInitializer.wp(IJml2bConfiguration config, java.lang.String result, Proofs normalBehaviour, ExceptionalBehaviourStack exceptionalBehaviour)
void	ArrayInitializer.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
LinkInfo	BinaryExp.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	BinaryExp.typeCheck(IJml2bConfiguration config, LinkContext f)
Proofs	BinaryExp.wp(IJml2bConfiguration config, java.lang.String result, Proofs normalProof, ExceptionalBehaviourStack exceptionalProof)
void	BinaryExp.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
void	Expression.linkParameters(IJml2bConfiguration config, LinkContext f, java.util.Vector parameters) Links the parameters list of a method call and the resulting type to the parameters vector.
LinkInfo	Expression.linkMethod(IJml2bConfiguration config, LinkContext f, java.util.Vector parameters) Links a method call.
Formula	Expression.exprToForm(IJml2bConfiguration config) Converts the expression into a formula.
Formula	Expression.predToForm(IJml2bConfiguration config) Converts the expression, considered as a predicate into a formula
Proofs	Expression.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour)
Statement	Expression.jmlNormalize(IJml2bConfiguration config, Class definingClass)
abstract Proofs	Expression.wp(IJml2bConfiguration config, java.lang.String result, Proofs normalBehaviour, ExceptionalBehaviourStack exceptionalBehaviour) Returns the proofs resulting where the WP calculus apply on this expression.
LinkInfo	IsSubtypeOfExp.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	IsSubtypeOfExp.typeCheck(IJml2bConfiguration config, LinkContext f)
Proofs	IsSubtypeOfExp.wp(IJml2bConfiguration config, java.lang.String result, Proofs normalProof, ExceptionalBehaviourStack exceptionalProof)
void	IsSubtypeOfExp.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
LinkInfo	MethodCallExp.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	MethodCallExp.typeCheck(IJml2bConfiguration config, LinkContext f)
Proofs	MethodCallExp.wp(IJml2bConfiguration config, java.lang.String result, Proofs normalBehaviour, ExceptionalBehaviourStack exceptionalBehaviour)
void	MethodCallExp.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
LinkInfo	QuantifiedExp.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	QuantifiedExp.typeCheck(IJml2bConfiguration config, LinkContext f)
Proofs	QuantifiedExp.wp(IJml2bConfiguration config, java.lang.String result, Proofs normalProof, ExceptionalBehaviourStack exceptionalProof)
void	QuantifiedExp.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
LinkInfo	QuestionExp.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	QuestionExp.typeCheck(IJml2bConfiguration config, LinkContext f)
Proofs	QuestionExp.wp(IJml2bConfiguration config, java.lang.String result, Proofs normalBehaviour, ExceptionalBehaviourStack exceptionalBehaviour)
void	QuestionExp.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
LinkInfo	StAssert.linkStatement(IJml2bConfiguration config, LinkContext f) Links the asserted predicate
Type	StAssert.typeCheck(IJml2bConfiguration config, LinkContext f)
Statement	StAssert.jmlNormalize(IJml2bConfiguration config, Class definingClass)
Proofs	StAssert.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour) Adds the asserted predicate in hypothesis of the current normal behaviour proof and adds a new proof corresponding to the proof of the assertion.
void	StAssert.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
LinkInfo	StBlock.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	StBlock.typeCheck(IJml2bConfiguration config, LinkContext f)
Statement	StBlock.jmlNormalize(IJml2bConfiguration config, Class definingClass)
Proofs	StBlock.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour) Applies the encapsulated statement on the current proof context.
void	StBlock.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
LinkInfo	StControlFlowBreak.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	StControlFlowBreak.typeCheck(IJml2bConfiguration config, LinkContext f)
Statement	StControlFlowBreak.jmlNormalize(IJml2bConfiguration config, Class definingClass)
Proofs	StControlFlowBreak.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour)
void	StControlFlowBreak.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
LinkInfo	StDoWhile.linkStatement(IJml2bConfiguration config, LinkContext f)
Statement	StDoWhile.jmlNormalize(IJml2bConfiguration config, Class definingClass)
Proofs	StDoWhile.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour)
void	StDoWhile.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
LinkInfo	StFor.linkStatement(IJml2bConfiguration config, LinkContext f)
Statement	StFor.jmlNormalize(IJml2bConfiguration config, Class definingClass)
Proofs	StFor.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour)
void	StFor.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
LinkInfo	StIf.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	StIf.typeCheck(IJml2bConfiguration config, LinkContext f)
Statement	StIf.jmlNormalize(IJml2bConfiguration config, Class definingClass)
Proofs	StIf.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour) Calculates the proof corresponding to each branch and guard each of them by the fact that the condition is respectively true or false.
void	StIf.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
LinkInfo	StImplementsLabel.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	StImplementsLabel.typeCheck(IJml2bConfiguration config, LinkContext f)
Statement	StImplementsLabel.jmlNormalize(IJml2bConfiguration config, Class definingClass)
Proofs	StImplementsLabel.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour) Selects in the lemmas corresponding to normal behaviour, the cases corresponding to the set of implemented labels.
void	StImplementsLabel.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
LinkInfo	StLabel.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	StLabel.typeCheck(IJml2bConfiguration config, LinkContext f)
Statement	StLabel.jmlNormalize(IJml2bConfiguration config, Class definingClass)
Proofs	StLabel.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour) If the encapsulated statement is a loop, the finishOnContinueLab proofs is changed during its evaluation.
void	StLabel.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
LinkInfo	StLoops.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	StLoops.typeCheck(IJml2bConfiguration config, LinkContext f)
Statement	StLoops.jmlNormalize(IJml2bConfiguration config, Class definingClass)
LinkInfo	StSequence.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	StSequence.typeCheck(IJml2bConfiguration config, LinkContext f)
Statement	StSequence.jmlNormalize(IJml2bConfiguration config, Class definingClass)
Proofs	StSequence.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour) Calculates the second statement on the proof context and then the first with the resulting proof as normal behaviour.
void	StSequence.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
LinkInfo	StSkip.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	StSkip.typeCheck(IJml2bConfiguration config, LinkContext f)
Statement	StSkip.jmlNormalize(IJml2bConfiguration config, Class definingClass)
Proofs	StSkip.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour) Returns the normal behaviour, till skip has no effect.
void	StSkip.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
LinkInfo	StSpecBlock.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	StSpecBlock.typeCheck(IJml2bConfiguration config, LinkContext f)
Statement	StSpecBlock.jmlNormalize(IJml2bConfiguration config, Class definingClass)
Proofs	StSpecBlock.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour)
void	StSpecBlock.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
LinkInfo	StSwitch.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	StSwitch.typeCheck(IJml2bConfiguration config, LinkContext f)
Statement	StSwitch.jmlNormalize(IJml2bConfiguration config, Class definingClass)
Proofs	StSwitch.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour)
void	StSwitch.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
LinkInfo	StTry.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	StTry.typeCheck(IJml2bConfiguration config, LinkContext f)
Statement	StTry.jmlNormalize(IJml2bConfiguration config, Class definingClass)
Proofs	StTry.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour)
void	StTry.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
LinkInfo	StVarDecl.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	StVarDecl.typeCheck(IJml2bConfiguration config, LinkContext f)
Statement	StVarDecl.jmlNormalize(IJml2bConfiguration config, Class definingClass)
Proofs	StVarDecl.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour)
void	StVarDecl.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
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.
Proofs	Statement.ensures(IJml2bConfiguration config, Proofs phi1, ExceptionalBehaviourStack phi7)
void	Statement.link(IJml2bConfiguration config, LinkContext f)
int	Statement.linkStatements(IJml2bConfiguration config, LinkContext f)
abstract LinkInfo	Statement.linkStatement(IJml2bConfiguration config, LinkContext f) Links the statement.
abstract Statement	Statement.jmlNormalize(IJml2bConfiguration config, Class definingClass) Collects all the indentifier of the statement to give them an index in the identifer array.
abstract Proofs	Statement.wp(IJml2bConfiguration config, Proofs normalBehaviour, Proofs finishOnReturn, LabeledProofsVector finishOnBreakLab, LabeledProofsVector finishOnContinueLab, ExceptionalBehaviourStack exceptionalBehaviour) Returns the proofs resulting where the WP calculus apply on this statement.
abstract void	Statement.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
LinkInfo	TTypeExp.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	TTypeExp.typeCheck(IJml2bConfiguration config, LinkContext f)
Proofs	TTypeExp.wp(IJml2bConfiguration config, java.lang.String result, Proofs normalBehaviour, ExceptionalBehaviourStack exceptionalBehaviour) Substitute in the normal behaviour proof the resulting temporary variable with the type.
void	TTypeExp.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
LinkInfo	TerminalExp.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	TerminalExp.typeCheck(IJml2bConfiguration config, LinkContext f)
Proofs	TerminalExp.wp(IJml2bConfiguration config, java.lang.String result, Proofs normalBehaviour, ExceptionalBehaviourStack exceptionalBehaviour) Returns the normal behaviour proof where the resulting variable has been substituted with the current expression.
void	TerminalExp.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
LinkInfo	UnaryExp.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	UnaryExp.typeCheck(IJml2bConfiguration config, LinkContext f)
Proofs	UnaryExp.wp(IJml2bConfiguration config, java.lang.String result, Proofs normalProof, ExceptionalBehaviourStack exceptionalProof)
void	UnaryExp.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)
LinkInfo	WithTypeExp.linkStatement(IJml2bConfiguration config, LinkContext f)
Type	WithTypeExp.typeCheck(IJml2bConfiguration config, LinkContext f)
Proofs	WithTypeExp.wp(IJml2bConfiguration config, java.lang.String result, Proofs normalBehaviour, ExceptionalBehaviourStack exceptionalBehaviour)
void	WithTypeExp.getPrecondition(IJml2bConfiguration config, ModifiableSet modifies, java.util.Vector req, java.util.Vector ens)

Uses of IJml2bConfiguration in jml2b.util

Methods in jml2b.util with parameters of type IJml2bConfiguration

void	JmlClassEntryFile.loadClass(IJml2bConfiguration config, boolean defaultExternalFile)
abstract void	JmlFileEntry.loadClass(IJml2bConfiguration config, boolean defaultExternalFile)
void	JmlSourceEntryFile.loadClass(IJml2bConfiguration config, boolean defaultExternalFile)

Uses of IJml2bConfiguration in jpov

Methods in jpov with parameters of type IJml2bConfiguration

static JmlFile

JpoFile.loadJmlFile(IJml2bConfiguration configuration, java.lang.String name) Loads a JPO file

Constructors in jpov with parameters of type IJml2bConfiguration

JpoFile(IJml2bConfiguration config, java.lang.String name)
Constucts a JPO file from a given repository and a given name.

PartialJpoFile(IJml2bConfiguration config, java.lang.String name)
Constucts a JPO file from a given repository and a given name.

Uses of IJml2bConfiguration in jpov.structure

Methods in jpov.structure with parameters of type IJml2bConfiguration

static JmlFile	JmlFile.loadJmlFile(IJml2bConfiguration config, java.io.File jpoFile, JpoInputStream s) Loads the root node from a .jpo file
void	JmlFile.save(IJml2bConfiguration config, JpoOutputStream s) Saves the JML file into a .jpo file

Constructors in jpov.structure with parameters of type IJml2bConfiguration

Method(IJml2bConfiguration config, IJmlFile fi, JpoInputStream s)
Constructs a method from a loaded .jpo file

Uses of IJml2bConfiguration in jpov.substitution

Methods in jpov.substitution with parameters of type IJml2bConfiguration

void	SubArrayElement.save(IJml2bConfiguration config, JpoOutputStream s, IJmlFile jf)
void	SubArrayElementSingle.save(IJml2bConfiguration config, JpoOutputStream s, IJmlFile jf)
void	SubArrayLength.save(IJml2bConfiguration config, JpoOutputStream s, IJmlFile jf)
void	SubForm.save(IJml2bConfiguration config, JpoOutputStream s, IJmlFile jf)
void	SubInstancesSet.save(IJml2bConfiguration config, JpoOutputStream s, IJmlFile jf)
void	SubInstancesSingle.save(IJml2bConfiguration config, JpoOutputStream s, IJmlFile jf)
void	SubMemberField.save(IJml2bConfiguration config, JpoOutputStream s, IJmlFile jf)
void	SubTmpVar.save(IJml2bConfiguration config, JpoOutputStream s, IJmlFile jf)
void	SubTypeofSet.save(IJml2bConfiguration config, JpoOutputStream s, IJmlFile jf)
void	SubTypeofSingle.save(IJml2bConfiguration config, JpoOutputStream s, IJmlFile jf)
void	Substitution.save(IJml2bConfiguration config, JpoOutputStream s, IJmlFile jf) Saves the substitution in a .jpo file

Constructors in jpov.substitution with parameters of type IJml2bConfiguration

SubArrayElement(IJml2bConfiguration config, IJmlFile fi, JpoInputStream s)
Constructs a substitution

SubArrayElementSingle(IJml2bConfiguration config, IJmlFile fi, JpoInputStream s)
Constructs a substitution

SubArrayLength(IJml2bConfiguration config, IJmlFile fi, JpoInputStream s)
Constructs a substitution

SubForm(IJml2bConfiguration config, IJmlFile fi, JpoInputStream s)
Constructs a substitution.

SubInstancesSet(IJml2bConfiguration config, IJmlFile fi, JpoInputStream s)
Constructs a substitution for instances

SubInstancesSingle(IJml2bConfiguration config, IJmlFile fi, JpoInputStream s)
Constructs a substitution for instances

SubMemberField(IJml2bConfiguration config, IJmlFile fi, JpoInputStream s)
Constructs a substitution

SubTmpVar(IJml2bConfiguration config, IJmlFile fi, JpoInputStream s)
Constructs a substitution from a loaded .jpo file

SubTypeofSet(IJml2bConfiguration config, IJmlFile fi, JpoInputStream s)
Constructs a substitution for typeof

SubTypeofSingle(IJml2bConfiguration config, IJmlFile fi, JpoInputStream s)
Constructs a substitution for typeof

Uses of IJml2bConfiguration in jpov.viewer.lemma

Methods in jpov.viewer.lemma with parameters of type IJml2bConfiguration

void	LemmaView.redraw(IJml2bConfiguration config, boolean horizontal, boolean applySubstitution)

Constructors in jpov.viewer.lemma with parameters of type IJml2bConfiguration

LemmaView(IJml2bConfiguration config, org.eclipse.swt.widgets.Composite right_sform, boolean horizontal)
Constructs the part of the view that displays the lemma