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

T

TASK_FINISHED - Static variable in class jpov.Icons

TASK_RUNNING - Static variable in class jpov.Icons

TASK_WAITING - Static variable in class jpov.Icons

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

comment indice corresponding to an exception thrown by a method call (red)

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

Substitution type corresponding to the substitution of a temporary variable by a

TTypeExp - class jml2b.structure.statement.TTypeExp.

This class implements expressions corresponding to types.

TTypeExp(Type) - Constructor for class jml2b.structure.statement.TTypeExp

TTypeForm - class jml2b.formula.TTypeForm.

This class implements type formula.

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

TTypeForm(byte, Type) - Constructor for class jml2b.formula.TTypeForm

Construct a formula from a type.

TYPE - Static variable in class jml2b.link.LinkInfo

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

Substitution type corresponding to the substitution of typeof by typeof <+ a * {b}

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

Substitution type corresponding to the substitution of typeof by typeof <+ a |-> b

TYPES - Static variable in class jml2b.formula.BasicType

T_ARRAY - Static variable in class jml2b.structure.java.Type

indicate an array type.

T_BOOLEAN - Static variable in class jml2b.structure.java.Type

Constant representing the boolean type.

T_BYTE - Static variable in class jml2b.structure.java.Type

Constant representing the byte type.

T_CALLED_OLD - Static variable in interface jml2b.formula.IFormToken

Called old operator with priority 250.

T_CALLED_OLD - Static variable in interface jml2b.structure.statement.MyToken

Token correspoding to a called old

T_CHAR - Static variable in class jml2b.structure.java.Type

Constant representing the char type.

T_CLASS - Static variable in class jml2b.structure.java.Type

used for typing class expression: this should always result in a typecheck error

T_DOUBLE - Static variable in class jml2b.structure.java.Type

Constant representing the double type.

T_FLOAT - Static variable in class jml2b.structure.java.Type

Constant representing the float type.

T_FRESH_CALLED_OLD - Static variable in interface jml2b.structure.statement.MyToken

Token correspoding to a fresh called old

T_INT - Static variable in class jml2b.structure.java.Type

Constant representing the int type.

T_LONG - Static variable in class jml2b.structure.java.Type

Constant representing the long type.

T_NULL - Static variable in class jml2b.structure.java.Type

Constant representing the null type.

T_REF - Static variable in class jml2b.structure.java.Type

Constant used to tag references to classes.

T_SHORT - Static variable in class jml2b.structure.java.Type

Constant representing the short type.

T_TYPE - Static variable in interface jml2b.formula.IFormToken

T_TYPE - Static variable in class jml2b.structure.java.Type

used for return values of \elemtype and \type

T_VARIANT_OLD - Static variable in interface jml2b.formula.IFormToken

T_VARIANT_OLD - Static variable in interface jml2b.structure.statement.MyToken

T_VOID - Static variable in class jml2b.structure.java.Type

Constant representing the void type.

Tabs - class jml2b.util.Tabs.

Simple class that simplifies handling tabs.

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

TemporaryField - class jml2b.pog.util.TemporaryField.

This class provides services to create and use temporary fields that are usefull during the proof obligation calculation.

TemporaryField(ParsedItem, Modifiers, Type, String, Expression) - Constructor for class jml2b.pog.util.TemporaryField

Constructs a temporary field from a field with a new name.

TemporaryField(ParsedItem, Type, String) - Constructor for class jml2b.pog.util.TemporaryField

Constructs a tempory field with a given name and a given type.

TerminalExp - class jml2b.structure.statement.TerminalExp.

This class implements a terminal expression.

TerminalExp(int, String) - Constructor for class jml2b.structure.statement.TerminalExp

Constructs an expression that is not a Java identifer.

TerminalExp(String, Type) - Constructor for class jml2b.structure.statement.TerminalExp

Constructs an expression that is an identifier but not a Java identifer.

TerminalExp(Identifier, String) - Constructor for class jml2b.structure.statement.TerminalExp

Constructs an expression from a Java identifer and a postfix string.

