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

A

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

AClass - class jml2b.structure.java.AClass.

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

AClass(JmlFile, AST) - Constructor for class jml2b.structure.java.AClass

AClassEnumeration - class jml2b.pog.printers.AClassEnumeration.

AClassEnumeration(Enumeration) - Constructor for class jml2b.pog.printers.AClassEnumeration

AField - class jml2b.structure.AField.

AField() - Constructor for class jml2b.structure.AField

AField(ParsedItem, Modifiers) - Constructor for class jml2b.structure.AField

ALWAYS_COMPILE_BEFORE_EDITING - Static variable in class jack.plugin.JackPlugin

ALWAYS_COMPILE_BEFORE_PROVING - Static variable in class jack.plugin.JackPlugin

ALWAYS_SAVE_BEFORE_COMPILING - Static variable in class jack.plugin.JackPlugin

ALWAYS_SAVE_BEFORE_EDITING - Static variable in class jack.plugin.JackPlugin

ALWAYS_SAVE_BEFORE_PROVING - Static variable in class jack.plugin.JackPlugin

AMethod - class jml2b.structure.AMethod.

AMethod() - Constructor for class jml2b.structure.AMethod

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

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

ARRAY_ACCESS - Static variable in interface jml2b.formula.IFormToken

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

Substitution type corresponding to the substitution of an xxxelements by a

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

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

Substitution type corresponding to the substitution of arraylength by a

ARRAY_RANGE - Static variable in interface jml2b.formula.IFormToken

array range UNION(x).(x : a | b[c]) with priority 250.

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

Goal origin value that corresponds to the proof of an assertion.

ASSERT - Static variable in class jml2b.pog.lemma.VirtualFormula

Formula origin corresponding to an assertion

ASSERT - Static variable in class jpov.Icons

Image corresponding to the assert icon.

AddFileUpdate - class jml2b.util.AddFileUpdate.

AddFileUpdate(File, int, String) - Constructor for class jml2b.util.AddFileUpdate

AddJmlAction - class jack.plugin.source.AddJmlAction.

Action allowing to generate JML specification.

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

Constructor for Action1.

AddJmlClauseWizard - class jack.plugin.source.AddJmlClauseWizard.

Wizard allowing to select JML clause to generate, file when the automatic annotation is performed, view the difference between the new files and the old ones and perform finally the modifications.

AddJmlClauseWizard(ICompilationUnit, LoadAndLink) - Constructor for class jack.plugin.source.AddJmlClauseWizard

ArrayInitializer - class jml2b.structure.statement.ArrayInitializer.

This class implements an array initializer statement, that is, for instance, { {"car", "house" }, {"dog", "cat", "monkey"} }.

absoluteNameEquals(String) - Method in class jml2b.pog.util.IdentifierResolver

Test whether the absolute name equals the parameter.

add(Vector) - Method in class jml2b.link.VarStack

Add a new set of fields to the top of the stack.

add(Field) - Method in class jml2b.link.VarStack

Add a field to the set on the top of the stack.

add(Formula, Proofs) - Method in class jml2b.pog.lemma.LabeledProofsVector

Add a new labeled proof at the beggining of the list.

add(ModifiesList) - Method in class jml2b.structure.jml.ModifiesList

Concats two lists.

addAll(ExceptionalBehaviourStack) - Method in class jml2b.pog.lemma.ExceptionalBehaviourStack

Concats two stacks.

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

Concats two proofs.

addAll(Set) - Method in class jml2b.util.ModifiableSet

addAnnotation(IJml2bConfiguration, Expression, SpecCase) - Method in class jml2b.structure.java.Method

addAnnotation(IJml2bConfiguration, Expression, Expression, ModifiesClause) - Method in class jml2b.structure.java.Method

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

addAnnotation(IJml2bConfiguration, Expression, ModifiesClause) - Method in class jml2b.structure.jml.SpecCase

addBox(Color, Color, int, int) - Method in class jack.plugin.edit.JavaLineStyler

addBox(ColoredInfo) - Method in class jml2b.pog.lemma.Proofs

Adds a colored info to the theorems.

addClass(AClass) - Method in class jml2b.structure.java.Package

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

addComputedModifies(IJml2bConfiguration, ModifiesList) - Method in class jml2b.structure.jml.SpecCase

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

addDepends(IJml2bConfiguration, Class) - Method in class jml2b.structure.jml.ModifiesClause

Complete the modifies with modified store-ref issued from depends clauses.

