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

J

JACK_DIR_PROPERTY - Static variable in class jack.plugin.JackPlugin

JACK_GENERATE - Static variable in class jack.plugin.JackPlugin

JACK_METRICS_VIEW_ID - Static variable in class jack.plugin.JackPlugin

The Id corresponding to the Jack Metrics view.

JACK_OBVIOUS_PO - Static variable in class jack.plugin.JackPlugin

JACK_PERSPECTIVE_ID - Static variable in class jack.plugin.JackPlugin

JACK_PROOF_TASK_MAX_RUNNING - Static variable in class jack.plugin.JackPlugin

JACK_PROOF_VIEW_ID - Static variable in class jack.plugin.JackPlugin

The Id corresponding to the Jack Prover view.

JACK_SUBDIRECTORY - Static variable in class jack.plugin.JackPlugin

Directory used to store the jpo files.

JACK_VIEWER_FONT - Static variable in class jack.plugin.JackPlugin

Font used within the source viewer.

JACK_VIEW_ID - Static variable in class jack.plugin.JackPlugin

The Id corresponding to the Jack PO Viewer view.

JACK_VIEW_SHOW - Static variable in class jack.plugin.JackPlugin

Boolean preference indicating wether a view should be displayed.

JACK_WELLDEF_LEMMA - Static variable in class jack.plugin.JackPlugin

JMLPATH_PREFERENCE - Static variable in class jack.plugin.JackPlugin

Preference corresponding to the search path used when loading files.

JML_COMPILED - Static variable in class jack.plugin.JackPlugin

The property corresponding to the fact that a file is compiled or not.

JML_KEYWORD_COLOR - Static variable in class jack.plugin.JackPlugin

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

.jpo file

Ja_ADD_OP - Static variable in interface jml2b.formula.IFormToken

Additive binary operator a + b with priority 180.

Ja_AND_OP - Static variable in interface jml2b.formula.IFormToken

Conjonction binary operator a && b with priority 40.

Ja_CHAR_LITERAL - Static variable in interface jml2b.formula.IFormToken

Character literal with priority 250.

Ja_COMMA - Static variable in interface jml2b.formula.IFormToken

Comma binary operator a , b with priority 70.

Ja_DIFFERENT_OP - Static variable in interface jml2b.formula.IFormToken

Different binary operator a != b with priority 50.

Ja_DIV_OP - Static variable in interface jml2b.formula.IFormToken

Division binary operator a / b with priority 190.

Ja_EQUALS_OP - Static variable in interface jml2b.formula.IFormToken

Equality binary operator a == b with priority 50.

Ja_GE_OP - Static variable in interface jml2b.formula.IFormToken

Greater or equal binary operator a >= b with priority 50.

Ja_GREATER_OP - Static variable in interface jml2b.formula.IFormToken

Strictly greater binary operator a > b with priority 50.

Ja_IDENT - Static variable in interface jml2b.formula.IFormToken

Identifier a with priority 250.

Ja_JAVA_BUILTIN_TYPE - Static variable in interface jml2b.formula.IFormToken

Java builtin type with priority 250.

Ja_LESS_OP - Static variable in interface jml2b.formula.IFormToken

Strictly less binary operator a < b with priority 50.

Ja_LE_OP - Static variable in interface jml2b.formula.IFormToken

Less or equal binary operator a <= b with priority 50.

Ja_LITERAL_false - Static variable in interface jml2b.formula.IFormToken

Literal false with priority 250.

Ja_LITERAL_null - Static variable in interface jml2b.formula.IFormToken

Literal null with priority 250.

Ja_LITERAL_super - Static variable in interface jml2b.formula.IFormToken

Literal super with priority 250.

Ja_LITERAL_this - Static variable in interface jml2b.formula.IFormToken

Literal this with priority 250.

Ja_LITERAL_true - Static variable in interface jml2b.formula.IFormToken

Literal true with priority 250.

Ja_LNOT - Static variable in interface jml2b.formula.IFormToken

Negation unary operator !a with priority 250.

Ja_MOD - Static variable in interface jml2b.formula.IFormToken

Modulo binary operator a mod b with priority 190.

Ja_MUL_OP - Static variable in interface jml2b.formula.IFormToken

Multiplicative binary operator a * b with priority 190.

Ja_NEGATIVE_OP - Static variable in interface jml2b.formula.IFormToken

