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

C

CASE_EXPLORER_VIEW_ID - Static variable in class jack.plugin.JackPlugin

The Id corresponding to

CHECKED - Static variable in class jpov.Icons

Image corresponding to the checked icon.

COMPILED_DESCRIPTOR - Static variable in class jpov.Icons

CONSTANT_FUNCTION - Static variable in interface jml2b.formula.IFormToken

constant function a * {b} with priority 200.

CONSTANT_FUNCTION_FUNCTION - Static variable in interface jml2b.formula.IFormToken

constant function function a * {b * {c}} with priority 200.

CaseExplorer - class jack.plugin.perspective.CaseExplorer.

View containing the cases explorer.

CaseExplorer() - Constructor for class jack.plugin.perspective.CaseExplorer

Class - class jml2b.structure.java.Class.

Internal representation of classes.

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

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

Creates a new class in package class_package, with the given modifiers.

Class(String, Proofs, Proofs, Vector, Vector) - Constructor for class jml2b.structure.java.Class

Creates a new class.

Class - class jpov.structure.Class.

This class implements a node tree corresponding to a class.

ClassDefaultConstructor - class jml2b.structure.bytecode.ClassDefaultConstructor.

ClassDefaultConstructor(ClassFile) - Constructor for class jml2b.structure.bytecode.ClassDefaultConstructor

ClassField - class jml2b.structure.bytecode.ClassField.

ClassField(Field, ClassFile) - Constructor for class jml2b.structure.bytecode.ClassField

ClassFile - class jml2b.structure.bytecode.ClassFile.

ClassFile(JavaClass) - Constructor for class jml2b.structure.bytecode.ClassFile

ClassLoadException - exception jml2b.exceptions.ClassLoadException.

ClassLoadException(String) - Constructor for class jml2b.exceptions.ClassLoadException

ClassMethod - class jml2b.structure.bytecode.ClassMethod.

ClassMethod(Method, ClassFile) - Constructor for class jml2b.structure.bytecode.ClassMethod

ClassParameters - class jml2b.structure.bytecode.ClassParameters.

ClassParameters(IJml2bConfiguration, Method) - Constructor for class jml2b.structure.bytecode.ClassParameters

ClassParameters() - Constructor for class jml2b.structure.bytecode.ClassParameters

ClassResolver - class jml2b.pog.printers.ClassResolver.

ClassResolver() - Constructor for class jml2b.pog.printers.ClassResolver

Constructs a file printer.

ColoredInfo - class jml2b.pog.util.ColoredInfo.

This class defines informations associated to formula in order to color the code in the viewer.

ColoredInfo() - Constructor for class jml2b.pog.util.ColoredInfo

Constructs a colored info with no coloration.

ColoredInfo(ParsedItem) - Constructor for class jml2b.pog.util.ColoredInfo

Constructs a green colored info

ColoredInfo(ParsedItem, byte) - Constructor for class jml2b.pog.util.ColoredInfo

Constructs a red colored info or a blue without additional informations.

ColoredInfo(ParsedItem, byte, String) - Constructor for class jml2b.pog.util.ColoredInfo

Constructs a blue colored info with informations.

CompilationUnitDecorator - class jack.plugin.compile.CompilationUnitDecorator.

Decorator allowing to add annotations to the name of the Java files.

CompilationUnitDecorator() - Constructor for class jack.plugin.compile.CompilationUnitDecorator

CompileButton - class jack.plugin.compile.CompileButton.

Action allowing to compile

CompileButton() - Constructor for class jack.plugin.compile.CompileButton

CompileMessageDialog - class jack.plugin.compile.CompileMessageDialog.

This class defines a dialog that indicates that some files need to be recompiled.

Constraint - class jml2b.structure.java.Constraint.

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

Constructor - class jml2b.structure.java.Constructor.

Specialisation of the Method class suitable for representing constructors.

ConstructorPO - class jml2b.pog.proofobligation.ConstructorPO.

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

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