TerminalExp(Identifier) - Constructor for class jml2b.structure.statement.TerminalExp

Constructs an expression from a Java identifer.

TerminalForm - class jml2b.formula.TerminalForm.

This class implements terminal formula: identifiers, literal constants and builtin types.

TerminalForm(byte, String, Identifier, boolean) - Constructor for class jml2b.formula.TerminalForm

Constructs a terminal formula.

TerminalForm(byte) - Constructor for class jml2b.formula.TerminalForm

Constructs a formula that is not a Java identifer.

TerminalForm(byte, String) - Constructor for class jml2b.formula.TerminalForm

Constructs a formula that is not a Java identifer.

TerminalForm(int) - Constructor for class jml2b.formula.TerminalForm

Constructs a formula that is a Ja_NUM_INT.

TerminalForm(String) - Constructor for class jml2b.formula.TerminalForm

Constructs a formula that is an identifier but not a Java identifer.

TerminalForm(Identifier) - Constructor for class jml2b.formula.TerminalForm

Constructs a formula from a Java identifer.

TerminalForm(Identifier, String) - Constructor for class jml2b.formula.TerminalForm

Constructs a formula from a Java identifer and a postfix string.

TestSerialize - class jml2b.util.TestSerialize.

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

Theorem - class jml2b.pog.lemma.Theorem.

This class describes a theorem.

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

Construct an empty theorem.

Theorem(IJml2bConfiguration, Enumeration, Expression, GoalOrigin) - Constructor for class jml2b.pog.lemma.Theorem

Construct a theorem from an enumeration of Exsures.

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

Construct a theorem from a method specification corresponding to the proof of its normal behaviours.

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

Construct a theorem containing one lemma

TheoremList - class jml2b.pog.lemma.TheoremList.

This class implements a list of theorems

TokenException - exception jml2b.exceptions.TokenException.

A specialisation of the ParseException class that is used when unexpected tokens are encountered.

TokenException(JmlFile, LineAST, String, String, String) - Constructor for class jml2b.exceptions.TokenException

Creates a new TokenException instance.

TokenException(JmlFile, LineAST, String, String, int) - Constructor for class jml2b.exceptions.TokenException

Creates a new TokenException instance.

TokenException(JmlFile, LineAST, String, int, int) - Constructor for class jml2b.exceptions.TokenException

Creates a new TokenException instance.

ToolbarButton - class jack.plugin.ToolbarButton.

Base class for toolbar buttons.

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

TranslationException - exception jml2b.exceptions.TranslationException.

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

TreeContentProvider - class jpov.viewer.tree.TreeContentProvider.

This class implements a content provider for the tree

TreeContentProvider(ICaseExplorer) - Constructor for class jpov.viewer.tree.TreeContentProvider

TreeFilter - class jpov.viewer.tree.TreeFilter.

This class implements a filter for tree.

TreeFilter(TreeFilterWindow) - Constructor for class jpov.viewer.tree.TreeFilter

Constructs a filter with an associated filter window

TreeFilterConfiguration - class jpov.viewer.tree.TreeFilterConfiguration.

Class containing the configuration for a TreeFilterWindow.

TreeFilterConfiguration(String) - Constructor for class jpov.viewer.tree.TreeFilterConfiguration

Creates a new TreeFilterConfiguration with the given name n.

TreeFilterConfiguration(String, boolean, boolean, int, int, int) - Constructor for class jpov.viewer.tree.TreeFilterConfiguration

Constructs a tree filter configuration

TreeFilterWindow - class jpov.viewer.tree.TreeFilterWindow.

This class implements the dialog that displays the window allowing to choose the filter to apply to the tree

TreeFilterWindow(Shell, ICaseExplorer) - Constructor for class jpov.viewer.tree.TreeFilterWindow

Constructs the tree filter windows.

TreeItemSelection - class jpov.viewer.tree.TreeItemSelection.

Tis class implements a selection changed listener for the tree.

TreeItemSelection(ILemmaViewer, ISourceCaseViewer, ICaseExplorer) - Constructor for class jpov.viewer.tree.TreeItemSelection