Minus binary operator a - b with priority 180.

Ja_NUM_INT - Static variable in interface jml2b.formula.IFormToken

Integer literal with priority 250.

Ja_OR_OP - Static variable in interface jml2b.formula.IFormToken

Disjonctive binary operator a || b with priority 40.

Ja_QUESTION - Static variable in interface jml2b.formula.IFormToken

Question tri-ary operator a ? b : c with priority 90.

Ja_STRING_LITERAL - Static variable in interface jml2b.formula.IFormToken

String literal "aaa" with priority 250.

Ja_UNARY_NUMERIC_OP - Static variable in interface jml2b.formula.IFormToken

Unary minus operator -a with priority 210.

JackDefaultSpecEditor - class jack.plugin.JackDefaultSpecEditor.

Control allowing to edit the default values added when clauses are not specified.

JackDefaultSpecEditor(Shell) - Constructor for class jack.plugin.JackDefaultSpecEditor

JackJml2bConfiguration - class jack.plugin.JackJml2bConfiguration.

This class represents a configuration extracted from the Jack plugin and used to compile, edit and prove jml files.

JackJml2bConfiguration(IProject) - Constructor for class jack.plugin.JackJml2bConfiguration

Creates a new JackJml2bConfiguration suitable for use with the given project.

JackPathEditor - class jack.plugin.JackPathEditor.

A dialog that allows editing a list of paths.

JackPathEditor(Shell, JackProjectPropertyPage) - Constructor for class jack.plugin.JackPathEditor

JackPerspective - class jack.plugin.perspective.JackPerspective.

The Jack perspective.

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

JackPlugin - class jack.plugin.JackPlugin.

Eclipse plugin for the Java Applet Correctness Kit.

JackPlugin(IPluginDescriptor) - Constructor for class jack.plugin.JackPlugin

The constructor.

JackPreferencePage - class jack.plugin.JackPreferencePage.

This class defines the Preferences page for Jack, the Java Applets Correctness Kit.

JackPreferencePage() - Constructor for class jack.plugin.JackPreferencePage

Creates the JackPreferencePage.

JackPreferencePageCompiler - class jack.plugin.JackPreferencePageCompiler.

This class implements the preference page for the compiler.

JackPreferencePageCompiler() - Constructor for class jack.plugin.JackPreferencePageCompiler

Creates the JackPreferencePage for the compiler.

JackPreferencePageEditor - class jack.plugin.JackPreferencePageEditor.

This class implements the preference page for the editor.

JackPreferencePageEditor() - Constructor for class jack.plugin.JackPreferencePageEditor

Creates the JackPreferencePage for the editor.

JackPreferencePageProvers - class jack.plugin.JackPreferencePageProvers.

This class implements the generic preference page for the provers.

JackPreferencePageProvers() - Constructor for class jack.plugin.JackPreferencePageProvers

Creates the JackPreferencePage for provers settings.

JackProjectPropertyPage - class jack.plugin.JackProjectPropertyPage.

Property page for Java projects.

JackProjectPropertyPage() - Constructor for class jack.plugin.JackProjectPropertyPage

JavaBinaryForm - class jml2b.languages.java.JavaBinaryForm.

JavaLanguage - class jml2b.languages.java.JavaLanguage.

JavaLanguage() - Constructor for class jml2b.languages.java.JavaLanguage

JavaLineStyler - class jack.plugin.edit.JavaLineStyler.

Line styler for JML files.

JavaLineStyler(JavaScanner) - Constructor for class jack.plugin.edit.JavaLineStyler

JavaModifiedFieldForm - class jml2b.languages.java.JavaModifiedFieldForm.

JavaQuantifiedForm - class jml2b.languages.java.JavaQuantifiedForm.

JavaQuantifiedVarForm - class jml2b.languages.java.JavaQuantifiedVarForm.

JavaScanner - class jack.plugin.edit.JavaScanner.

A simple scanner for Java and JML

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

JavaTTypeForm - class jml2b.languages.java.JavaTTypeForm.

JavaTerminalForm - class jml2b.languages.java.JavaTerminalForm.

JavaTranslationResult - class jml2b.languages.java.JavaTranslationResult.

JavaTriaryForm - class jml2b.languages.java.JavaTriaryForm.

JavaType - class jml2b.languages.java.JavaType.

JavaUnaryForm - class jml2b.languages.java.JavaUnaryForm.