Constructs a proof obligation

ContextFromPureMethod - class jml2b.pog.util.ContextFromPureMethod.

This class contains the context issued from pure method that is used when translating an expression into a formula.

ContextFromPureMethod(Formula) - Constructor for class jml2b.pog.util.ContextFromPureMethod

Constructs a context form a formula, the context is empty.

ContextFromPureMethod(ContextFromPureMethod, Formula) - Constructor for class jml2b.pog.util.ContextFromPureMethod

Constructs a context from an existing context and a formula.

ContextFromPureMethod(String, Formula, Type, Formula) - Constructor for class jml2b.pog.util.ContextFromPureMethod

Constructs a context from a method call without parameter.

ContextFromPureMethod(ContextFromPureMethod, String, Formula, Type, Formula) - Constructor for class jml2b.pog.util.ContextFromPureMethod

Constructs a context from a method call with parameter.

ContextFromPureMethod(ContextFromPureMethod, ContextFromPureMethod, Formula) - Constructor for class jml2b.pog.util.ContextFromPureMethod

Constructs a context from the translation of a binary operator.

ContextFromPureMethod(ContextFromPureMethod, ContextFromPureMethod, ContextFromPureMethod, Formula) - Constructor for class jml2b.pog.util.ContextFromPureMethod

Constructs a context from the translation of a 3-ary operator.

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

catchException(Type, Field) - Method in class jml2b.pog.lemma.Lemma

Returns the lemma corresponding to the current lemma encapsulated in the fact that it corresponds to a catch of an exception.

catchException(Type, Field) - Method in class jml2b.pog.lemma.NormalLemma

Creates an exceptional lemma set from the current one and a catched type with a catched parameter.

catchException(Type, Field) - Method in class jml2b.pog.lemma.SimpleLemma

Returns an exsures lemma

catches(AClass) - Method in class jml2b.pog.lemma.ExceptionalLemma

catches(AClass) - Method in class jml2b.pog.lemma.ExsuresLemma

catches(AClass) - Method in class jml2b.pog.lemma.Lemma

Returns whether a exsures lemma catches a given exception.

change(ParsedItem) - Method in class jml2b.structure.java.ParsedItem

change(Vector) - Method in class jml2b.structure.java.ParsedItem

charelements - Static variable in class jml2b.formula.ElementsForm

The formula charelements_n.

checkDirectory(IJml2bConfiguration, String) - Static method in class jml2b.structure.java.JmlLoader

Checks that the given directory exists within the search path.

checkDirectory(String) - Method in class jml2b.util.JmlPathDirectory

checkDirectory(String) - Method in class jml2b.util.JmlPathEntry

checkDirectory(String) - Method in class jml2b.util.JmlPathJar

checkFields(boolean) - Method in class jack.plugin.JackDefaultSpecEditor

Checks that the text fields contains parseable JML.

checkFile(File) - Method in class jml2b.util.JmlPathDirectory

checkFile(File) - Method in class jml2b.util.JmlPathEntry

checkFile(File) - Method in class jml2b.util.JmlPathJar

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

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

The Class ClassCastException

classExists(String, String[]) - Static method in class jml2b.structure.java.JmlLoader

Return true iff the given class exists in the given search path.

clearAll() - Static method in class jml2b.structure.java.Class

Clear all classes that could have been instanciated.

clearAll() - Static method in class jml2b.structure.java.JmlLoader

Remove any unlinked file from the unlinkedFiles stack.

clearAll() - Static method in class jml2b.structure.java.Package

Unload all the loaded packages.

clearAll() - Static method in class jml2b.structure.java.Type

Sets typeObject to null.

clearBoxes() - Method in class jack.plugin.edit.JavaLineStyler

clearFlag(int) - Method in class jml2b.structure.java.Modifiers

Clear the given flag(s).

clearNName() - Method in class jml2b.pog.util.IdentifierResolver

Clear the name index.

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

Clear the name index of all the named node of the identifier set.

