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

L

LEMMA_VIEWER - Static variable in class jack.plugin.JackPlugin

The Id corresponding to

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

Constant corresponding to lightweight cases.

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

Constant corresponding to the loading state.

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

Formula origin corresponding to a local hypothese

LOCALES - Static variable in class jpov.Icons

Image corresponding to the local icon for hypothesis.

LOCAL_ELEMENTS_DECL - Static variable in interface jml2b.formula.IFormToken

Local xxxelements declaration corresponding formally to a B_IN

LOCAL_VAR_DECL - Static variable in interface jml2b.formula.IFormToken

Local variable declaration corresponding formally to a B_IN

LOCK - Static variable in class jack.plugin.JackPlugin

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

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

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

Formula origin corresponding to a loop exsures

LOOP_EXSURES - Static variable in class jpov.Icons

Image corresponding to the loop exsures icon.

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

Formula origin corresponding to a loop invariant

LOOP_INVARIANT - Static variable in class jpov.Icons

Image corresponding to the loop invariant icon.

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

Goal origin value that corresponds to the proof of the initialization of a loop invariant.

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

Goal origin value that corresponds to the proof of the preservation of a loop invariant.

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

Goal origin value that corresponds to the proof of a loop variant.

LabeledProofsVector - class jml2b.pog.lemma.LabeledProofsVector.

This class provides a set of LabeledProofs.

LabeledProofsVector() - Constructor for class jml2b.pog.lemma.LabeledProofsVector

Constructs an empty set.

LanguageException - exception jml2b.exceptions.LanguageException.

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

Languages - class jml2b.languages.Languages.

This class allows to register plugins into Jack.

Languages() - Constructor for class jml2b.languages.Languages

Lemma - class jml2b.pog.lemma.Lemma.

This class defines a lemma.

Lemma() - Constructor for class jml2b.pog.lemma.Lemma

Lemma - class jpov.structure.Lemma.

This class implements a node tree corresponding to a case.

LemmaFilterWindow - class jpov.viewer.lemma.LemmaFilterWindow.

This class displays the filter window that allow to filter hypotheses

LemmaFilterWindow(Shell, Hashtable) - Constructor for class jpov.viewer.lemma.LemmaFilterWindow

Constructs a filter window into the current shell.

LemmaHierarchy - class jpov.structure.LemmaHierarchy.

LemmaSorter - class jpov.viewer.lemma.LemmaSorter.

The class implements a sorter for the hypothesis viewer

LemmaSorter(LemmaFilterWindow) - Constructor for class jpov.viewer.lemma.LemmaSorter

Constructs a lemma filter

LemmaView - class jpov.viewer.lemma.LemmaView.

This class implements the part of the viewer that displays the lemmas in different languages.

LemmaView(IJml2bConfiguration, Composite, boolean) - Constructor for class jpov.viewer.lemma.LemmaView

Constructs the part of the view that displays the lemma

LemmaViewer - class jack.plugin.perspective.LemmaViewer.

View displaying a lemma.

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

LinkContext - class jml2b.link.LinkContext.

LinkContext(JmlFile) - Constructor for class jml2b.link.LinkContext

LinkContext(AClass) - Constructor for class jml2b.link.LinkContext

LinkContext(LinkContext, LinkInfo) - Constructor for class jml2b.link.LinkContext

LinkException - exception jml2b.exceptions.LinkException.

LinkException(String, ParsedItem) - Constructor for class jml2b.exceptions.LinkException

LinkInfo - class jml2b.link.LinkInfo.

LinkInfo(Package) - Constructor for class jml2b.link.LinkInfo

LinkInfo(Type) - Constructor for class jml2b.link.LinkInfo

LinkUtils - class jml2b.link.LinkUtils.

LinkUtils() - Constructor for class jml2b.link.LinkUtils

Linkable - interface jml2b.link.Linkable.

LoadAndLink - class jack.plugin.source.LoadAndLink.

Action that loads end links a JML file.

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

LoadException - exception jml2b.exceptions.LoadException.

This class provides an exception that can be threw during the load of a JPO file.

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

Constructs an exception when a given message.

lemmas - Variable in class jml2b.structure.java.Method

lineGetStyle(LineStyleEvent) - Method in class jack.plugin.edit.JavaLineStyler

Event.detail line start offset (input) Event.text line text (input) LineStyleEvent.styles Enumeration of StyleRanges, need to be in order.

link(IJml2bConfiguration, LinkContext) - Method in interface jml2b.link.Linkable

