A B C D E F G H I J K L M N O P Q R S T U V W Z

M

MAXIMUM_TOKEN - Static variable in class jack.plugin.edit.JavaLineStyler

MEMBER_FIELD - Static variable in interface jml2b.pog.substitution.Substitution

Substitution type corresponding to the substitution of a member field by a <+ { b |-> c }

MEMBER_INVARIANT - Static variable in class jml2b.pog.lemma.GoalOrigin

Goal origin value that corresponds to the proof of a non static invariant.

METHOD_CALL - Static variable in class jml2b.pog.util.ColoredInfo

comment indice corresponding to the call of a method (blue).

METHOD_CALL - Static variable in interface jml2b.structure.statement.MyToken

Token correspoding to a method call

MODEL - Static variable in interface jml2b.structure.java.ModFlags

MODIFIED_FIELD - Static variable in interface jml2b.formula.IFormToken

identifier corresponding to a modified field.

MODIFIES - Static variable in class jml2b.pog.lemma.GoalOrigin

Goal origin value that corresponds to the proof of a modifies clause.

MULTI_COMMENT - Static variable in class jack.plugin.edit.JavaLineStyler

MULTI_COMMENT_JML - Static variable in class jack.plugin.edit.JavaLineStyler

MULTI_COMMENT_JML_COLOR - Static variable in class jack.plugin.JackPlugin

Method - class jml2b.structure.java.Method.

Method() - Constructor for class jml2b.structure.java.Method

Method(JmlFile, AST, Modifiers, Class) - Constructor for class jml2b.structure.java.Method

Method(ParsedItem, Modifiers, Class) - Constructor for class jml2b.structure.java.Method

Method - class jpov.structure.Method.

This class implements a node tree corresponding to a method.

Method(IJml2bConfiguration, IJmlFile, JpoInputStream) - Constructor for class jpov.structure.Method

Constructs a method from a loaded .jpo file

MethodCallExp - class jml2b.structure.statement.MethodCallExp.

This class implements a method call expression

MethodCallExp(int, Expression, String, Expression) - Constructor for class jml2b.structure.statement.MethodCallExp

Constructs a method call expression form another one

MethodListContentProvider - class jack.plugin.source.MethodListContentProvider.

Content provider for the method list page.

MethodListContentProvider() - Constructor for class jack.plugin.source.MethodListContentProvider

MethodListLabelProvider - class jack.plugin.source.MethodListLabelProvider.

Label provider for the method list page.

MethodListLabelProvider() - Constructor for class jack.plugin.source.MethodListLabelProvider

MethodPO - class jml2b.pog.proofobligation.MethodPO.

This class describes proof obligations for a method and facilities to calculate them.

MethodPO(Class, Method, Formula, Formula, ColoredInfo, Statement, Theorem, Theorem) - Constructor for class jml2b.pog.proofobligation.MethodPO

Constructs a proof obligation

MetricsAction - class jack.plugin.metrics.MetricsAction.

Action allowing openning the selection in the Jack PO viewer view.

MetricsAction() - Constructor for class jack.plugin.metrics.MetricsAction

MetricsContentProvider - class jack.plugin.metrics.MetricsContentProvider.

Content provider providing content for ProofTaskList elements.

MetricsFilterWindow - class jack.plugin.metrics.MetricsFilterWindow.

Filter dialog for the metrics view.

MetricsView - class jack.plugin.metrics.MetricsView.

View displaying the proof results of selected JML files.

MetricsView() - Constructor for class jack.plugin.metrics.MetricsView

ModFlags - interface jml2b.structure.java.ModFlags.

Interface defining constants for the different modifier flags.

ModifiableSet - class jml2b.util.ModifiableSet.

ModifiableSet() - Constructor for class jml2b.util.ModifiableSet

ModifiableSet(HashSet) - Constructor for class jml2b.util.ModifiableSet

ModifiedFieldForm - class jml2b.formula.ModifiedFieldForm.

ModifiedFieldForm(ModifiedFieldForm) - Constructor for class jml2b.formula.ModifiedFieldForm

ModifiedFieldForm(AField, IModifiesField) - Constructor for class jml2b.formula.ModifiedFieldForm

Modifiers - class jml2b.structure.java.Modifiers.

Class used to represent Java modifiers .

Modifiers(AST) - Constructor for class jml2b.structure.java.Modifiers

Creates a new instance, initialising the modifiers from the given AST.

Modifiers(int) - Constructor for class jml2b.structure.java.Modifiers

Creates a new instance, initialising the modifiers from the given flags.

Modifies - class jml2b.structure.jml.Modifies.

This class represents a modified variable.

ModifiesClause - class jml2b.structure.jml.ModifiesClause.

This class describes the content of a modifies clause.

ModifiesDot - class jml2b.structure.jml.ModifiesDot.

This class implements a modifies corresponding to a member field.

ModifiesDot(ParsedItem, Type, Formula, ModifiesIdent) - Constructor for class jml2b.structure.jml.ModifiesDot

Constructs a modified identifier from a formula and a modified field.

ModifiesEverything - class jml2b.structure.jml.ModifiesEverything.

This class implements a \everything

ModifiesEverything() - Constructor for class jml2b.structure.jml.ModifiesEverything