clearName() - Method in class jml2b.structure.java.NamedNode

clear all the names of the named node.

clearSuffix() - Static method in class jml2b.formula.ElementsForm

Resets all the suffix of the xxxelements_n formula to 0.

clearViewedFile(ICompilationUnit) - Method in class jack.plugin.perspective.CaseExplorer

Clear the viewed file.

clone() - Method in class jml2b.formula.BinaryForm

Clones the formula

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

Clones the formula.

clone() - Method in class jml2b.formula.QuantifiedForm

clone() - Method in class jml2b.formula.QuantifiedVarForm

Clones the quantified variables

clone() - Method in class jml2b.formula.TTypeForm

clone() - Method in class jml2b.formula.TerminalForm

clone() - Method in class jml2b.formula.TriaryForm

clone() - Method in class jml2b.formula.UnaryForm

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

Clones the stack

clone() - Method in class jml2b.pog.lemma.ExceptionalLemma

clone() - Method in class jml2b.pog.lemma.ExceptionalProofs

Clones a proof.

clone() - Method in class jml2b.pog.lemma.ExsuresLemma

clone() - Method in class jml2b.pog.lemma.Goal

Clones the goal

clone() - Method in class jml2b.pog.lemma.Lemma

Clones a lemma.

clone() - Method in class jml2b.pog.lemma.NormalLemma

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

Clones a proof.

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

Clones the simple lemma

clone() - Method in class jml2b.pog.lemma.Theorem

Clone the theorem

clone() - Method in class jml2b.pog.lemma.TheoremList

Clones the theorem list

clone() - Method in class jml2b.pog.substitution.SubArrayElement

clone() - Method in class jml2b.pog.substitution.SubArrayElementSingle

clone() - Method in class jml2b.pog.substitution.SubArrayLength

clone() - Method in class jml2b.pog.substitution.SubForm

clone() - Method in class jml2b.pog.substitution.SubInstances

clone() - Method in class jml2b.pog.substitution.SubInstancesSet

clone() - Method in class jml2b.pog.substitution.SubInstancesSingle

clone() - Method in class jml2b.pog.substitution.SubMemberField

clone() - Method in class jml2b.pog.substitution.SubStaticOrLocalField

clone() - Method in class jml2b.pog.substitution.SubTmpVar

clone() - Method in class jml2b.pog.substitution.SubTypeof

clone() - Method in class jml2b.pog.substitution.SubTypeofSet

clone() - Method in class jml2b.pog.substitution.SubTypeofSingle

clone() - Method in interface jml2b.pog.substitution.Substitution

Clones the substitution.

clone() - Method in class jml2b.structure.jml.Exsures

clone() - Method in class jml2b.structure.jml.GuardedModifies

clone() - Method in interface jml2b.structure.jml.JmlExpression

clone() - Method in class jml2b.structure.jml.Modifies

Clones the modified variable.

clone() - Method in class jml2b.structure.jml.ModifiesClause

Clones the object.

clone() - Method in class jml2b.structure.jml.ModifiesDot

clone() - Method in class jml2b.structure.jml.ModifiesEverything

clone() - Method in class jml2b.structure.jml.ModifiesIdent

clone() - Method in class jml2b.structure.jml.ModifiesLbrack

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

Clones the list.

clone() - Method in class jml2b.structure.jml.ModifiesNothing

clone() - Method in class jml2b.structure.jml.Represents

clone() - Method in class jml2b.structure.jml.SpecArray

Clones the indexes set.

clone() - Method in class jml2b.structure.jml.SpecArrayDotDot

clone() - Method in class jml2b.structure.jml.SpecArrayExpr

clone() - Method in class jml2b.structure.jml.SpecArrayStar

clone() - Method in class jml2b.structure.jml.SpecCase

clone() - Method in class jml2b.structure.statement.ArrayInitializer

Clones the array initializer

clone() - Method in class jml2b.structure.statement.BinaryExp

