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

E

ECLIPSE_RESOURCE_KEY - Static variable in class jack.plugin.Generator

The key that is used for storing the eclipse resource corresponding to the jml file.

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

Goal origin value that corresponds to the proof of an ensures clause.

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

Formula origin corresponding to an ensures clause of a called method

ENSURES - Static variable in class jpov.Icons

Image corresponding to the ensures icon.

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

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

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

comment indice corresponding to a ArithmeticException (red).

EQUALS_ON_OLD_INSTANCES - Static variable in interface jml2b.formula.IFormToken

Domain restriction equality operator a <| b == a <| c with priority 50.

EQUALS_ON_OLD_INSTANCES_ARRAY - Static variable in interface jml2b.formula.IFormToken

Domain restriction equality operator a <| b == a <| c with priority 50.

ERROR - Static variable in class jack.plugin.prove.ProofTask

Constant corresponding to the error state.

EVERYTHING - Static variable in class jack.plugin.JackJml2bConfiguration

EXCEPTIONAL_BEHAVIOR_CASE - Static variable in class jml2b.structure.jml.SpecCase

Constant corresponding to exceptional_behavior cases.

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

Goal origin value that corresponds to the proof of an exsures clause.

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

Formula origin corresponding to an exsures clause of a called method

EXSURES - Static variable in class jpov.Icons

Image corresponding to the exsures icon.

EXSURES_EXCEPTION_FALSE - Static variable in class jack.plugin.JackJml2bConfiguration

EXSURES_EXCEPTION_TRUE - Static variable in class jack.plugin.JackJml2bConfiguration

EXSURES_OTHER - Static variable in class jack.plugin.JackJml2bConfiguration

EXSURES_RUNTIMEEXCEPTION_FALSE - Static variable in class jack.plugin.JackJml2bConfiguration

EditAction - class jack.plugin.edit.EditAction.

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

EditAction() - Constructor for class jack.plugin.edit.EditAction

EditButton - class jack.plugin.edit.EditButton.

Button allowing to "edit" the selected JML file.

EditButton() - Constructor for class jack.plugin.edit.EditButton

ElementsForm - class jml2b.formula.ElementsForm.

This class implements terminal formulas that correspond to variables xxxelements_n, where xxx can be int, short, byte, boolean, char ou ref and n is a natural number.

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

Emitter - class jml2b.util.Emitter.

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

ErrorHandler - class jml2b.exceptions.ErrorHandler.

Interface defining how errors are reported to the user.

ErrorHandler() - Constructor for class jml2b.exceptions.ErrorHandler

ExceptionalBehaviourStack - class jml2b.pog.lemma.ExceptionalBehaviourStack.

This class describes a stack of proof obligations associated to exceptional behaviours.

ExceptionalBehaviourStack(ExceptionalProofs) - Constructor for class jml2b.pog.lemma.ExceptionalBehaviourStack

Constructs a stack with one element.

ExceptionalLemma - class jml2b.pog.lemma.ExceptionalLemma.

This class defines lemmas resulting from the proof of an exceptional method specification.

ExceptionalLemma(IJml2bConfiguration, Method, Vector, SimpleLemma, SimpleLemma, SimpleLemma) - Constructor for class jml2b.pog.lemma.ExceptionalLemma

Creates a set of exsures labelled lemma corresponding to the cases of a method specification corresponding to exceptional behaviours.

ExceptionalProofs - class jml2b.pog.lemma.ExceptionalProofs.

Class used during the PO generation to treat the proofs corresponding to exceptional behaviours.

ExceptionalProofs(Theorem) - Constructor for class jml2b.pog.lemma.ExceptionalProofs

Constructs a proof from a theorem

ExceptionalProofs(Type, Field, Proofs) - Constructor for class jml2b.pog.lemma.ExceptionalProofs

Constructs an exceptional proof from a proof catched by an exception

Expression - class jml2b.structure.statement.Expression.

This class defines a Java expression.

Exsures - class jml2b.structure.jml.Exsures.

This class implements an exsures clause, that is an exception type, a field corresponding to the exception and a property.

Exsures(Type, String, Expression) - Constructor for class jml2b.structure.jml.Exsures

Constructs an exsure clause.

ExsuresLemma - class jml2b.pog.lemma.ExsuresLemma.

This class contains the information extracted from an exsures pragma.

ExsuresLemma(Type, Field, SimpleLemma) - Constructor for class jml2b.pog.lemma.ExsuresLemma

Constructs an exsures lemma

ExsuresLemma(IJml2bConfiguration, Exsures, Expression, GoalOrigin) - Constructor for class jml2b.pog.lemma.ExsuresLemma

Constructs an exsures lemma from an exsures clause

ExsuresLemma(IJml2bConfiguration, Exsures, GoalOrigin) - Constructor for class jml2b.pog.lemma.ExsuresLemma

Constructs an exsures lemma from an exsures clause

edit(ICompilationUnit) - Static method in class jack.plugin.edit.EditAction

edit(IFile) - Static method in class jack.plugin.edit.EditAction

elements - Static variable in class jml2b.formula.ElementsForm

Array of all xxxelements_n formulas.

elements() - Method in class jml2b.link.VarStack

Returns the elements of the stack.

elementsType - Static variable in class jml2b.formula.ElementsForm

Array of type corresponding to each xxxelements_n formula.

elemtype - Static variable in class jml2b.formula.TerminalForm

The constant formula elemtype, In the B lemmas, elemtype is a function that assign the type of its element to an array instance.

emit() - Method in class jml2b.structure.bytecode.ClassField

emit() - Method in class jml2b.structure.bytecode.ClassFile