Jm_AND_THEN - Static variable in interface jml2b.formula.IFormToken

Jm_EXISTS - Static variable in interface jml2b.formula.IFormToken

B existential quantifier operator #a.b with priority 250.

Jm_FORALL - Static variable in interface jml2b.formula.IFormToken

B universal quantification operator !a.b with priority 250.

Jm_IMPLICATION_OP - Static variable in interface jml2b.formula.IFormToken

JML Implication binary operator a ==> b with priority 30.

Jm_IS_SUBTYPE - Static variable in interface jml2b.formula.IFormToken

JML subtype binary operator a <: b with priority 250.

Jm_OR_ELSE - Static variable in interface jml2b.formula.IFormToken

Jm_T_OLD - Static variable in interface jml2b.formula.IFormToken

JML old unary operator \old(a) with priority 250.

Jm_T_RESULT - Static variable in interface jml2b.formula.IFormToken

JML literal \result with priority 250.

Jm_T_TYPE - Static variable in interface jml2b.formula.IFormToken

JML type unary operator \type(a) with priority 250.

Jml2b - class jml2b.Jml2b.

Jml2b() - Constructor for class jml2b.Jml2b

Jml2bConfig - class jml2b.Jml2bConfig.

Jml2bConfig(String[], boolean) - Constructor for class jml2b.Jml2bConfig

Jml2bException - exception jml2b.exceptions.Jml2bException.

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

JmlClassEntryFile - class jml2b.util.JmlClassEntryFile.

JmlClassEntryFile(String, String) - Constructor for class jml2b.util.JmlClassEntryFile

JmlClauseGenerator - class jack.plugin.source.JmlClauseGenerator.

Generator of JML clause.

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

JmlEntryFile - class jml2b.util.JmlEntryFile.

JmlEntryFile(File) - Constructor for class jml2b.util.JmlEntryFile

JmlEntryFileInJar - class jml2b.util.JmlEntryFileInJar.

JmlEntryFileInJar(String, String) - Constructor for class jml2b.util.JmlEntryFileInJar

JmlExpression - interface jml2b.structure.jml.JmlExpression.

The interface defines methods to apply to a JML expression.

JmlFile - class jml2b.structure.java.JmlFile.

Class keeping information on Java/JML files.

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

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

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

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

JmlFile - class jpov.structure.JmlFile.

This class implements the root node of the tree.

JmlFileEntry - class jml2b.util.JmlFileEntry.

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

JmlFileStream - class jml2b.util.JmlFileStream.

JmlFileStream(File) - Constructor for class jml2b.util.JmlFileStream

JmlLoader - class jml2b.structure.java.JmlLoader.

class used to load classes.

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

JmlMergeViewer - class jack.plugin.source.JmlMergeViewer.

A text merge viewer for JML files.

JmlMergeViewer(ViewForm, CompareConfiguration) - Constructor for class jack.plugin.source.JmlMergeViewer

JmlMergeViewerContentProvider - class jack.plugin.source.JmlMergeViewerContentProvider.

Content provider for the JML merge viewer.

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

JmlPathDirectory - class jml2b.util.JmlPathDirectory.

JmlPathDirectory(String) - Constructor for class jml2b.util.JmlPathDirectory

JmlPathEntry - class jml2b.util.JmlPathEntry.

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

JmlPathJar - class jml2b.util.JmlPathJar.

JmlPathJar(String) - Constructor for class jml2b.util.JmlPathJar

JmlSourceEntryFile - class jml2b.util.JmlSourceEntryFile.

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

JpoFile - class jpov.JpoFile.

This class defines a JPO file.

JpoFile(IJml2bConfiguration, String) - Constructor for class jpov.JpoFile

Constucts a JPO file from a given repository and a given name.

JpoInputStream - class jml2b.util.JpoInputStream.

JpoInputStream(DataInput, DataInputStream) - Constructor for class jml2b.util.JpoInputStream

JpoOutputStream - class jml2b.util.JpoOutputStream.

JpoOutputStream(OutputStream) - Constructor for class jml2b.util.JpoOutputStream

JpovError - class jpov.JpovError.

Utility class the diplay error dialogs with details

JpovError() - Constructor for class jpov.JpovError

JpovUtil - class jack.plugin.JpovUtil.

Utilities for handling Jpov within the plugin.

JpovUtil() - Constructor for class jack.plugin.JpovUtil