clone() - Method in class jml2b.structure.statement.IsSubtypeOfExp

clone() - Method in class jml2b.structure.statement.MethodCallExp

clone() - Method in class jml2b.structure.statement.QuantifiedExp

clone() - Method in class jml2b.structure.statement.QuantifiedVar

Clones the list of quantified fields

clone() - Method in class jml2b.structure.statement.QuestionExp

clone() - Method in class jml2b.structure.statement.Statement

clone() - Method in class jml2b.structure.statement.TTypeExp

clone() - Method in class jml2b.structure.statement.TerminalExp

clone() - Method in class jml2b.structure.statement.UnaryExp

clone() - Method in class jml2b.structure.statement.WithTypeExp

close() - Method in class jml2b.util.JpoOutputStream

close() - Method in class jpov.JpoFile

collectCalledMethod(Vector) - Method in class jml2b.structure.statement.ArrayInitializer

collectCalledMethod(Vector) - Method in class jml2b.structure.statement.BinaryExp

collectCalledMethod(Vector) - Method in class jml2b.structure.statement.IsSubtypeOfExp

collectCalledMethod(Vector) - Method in class jml2b.structure.statement.MethodCallExp

collectCalledMethod(Vector) - Method in class jml2b.structure.statement.QuantifiedExp

collectCalledMethod(Vector) - Method in class jml2b.structure.statement.QuestionExp

collectCalledMethod(Vector) - Method in class jml2b.structure.statement.StAssert

collectCalledMethod(Vector) - Method in class jml2b.structure.statement.StBlock

collectCalledMethod(Vector) - Method in class jml2b.structure.statement.StControlFlowBreak

collectCalledMethod(Vector) - Method in class jml2b.structure.statement.StDoWhile

collectCalledMethod(Vector) - Method in class jml2b.structure.statement.StFor

collectCalledMethod(Vector) - Method in class jml2b.structure.statement.StIf

collectCalledMethod(Vector) - Method in class jml2b.structure.statement.StImplementsLabel

collectCalledMethod(Vector) - Method in class jml2b.structure.statement.StLabel

collectCalledMethod(Vector) - Method in class jml2b.structure.statement.StSequence

collectCalledMethod(Vector) - Method in class jml2b.structure.statement.StSkip

collectCalledMethod(Vector) - Method in class jml2b.structure.statement.StSpecBlock

collectCalledMethod(Vector) - Method in class jml2b.structure.statement.StSwitch

collectCalledMethod(Vector) - Method in class jml2b.structure.statement.StTry

collectCalledMethod(Vector) - Method in class jml2b.structure.statement.StVarDecl

collectCalledMethod(Vector) - Method in class jml2b.structure.statement.Statement

collectCalledMethod(Vector) - Method in class jml2b.structure.statement.TTypeExp

collectCalledMethod(Vector) - Method in class jml2b.structure.statement.TerminalExp

collectCalledMethod(Vector) - Method in class jml2b.structure.statement.UnaryExp

collectCalledMethod(Vector) - Method in class jml2b.structure.statement.WithTypeExp

coloredInfos(Vector, byte) - Static method in class jml2b.pog.lemma.SimpleLemma

Returns the set of ColoredInfo construct from a set of ParsedItem

compare(Object, Object) - Method in class jml2b.util.FileUpdateComparator

compare(Viewer, Object, Object) - Method in class jpov.viewer.lemma.LemmaSorter

If the two lines have the same origin, compare their nums, otherwise compare their origins.

compare(Viewer, Object, Object) - Method in class jpov.viewer.tree.TreeSorter

Compares two nodes.

compile(ICompilationUnit) - Static method in class jack.plugin.compile.PoGenerator

compileRessources(ICompilationUnit, IWorkbenchPart, String, String) - Static method in class jack.plugin.compile.CompileMessageDialog

completeModifiesWithFields(ModifiesList) - Method in class jml2b.structure.jml.ModifiesClause

completeModifiesWithFields(ModifiesList) - Method in class jml2b.structure.jml.ModifiesEverything

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