Constructs an empty modifies clause.

ModifiesGenerator - class jack.plugin.source.ModifiesGenerator.

Generator of modifies clause.

ModifiesGenerator(IJml2bConfiguration, Shell, JmlFile) - Constructor for class jack.plugin.source.ModifiesGenerator

ModifiesIdent - class jml2b.structure.jml.ModifiesIdent.

This class corresponds to a modified field.

ModifiesIdent(ParsedItem, Type, Identifier) - Constructor for class jml2b.structure.jml.ModifiesIdent

Constructs a modified identifier from an identifier.

ModifiesIdent(AField, Identifier) - Constructor for class jml2b.structure.jml.ModifiesIdent

Constructs a modifies corresponding to an identifier

ModifiesLbrack - class jml2b.structure.jml.ModifiesLbrack.

This class implements a modifies corresponding to array elements, that is a[b], a[b..c] or a[*] where a, b and c are expressions.

ModifiesList - class jml2b.structure.jml.ModifiesList.

This class describes the modifies clause as a list of Modifies elements.

ModifiesList(GuardedModifies, ModifiesList) - Constructor for class jml2b.structure.jml.ModifiesList

Constructs a list from a new Modifies element and a list.

ModifiesList(Enumeration) - Constructor for class jml2b.structure.jml.ModifiesList

ModifiesList(Iterator) - Constructor for class jml2b.structure.jml.ModifiesList

ModifiesNothing - class jml2b.structure.jml.ModifiesNothing.

This class implements a \nothing modifies clause.

ModifiesNothing() - Constructor for class jml2b.structure.jml.ModifiesNothing

Constructs a \nothing modifies clause

MyLabelProvider - class jpov.viewer.lemma.MyLabelProvider.

This class implements a label provider for hypothesis and goal.

MyLabelProvider() - Constructor for class jpov.viewer.lemma.MyLabelProvider

MyToken - interface jml2b.structure.statement.MyToken.

This class defines tokens that are used to create expressions and statement that does not exist as an output of the JML parser.

main(String[]) - Static method in class jml2b.Jml2b

Parses and converts the given files.

main(String[]) - Static method in class jml2b.Serializer

main(String[]) - Static method in class jml2b.astprint

main(String[]) - Static method in class jml2b.util.Emitter

main(String[]) - Static method in class jml2b.util.TestSerialize

matchAEqualsNull() - Method in class jml2b.formula.Formula

Returns whether a formula matches with an equality with null

matchWith(IJml2bConfiguration, Method) - Method in class jml2b.structure.java.Method

matchingSignaturesF(Vector) - Method in class jml2b.structure.bytecode.ClassDefaultConstructor

matchingSignaturesF(Vector) - Method in class jml2b.structure.bytecode.ClassMethod

mergeWith(Goal) - Method in class jml2b.pog.lemma.NonObviousGoal

Compares the goal with a set of possible loaded goals.

mergeWith(Proofs) - Method in class jml2b.pog.lemma.Proofs

Merge two proofs.

mergeWith(Goal[]) - Method in class jml2b.pog.lemma.SimpleLemma

Merges the lemma with a loaded set of lemmas.

mergeWith(Class[]) - Method in class jml2b.structure.java.Class

mergeWith(JmlFile) - Method in class jml2b.structure.java.JmlFile

methodCount - Static variable in class jml2b.pog.proofobligation.SourceProofObligation

Method counter usefull to give a uniq name to each method.

methods - Variable in class jml2b.structure.java.Class

Methods defined by the current class.

modifies(IJml2bConfiguration, IModifiesField, Proofs) - Method in class jml2b.structure.jml.ModifiesClause

Returns the proof modified in manner to take into account the modifies clause of a called method.

modifies(IJml2bConfiguration, IModifiesField, Proofs) - Method in class jml2b.structure.jml.ModifiesEverything

modifies(IJml2bConfiguration, IModifiesField, Proofs) - Method in class jml2b.structure.jml.ModifiesList

Quantifies lemmas and add hypothesis depending on the modified variable list.

modifies(IJml2bConfiguration, IModifiesField, Proofs) - Method in class jml2b.structure.jml.ModifiesNothing

Returns the proofs s, till no fields are modified

modifiesLemmas(IJml2bConfiguration, Vector, Vector, Formula[]) - Method in class jml2b.structure.jml.ModifiesClause

Returns the lemmas concerning the proof of the modifies clause for the current method.

modifiesLemmas(IJml2bConfiguration, Vector, Vector, Formula[]) - Method in class jml2b.structure.jml.ModifiesEverything

modifiesLemmas(IJml2bConfiguration, Vector, Vector, Formula[]) - Method in class jml2b.structure.jml.ModifiesList

modifiesLemmas(IJml2bConfiguration, Vector, Vector, Formula[]) - Method in class jml2b.structure.jml.ModifiesNothing

Returns the lemma corresponding to proof that all the fields and all the array elements have not been modified.

modifiesLemmas(IJml2bConfiguration, Vector) - Method in class jml2b.structure.jml.SpecCase

Returns the lemmas concerning the proof of the modifies clause.

mth - Variable in class jml2b.structure.java.Identifier