Constructs a selection changed listener

TreeLabelProvider - class jpov.viewer.tree.TreeLabelProvider.

This class provides methods that associate an image and a text to a node of the tree in the viewer.

TreeLabelProvider(ICaseExplorer) - Constructor for class jpov.viewer.tree.TreeLabelProvider

TreeObject - class jpov.structure.TreeObject.

This class defines a node of the tree of the viewer.

TreeObject() - Constructor for class jpov.structure.TreeObject

TreeSorter - class jpov.viewer.tree.TreeSorter.

This class implements a sorter for the node of the tree

TreeSorter(ICaseExplorer) - Constructor for class jpov.viewer.tree.TreeSorter

TriaryForm - class jml2b.formula.TriaryForm.

This class implements tri-ary formula, that is conditional formula coming from the Java structure a ? b : c or equals with restricted domains formulas.

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

TriaryForm(byte, Formula, Formula, Formula) - Constructor for class jml2b.formula.TriaryForm

Constructs a question formula from three formulas.

Type - class jml2b.structure.java.Type.

Class representing types.

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

Type(String) - Constructor for class jml2b.structure.java.Type

Type(int) - Constructor for class jml2b.structure.java.Type

Creates a new builtin type with the given tag.

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

Creates a new type corresponding to the given class.

Type(IJml2bConfiguration, Type) - Constructor for class jml2b.structure.java.Type

Creates a new array class containing the given elements.

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

Creates a new array type using the given type as elements.

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

Creates a new type from the given AST.

TypeCheckException - exception jml2b.exceptions.TypeCheckException.

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

TypeCheckable - interface jml2b.link.TypeCheckable.

TypesType - Static variable in class jml2b.formula.BasicType

tag - Variable in class jml2b.link.LinkInfo

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

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

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

Returns the tail statement in a sequence considered as a list.

throwException(Formula, Formula) - Method in class jml2b.pog.lemma.ExceptionalBehaviourStack

Returns the proof to prove to ensure that the thrown of an exception ensures the current proof.

throwException(String, AClass) - Method in class jml2b.pog.lemma.ExceptionalBehaviourStack

Returns the proof obligation ensuring that the thrown of an exception ensures the current proof.

throwException(IJml2bConfiguration, AClass) - Method in class jml2b.pog.lemma.ExceptionalBehaviourStack

Calculates the proof obligation ensuring that the thrown of a runtime exception ensures the current proof.

throwException(Formula, Formula) - Method in class jml2b.pog.lemma.ExceptionalLemma

throwException(String, AClass) - Method in class jml2b.pog.lemma.ExceptionalLemma

throwException(String, AClass) - Method in class jml2b.pog.lemma.ExsuresLemma

throwException(Formula, Formula) - Method in class jml2b.pog.lemma.ExsuresLemma

throwException(Formula, Formula) - Method in class jml2b.pog.lemma.Lemma

Returns the lemma to prove to ensure that the thrown of an exception ensures the current lemma.

throwException(String, AClass) - Method in class jml2b.pog.lemma.Lemma

Returns the lemma to prove to ensure that the thrown of an exception ensures the current lemma.

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

toJava(int) - Method in class jml2b.formula.Formula

Translates the formula into the Java language

toJava() - Method in class jml2b.structure.java.Parameters

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

Converts the type to a java representation.

toJava(int) - Method in class jml2b.structure.jml.Exsures

toJava(int) - Method in class jml2b.structure.jml.ModifiesClause

Converts the clause into a string.

toJava(int) - Method in class jml2b.structure.jml.ModifiesEverything

toJava(int) - Method in class jml2b.structure.jml.ModifiesList

toJava(int) - Method in class jml2b.structure.jml.ModifiesNothing

toJava(int) - Method in class jml2b.structure.statement.ArrayInitializer

toJava(int) - Method in class jml2b.structure.statement.BinaryExp

toJava(int) - Method in class jml2b.structure.statement.Expression

Displays the expression corresponding to a part of a method specification in a tool tip with the initial Java syntax.