addDepends(IJml2bConfiguration, Class) - Method in class jml2b.structure.jml.ModifiesEverything

Performs no action

addDepends(IJml2bConfiguration, Class) - Method in class jml2b.structure.jml.ModifiesList

addDepends(IJml2bConfiguration, Class) - Method in class jml2b.structure.jml.ModifiesNothing

Performs no action

addDims(JmlFile, AST, Type) - Static method in class jml2b.structure.java.Type

count the number of dimensions in the given ast.

addFields(Field) - Method in class jml2b.structure.java.Class

addGhost(Field) - Method in class jml2b.structure.java.Class

addGoal(Goal) - Method in class jml2b.pog.lemma.SimpleLemma

Adds a goal to the goal set

addGoals(SimpleLemma) - Method in class jml2b.pog.lemma.SimpleLemma

Concats two simple lemmas

addGoals(ArrayList) - Method in class jpov.structure.Lemma

addGoals(ArrayList) - Method in class jpov.structure.Method

addGoals(ArrayList) - Method in class jpov.structure.Proofs

addHyp(SimpleLemma, byte) - Method in class jml2b.pog.lemma.Proofs

Adds the goals of a lemme to the hypothesis.

addHyp(Formula, ColoredInfo, byte) - Method in class jml2b.pog.lemma.Proofs

Adds new hypothesis.

addHyp(Formula, Vector, byte) - Method in class jml2b.pog.lemma.Proofs

Adds new hypothesis.

addHyp(Formula) - Method in class jml2b.pog.lemma.Proofs

Adds new local hypothesis with no associated colored info.

addIdent(AField) - Static method in class jml2b.pog.util.IdentifierResolver

Adds a field identifier in the set of identifier.

addIdent(AClass) - Static method in class jml2b.pog.util.IdentifierResolver

Adds a class identifier in the set of identifier.

addIdent(Package) - Static method in class jml2b.pog.util.IdentifierResolver

Adds a package identifier in the set of identifier.

addImplicToGoal(Formula, byte) - Method in class jml2b.pog.lemma.Goal

Transforms the goal into an implication formula

addImplicToGoal(Formula, byte) - Method in class jml2b.pog.lemma.SimpleLemma

Transforms each goal into an implication formula

addInConjonction(Expression) - Method in class jml2b.structure.statement.Expression

addListener(ILabelProviderListener) - Method in class jack.plugin.source.MethodListLabelProvider

addModifiesWithoutDoublon(IJml2bConfiguration, GuardedModifies) - Method in class jml2b.structure.jml.ModifiesList

addPackage(Package) - Method in class jml2b.structure.java.Package

addPackages(AST, Package) - Static method in class jml2b.structure.java.JmlFile

parse a package AST clause, adding packages as needed.

addPages() - Method in class jack.plugin.source.AddJmlClauseWizard

addProof(ProofTask) - Method in class jack.plugin.prove.ProofView

Adds the given proof to the list of proofs to be performed.

addSuperFields(AClass, Vector) - Method in class jml2b.structure.java.AClass

Adds the fields defined by super classes that are visibles from the given class to the given vector.

addUnlinkedExsuresFalse(String) - Method in class jml2b.structure.jml.SpecCase

Add a exsure false clause for the given exception type fqn.

addWithoutDoublon(IJml2bConfiguration, ModifiesList) - Method in class jml2b.structure.jml.ModifiesList

and(Formula, Formula) - Static method in class jml2b.formula.Formula

Returns the conjunctive formula between the two parameters.

and(Expression, Expression) - Static method in class jml2b.structure.statement.Expression

Returns the conjonction of two expressions.

andEnumeration(Enumeration) - Static method in class jml2b.util.StatementUtils

Return an expression corresponding to the "and" of all the expression enumerated.

annotate(IJml2bConfiguration) - Method in class jml2b.structure.java.Method

annotateFiles(Vector) - Static method in class jml2b.util.FileUpdate

arithmeticException - Static variable in class jml2b.structure.statement.Statement

The Class ArithmeticException

arrayIndexOutOfBoundsException - Static variable in class jml2b.structure.statement.Statement

The Class ArrayIndexOutOfBoundsException

arrayStoreException - Static variable in class jml2b.structure.statement.Statement

The Class ArrayStoreException

arraylength - Static variable in class jml2b.formula.TerminalForm

The formula arraylength.

astprint - class jml2b.astprint.

Simple class that prints Java/JML classes.

astprint() - Constructor for class jml2b.astprint