link(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.bytecode.ClassField

link(IJml2bConfiguration) - Method in class jml2b.structure.bytecode.ClassFile

link(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.bytecode.ClassFile

link(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.bytecode.ClassMethod

link(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.java.Class

Link the externally visible parts of the class.

link(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.java.Field

link(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.java.Invariant

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

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

link(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.java.Parameters

link(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.java.Type

link(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.java.VarDeclParser

link(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.jml.Depends

link(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.jml.Exsures

link(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.jml.Represents

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

link(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.statement.Statement

linkEnumeration(IJml2bConfiguration, Enumeration, LinkContext) - Static method in class jml2b.link.LinkUtils

Links all the Linkable elements provided by the enumeration e using LinkContext f.

linkFieldIdent(IJml2bConfiguration, LinkContext, ParsedItem) - Method in class jml2b.structure.java.Identifier

linkMethod(IJml2bConfiguration, LinkContext, Vector) - Method in class jml2b.structure.statement.Expression

Links a method call.

linkParameters(IJml2bConfiguration, LinkContext, Vector) - Method in class jml2b.structure.statement.Expression

Links the parameters list of a method call and the resulting type to the parameters vector.

linkStatement(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.statement.ArrayInitializer

linkStatement(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.statement.BinaryExp

linkStatement(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.statement.IsSubtypeOfExp

linkStatement(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.statement.MethodCallExp

linkStatement(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.statement.QuantifiedExp

linkStatement(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.statement.QuestionExp

linkStatement(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.statement.StAssert

Links the asserted predicate

linkStatement(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.statement.StBlock

linkStatement(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.statement.StControlFlowBreak

linkStatement(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.statement.StDoWhile

linkStatement(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.statement.StFor

linkStatement(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.statement.StIf

linkStatement(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.statement.StImplementsLabel

linkStatement(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.statement.StLabel

linkStatement(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.statement.StLoops

linkStatement(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.statement.StSequence

linkStatement(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.statement.StSkip

linkStatement(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.statement.StSpecBlock

linkStatement(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.statement.StSwitch

linkStatement(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.statement.StTry

linkStatement(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.statement.StVarDecl

linkStatement(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.statement.Statement

Links the statement.

linkStatement(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.statement.TTypeExp

linkStatement(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.statement.TerminalExp

linkStatement(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.statement.UnaryExp

linkStatement(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.statement.WithTypeExp

linkStatements(IJml2bConfiguration, Enumeration, LinkContext) - Static method in class jml2b.link.LinkUtils

linkStatements(IJml2bConfiguration, LinkContext) - Method in interface jml2b.link.Linkable

linkStatements(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.bytecode.ClassField

linkStatements(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.bytecode.ClassFile

linkStatements(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.bytecode.ClassMethod

linkStatements(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.java.Class

Link the parts that cannot be directly referenced from the outside.

linkStatements(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.java.Field

linkStatements(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.java.Invariant

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

Links the statement parts of the file if needed.

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

Links statements for all the remaining files.

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

linkStatements(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.java.Parameters

linkStatements(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.java.Type

linkStatements(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.java.VarDeclParser

linkStatements(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.jml.Depends

linkStatements(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.jml.Exsures

linkStatements(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.jml.ModifiesClause

Links the content of the clause.

linkStatements(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.jml.ModifiesEverything

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

linkStatements(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.jml.ModifiesNothing

linkStatements(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.jml.Represents

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

linkStatements(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.statement.Statement

linkVars - Variable in class jml2b.link.LinkContext

Stack of local variables used for linking

load(JpoInputStream) - Method in interface jml2b.languages.ILanguage

Load a terminal formula from a jpo file.

load(JpoInputStream) - Method in class jml2b.languages.java.JavaLanguage

loadAstImage(IJml2bConfiguration, String) - Static method in class jml2b.Jml2b

loadClass(IJml2bConfiguration, String) - Static method in class jml2b.Serializer

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

Returns the class name from package p.

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

Load the given class, creating the package as needed.

loadClass(IJml2bConfiguration, boolean) - Method in class jml2b.util.JmlClassEntryFile

loadClass(IJml2bConfiguration, boolean) - Method in class jml2b.util.JmlFileEntry

loadClass(IJml2bConfiguration, boolean) - Method in class jml2b.util.JmlSourceEntryFile

loadDefaultClasses() - Method in class jack.plugin.Generator

Loads the default classes.

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

Loads the default classes (ensures that they are loaded)

loadFile(boolean) - Method in class jml2b.util.JmlSourceEntryFile

/** Load the given Java/JML file and return a new JmlFile structure

loadFileImage(String) - Static method in class jml2b.Jml2b

Restore the JmlFile array as well as the system packages from the given file.

loadFiles(IJml2bConfiguration, String[]) - Static method in class jml2b.Jml2b

Loads files from args.

loadFiles(IJml2bConfiguration, String[], int) - Static method in class jml2b.Jml2b

Loads the file_count files from args.

loadJmlFile(IJml2bConfiguration, String) - Static method in class jpov.JpoFile

Loads a JPO file

loadJmlFile(IJml2bConfiguration, File, JpoInputStream) - Static method in class jpov.structure.JmlFile

Loads the root node from a .jpo file

loadJpoFile(IFile) - Static method in class jack.plugin.JpovUtil

Load a Jpov object from the given .jpo file.

loadPartialJpoFile(IFile) - Static method in class jack.plugin.JpovUtil

loadProperties() - Static method in class jml2b.Jml2b

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

Loads classes from the given serialized image.

loadedFilesCount - Static variable in class jml2b.structure.java.JmlFile

lock(IResource) - Static method in class jack.plugin.JackPlugin

lookupMethod(IJml2bConfiguration, String, Vector) - Method in class jml2b.structure.java.AClass

Search the given method in the class and superclass methods.

lookupMethodClass(IJml2bConfiguration, String, Vector, AMethod) - Method in class jml2b.structure.java.AClass

Lookup the given method in the current class (which is not an interface).

lookupMethodCurrentClass(IJml2bConfiguration, String, Vector, AMethod) - Method in class jml2b.structure.bytecode.ClassFile

lookupMethodCurrentClass(IJml2bConfiguration, String, Vector, AMethod) - Method in class jml2b.structure.java.AClass

lookupMethodCurrentClass(IJml2bConfiguration, String, Vector, AMethod) - Method in class jml2b.structure.java.Class

Search for a method looking only in the current class (or interface).

lookupMethodInterface(IJml2bConfiguration, String, Vector, AMethod) - Method in class jml2b.structure.java.AClass

Lookup the given method in the current interface (which is not class).