emit() - Method in class jml2b.structure.bytecode.ClassMethod

emit(IJml2bConfiguration) - Method in class jml2b.structure.java.Class

emit() - Method in class jml2b.structure.java.Field

emit() - Method in interface jml2b.structure.java.IModifiers

emit(IJml2bConfiguration) - Method in class jml2b.structure.java.JmlFile

emit() - Method in class jml2b.structure.java.Modifiers

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

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

emit() - Method in class jml2b.structure.statement.StAssert

emit() - Method in class jml2b.structure.statement.StBlock

emit() - Method in class jml2b.structure.statement.StControlFlowBreak

emit() - Method in class jml2b.structure.statement.StDoWhile

emit() - Method in class jml2b.structure.statement.StFor

emit() - Method in class jml2b.structure.statement.StIf

emit() - Method in class jml2b.structure.statement.StImplementsLabel

emit() - Method in class jml2b.structure.statement.StLabel

emit() - Method in class jml2b.structure.statement.StSequence

emit() - Method in class jml2b.structure.statement.StSkip

emit() - Method in class jml2b.structure.statement.StSpecBlock

emit() - Method in class jml2b.structure.statement.StSwitch

emit() - Method in class jml2b.structure.statement.StTry

emit() - Method in class jml2b.structure.statement.StVarDecl

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

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

empty() - Method in class jml2b.link.VarStack

Returns whether the stack is empty or not.

end() - Static method in class jml2b.pog.Pog

Clear the names in the identifier array.

ensures(IJml2bConfiguration, Theorem, ExceptionalBehaviourStack, Vector) - Method in class jml2b.structure.statement.Statement

Returns the proofs resulting where the WP calculus apply on this statement.

ensures(IJml2bConfiguration, Proofs, ExceptionalBehaviourStack) - Method in class jml2b.structure.statement.Statement

equals(Object) - Method in class jml2b.formula.BinaryForm

equals(Object) - Method in class jml2b.formula.Formula

Returns whether the formula equals the parameter.

equals(Object) - Method in class jml2b.formula.QuantifiedForm

equals(Object) - Method in class jml2b.formula.TTypeForm

equals(Object) - Method in class jml2b.formula.TerminalForm

equals(Object) - Method in class jml2b.formula.TriaryForm

equals(Object) - Method in class jml2b.formula.UnaryForm

equals(String) - Method in class jml2b.structure.java.Class

Return true iff the class "this" is equals to the class denoted by the given fully qualified name.

equals(Identifier) - Method in class jml2b.structure.java.Identifier

Indicate wether this identifier is equal to the given one.

equals(Type) - Method in class jml2b.structure.java.Type

equals(Object) - Method in class jml2b.structure.java.Type

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

equals(IJml2bConfiguration, Modifies) - Method in class jml2b.structure.jml.Modifies

equals(IJml2bConfiguration, Modifies) - Method in class jml2b.structure.jml.ModifiesDot

equals(IJml2bConfiguration, Modifies) - Method in class jml2b.structure.jml.ModifiesIdent

equals(IJml2bConfiguration, Modifies) - Method in class jml2b.structure.jml.ModifiesLbrack

equals(Object) - Method in class jml2b.structure.jml.SpecArrayDotDot

equals(Object) - Method in class jml2b.structure.jml.SpecArrayExpr

equals(Object) - Method in class jml2b.structure.jml.SpecArrayStar

equals(Expression) - Method in class jml2b.structure.statement.ArrayInitializer

equals(Expression) - Method in class jml2b.structure.statement.BinaryExp

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

Returns whether two expressions are equal.

equals(Expression) - Method in class jml2b.structure.statement.IsSubtypeOfExp

equals(Expression) - Method in class jml2b.structure.statement.MethodCallExp

equals(Expression) - Method in class jml2b.structure.statement.QuantifiedExp

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

Returns whether two lists are equal.

equals(Expression) - Method in class jml2b.structure.statement.QuestionExp

equals(Expression) - Method in class jml2b.structure.statement.TTypeExp

equals(Expression) - Method in class jml2b.structure.statement.TerminalExp

equals(Expression) - Method in class jml2b.structure.statement.UnaryExp

equals(Expression) - Method in class jml2b.structure.statement.WithTypeExp

erase() - Method in class jpov.viewer.lemma.LemmaView

Sets the input of the viewers to null

eraseColor() - Method in interface jack.plugin.perspective.ISourceCaseViewer

eraseColor() - Method in class jack.plugin.perspective.SourceCaseViewer

error(JmlFile, int, int, String) - Static method in class jml2b.exceptions.ErrorHandler

Indicate an error in the specified file, line and column.

errorDialogWithDetails(Shell, String, String, String, String) - Static method in class jpov.JpovError

Displays an error dialog with details

errorMessage(String) - Method in class jack.plugin.perspective.CaseExplorer

Display the following error message using the appropriate title window.

exactMatch(Vector) - Method in class jml2b.structure.AMethod

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

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

exactMatch(Vector) - Method in class jml2b.structure.java.Method

Returns true if the given method has exactly the same signature as the given vector of types.

exprToForm(IJml2bConfiguration) - Method in class jml2b.structure.statement.Expression

Converts the expression into a formula.

exsureVectorInstancie(Enumeration) - Static method in class jml2b.structure.jml.SpecCase

Instancie the exsures clause.

exsureVectorProcessIdent(Enumeration) - Static method in class jml2b.structure.jml.SpecCase

Collects all the indentifier of the exsures clause to give them an index in the identifer array.

exsureVectorRenameParam(Enumeration, Parameters, Parameters) - Static method in class jml2b.structure.jml.SpecCase