toJava(int) - Method in class jml2b.structure.statement.IsSubtypeOfExp

toJava(int) - Method in class jml2b.structure.statement.MethodCallExp

toJava(int) - Method in class jml2b.structure.statement.QuantifiedExp

toJava(int) - Method in class jml2b.structure.statement.QuestionExp

toJava(int) - Method in class jml2b.structure.statement.TTypeExp

toJava(int) - Method in class jml2b.structure.statement.TerminalExp

toJava(int) - Method in class jml2b.structure.statement.UnaryExp

toJava(int) - Method in class jml2b.structure.statement.WithTypeExp

toJava(int) - Method in class jpov.structure.VirtualFormula

Converts the current formula to a string suitable for output into the Java view.

toJavaWithParameterName() - Method in class jml2b.structure.java.Parameters

toLang(String, int) - Method in class jml2b.formula.Formula

Translates the formula into a given language.

toLang(String, int) - Method in class jml2b.formula.QuantifiedVarForm

toLang(int) - Method in interface jml2b.languages.ITranslatable

Translate a formula, a type or quantified variables.

toLang(int) - Method in class jml2b.languages.java.JavaBinaryForm

Converts the binary formula to a string suitable for output into the Java view.

toLang(int) - Method in class jml2b.languages.java.JavaModifiedFieldForm

toLang(int) - Method in class jml2b.languages.java.JavaQuantifiedForm

The formula is displayed \forall vars; body or \exists vars; body

toLang(int) - Method in class jml2b.languages.java.JavaQuantifiedVarForm

Converts the quantified formulas to a string suitable for output into the Java view.

toLang(int) - Method in class jml2b.languages.java.JavaTTypeForm

toLang(int) - Method in class jml2b.languages.java.JavaTerminalForm

Converts the formula into Java.

toLang(int) - Method in class jml2b.languages.java.JavaTriaryForm

Converts the current formula to a string suitable for output into the Java view.

toLang(int) - Method in class jml2b.languages.java.JavaType

toLang(int) - Method in class jml2b.languages.java.JavaUnaryForm

Converts the unary formula to a string suitable for output into the Java view.

toLang(String) - Method in class jml2b.structure.java.Type

toString - Static variable in interface jml2b.formula.IFormToken

Array given token name for the error displaying.

toString() - Method in class jml2b.languages.java.JavaTranslationResult

toString(char) - Method in class jml2b.structure.IAParameters

toString(char) - Method in class jml2b.structure.bytecode.ClassParameters

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

toString() - Method in class jml2b.structure.java.Method

toString() - Method in class jml2b.structure.java.Parameters

toString(char) - Method in class jml2b.structure.java.Parameters

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

toString() - Method in class jml2b.util.JmlEntryFile

toString() - Method in class jml2b.util.JmlEntryFileInJar

toString() - Method in class jml2b.util.Tabs

convert the given set of tabs to a string.

toStrings() - Method in class jml2b.languages.java.JavaTranslationResult

toUniqString() - Method in interface jml2b.languages.ITranslationResult

toUniqString() - Method in class jml2b.languages.java.JavaTranslationResult

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

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

Converts comma separated formulas into a set of formulas.

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

Returns a string array corresponding to parts of a given string

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

Returns the top of the stack.

type - Variable in class jml2b.link.LinkInfo

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

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

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

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

Links the statement parts of the file if needed.

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

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

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

typeCheck(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.jml.ModifiesDot

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

typeCheck(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.jml.ModifiesIdent

typeCheck(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.jml.ModifiesLbrack

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

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

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

typeCheck(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.jml.SpecArrayDotDot

typeCheck(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.jml.SpecArrayExpr

typeCheck(IJml2bConfiguration, LinkContext) - Method in class jml2b.structure.jml.SpecArrayStar

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

typeFactory(Type) - Method in interface jml2b.languages.ILanguage

Returns a type corresponding to the initial one but converted in a translatable type.

typeFactory(Type) - Method in class jml2b.languages.java.JavaLanguage

typeof - Static variable in class jml2b.formula.TerminalForm

The formula typeof.