j_int2byte - Static variable in class jml2b.formula.TerminalForm

The constant formula j_int2byte, In the B lemmas, j_int2byte is a function that converts an int into a byte.

j_int2char - Static variable in class jml2b.formula.TerminalForm

The constant formula j_int2char, In the B lemmas, j_int2char is a function that converts an int into a char.

j_int2short - Static variable in class jml2b.formula.TerminalForm

The constant formula j_int2short, In the B lemmas, j_int2short is a function that converts an int into a short.

jack.plugin - package jack.plugin

jack.plugin.compile - package jack.plugin.compile

jack.plugin.edit - package jack.plugin.edit

jack.plugin.metrics - package jack.plugin.metrics

jack.plugin.perspective - package jack.plugin.perspective

jack.plugin.prove - package jack.plugin.prove

jack.plugin.source - package jack.plugin.source

jml2b - package jml2b

jml2b.exceptions - package jml2b.exceptions

jml2b.formula - package jml2b.formula

Provides the classes necessary to create and manage formulas.

jml2b.languages - package jml2b.languages

jml2b.languages.java - package jml2b.languages.java

jml2b.link - package jml2b.link

jml2b.pog - package jml2b.pog

Provides the classes necessary to generate proof obligations.

jml2b.pog.lemma - package jml2b.pog.lemma

jml2b.pog.printers - package jml2b.pog.printers

jml2b.pog.proofobligation - package jml2b.pog.proofobligation

jml2b.pog.substitution - package jml2b.pog.substitution

Provides the classes necessary to create and manage substitutions.

jml2b.pog.util - package jml2b.pog.util

jml2b.structure - package jml2b.structure

jml2b.structure.bytecode - package jml2b.structure.bytecode

jml2b.structure.java - package jml2b.structure.java

jml2b.structure.jml - package jml2b.structure.jml

Provides the classes necessary to create and manage jml clauses such that depends, represents, specification cases, modifies and exsures.

jml2b.structure.statement - package jml2b.structure.statement

Provides the classes necessary to create and manage java and jml statements and expressions.

jml2b.util - package jml2b.util

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

Normalize the specification case.

jmlNormalize(IJml2bConfiguration, Class) - Method in class jml2b.structure.statement.Expression

jmlNormalize(IJml2bConfiguration, Class) - Method in class jml2b.structure.statement.StAssert

jmlNormalize(IJml2bConfiguration, Class) - Method in class jml2b.structure.statement.StBlock

jmlNormalize(IJml2bConfiguration, Class) - Method in class jml2b.structure.statement.StControlFlowBreak

jmlNormalize(IJml2bConfiguration, Class) - Method in class jml2b.structure.statement.StDoWhile

jmlNormalize(IJml2bConfiguration, Class) - Method in class jml2b.structure.statement.StFor

jmlNormalize(IJml2bConfiguration, Class) - Method in class jml2b.structure.statement.StIf

jmlNormalize(IJml2bConfiguration, Class) - Method in class jml2b.structure.statement.StImplementsLabel

jmlNormalize(IJml2bConfiguration, Class) - Method in class jml2b.structure.statement.StLabel

jmlNormalize(IJml2bConfiguration, Class) - Method in class jml2b.structure.statement.StLoops

jmlNormalize(IJml2bConfiguration, Class) - Method in class jml2b.structure.statement.StSequence

jmlNormalize(IJml2bConfiguration, Class) - Method in class jml2b.structure.statement.StSkip

jmlNormalize(IJml2bConfiguration, Class) - Method in class jml2b.structure.statement.StSpecBlock

jmlNormalize(IJml2bConfiguration, Class) - Method in class jml2b.structure.statement.StSwitch

jmlNormalize(IJml2bConfiguration, Class) - Method in class jml2b.structure.statement.StTry

jmlNormalize(IJml2bConfiguration, Class) - Method in class jml2b.structure.statement.StVarDecl

jmlNormalize(IJml2bConfiguration, Class) - Method in class jml2b.structure.statement.Statement

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

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

jmlPathProperty - Static variable in class jml2b.Jml2b

jpov - package jpov

jpov.structure - package jpov.structure

jpov.substitution - package jpov.substitution

jpov.viewer.lemma - package jpov.viewer.lemma

jpov.viewer.source - package jpov.viewer.source

jpov.viewer.tree - package jpov.viewer.tree