completeModifiesWithFields(ModifiesList) - Method in class jml2b.structure.jml.ModifiesNothing

completeModifiesWithOwnFields(IJml2bConfiguration) - Method in class jml2b.structure.java.Constructor

completeModifiesWithOwnFields(ModifiesList) - Method in class jml2b.structure.jml.SpecCase

Complete the modifies clause of a constructor with the fields of the class.

completeSpecCase(IJml2bConfiguration, Expression, Vector, Modifiers, Modifiers, int) - Method in class jml2b.structure.jml.SpecCase

Completes the modifies, if no modifies were declared, the modifies becomes a modifies \everything

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

Constructors defined by the current class.

contains(Vector) - Method in class jml2b.formula.BinaryForm

contains(Vector) - Method in class jml2b.formula.Formula

contains(Vector) - Method in class jml2b.formula.QuantifiedForm

contains(Vector) - Method in class jml2b.formula.TTypeForm

contains(Vector) - Method in class jml2b.formula.TerminalForm

contains(Vector) - Method in class jml2b.formula.TriaryForm

contains(Vector) - Method in class jml2b.formula.UnaryForm

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

contentChanged() - Method in class jack.plugin.metrics.MetricsContentProvider

Called by the ProofList when its content changes.

contentChanged() - Method in class jack.plugin.prove.ProofContentProvider

Called by the ProofList when its content changes.

countTokens(String, String) - Static method in class jml2b.util.Util

Returns the number of parts into a given string

create(IJml2bConfiguration, JpoInputStream, IJmlFile) - Static method in class jml2b.formula.Formula

Create a formula from a token read into a stream.

create(JmlFile, AST) - Static method in class jml2b.structure.jml.ModifiesClause

Create a concrete modifies clause depending of the AST content

create(JmlFile, AST, Modifiers, Class) - Static method in class jml2b.structure.jml.Represents

Creates an empty represent clause from a loaded file.

createAndCheckSubPackage(IJml2bConfiguration, String) - Method in class jml2b.structure.java.Package

Check that the package name exists and create the subpackage if it does.

createDialogArea(Composite) - Method in class jack.plugin.ImageContentEditor

Creates the widgets corresponding to the editor.

createE(JmlFile, AST) - Static method in class jml2b.structure.statement.Expression

Creates an expression from an AST node.

createFieldEditors() - Method in class jack.plugin.JackPreferencePage

Creates the field editors.

createFieldEditors() - Method in class jack.plugin.JackPreferencePageCompiler

Creates the field editors.

createFieldEditors() - Method in class jack.plugin.JackPreferencePageEditor

Creates the field editors.

createFieldEditors() - Method in class jack.plugin.JackPreferencePageProvers

Creates the field editors.

createInitialLayout(IPageLayout) - Method in class jack.plugin.perspective.JackPerspective

createPartControl(Composite) - Method in class jack.plugin.metrics.MetricsView

createPartControl(Composite) - Method in class jack.plugin.perspective.CaseExplorer

createPartControl(Composite) - Method in class jack.plugin.perspective.LemmaViewer

createPartControl(Composite) - Method in class jack.plugin.perspective.SourceCaseViewer

createPartControl(Composite) - Method in class jack.plugin.prove.ProofView

createS(JmlFile, AST) - Static method in class jml2b.structure.statement.Statement

Creates a statement from an AST.

createSubPackage(String) - Method in class jml2b.structure.java.Package

createUnlinkedClass(String) - Static method in class jml2b.structure.java.Type

Creates an unlinked type element corresponding to the given fully qualified class name.

createWidgets(Composite) - Method in class jack.plugin.JackDefaultSpecEditor

createWidgets(Composite) - Method in class jack.plugin.JackPathEditor

currentClass - Variable in class jml2b.link.LinkContext

currentMethod - Variable in class jml2b.link.LinkContext

currentPackage - Variable in class jml2b.link.LinkContext