Overview  Package  Class  Use  Tree  Deprecated   Index  Help 
 PREV LETTER   NEXT LETTER FRAMES    NO FRAMES    
A B C D E F G H I J K L M N O P Q R S T U V W Z

G

GHOST - Static variable in interface jml2b.structure.java.ModFlags
 
GOAL - Static variable in class jml2b.pog.lemma.VirtualFormula
Formula origin corresponding to a goal
GREEN - Static variable in class jpov.viewer.source.Box
The green color.
GUARDED_SET - Static variable in interface jml2b.formula.IFormToken
Set guarded by a condition
Generator - class jack.plugin.Generator.
This class loads and links a JML file.
Generator(Iterator) - Constructor for class jack.plugin.Generator
Create a new Generator allowing to load and link given compilation units.
Generator(ICompilationUnit, String) - Constructor for class jack.plugin.Generator
 
Goal - class jml2b.pog.lemma.Goal.
This class implements a goal.
Goal(VirtualFormula, GoalOrigin) - Constructor for class jml2b.pog.lemma.Goal
Constructs a goal from a formula and an origin.
Goal(Formula, GoalOrigin) - Constructor for class jml2b.pog.lemma.Goal
Constructs a goal from a formula and an origin.
Goal - class jpov.structure.Goal.
This class implements a goal.
GoalContentProvider - class jpov.viewer.lemma.GoalContentProvider.
Class that give the content to display in the goal folder of the lemma view.
GoalOrigin - class jml2b.pog.lemma.GoalOrigin.
This class describes the origin of a goal.
GoalOrigin(JpoInputStream) - Constructor for class jml2b.pog.lemma.GoalOrigin
Constructs a goal origin from a loaded .jpo file
GoalOrigin(byte, AField) - Constructor for class jml2b.pog.lemma.GoalOrigin
Constructs a goal origin for a modifies
GoalOrigin(byte, AMethod) - Constructor for class jml2b.pog.lemma.GoalOrigin
Constructs a goal origin for a requires
GoalOrigin(byte) - Constructor for class jml2b.pog.lemma.GoalOrigin
Constructs a goal origin with no comment
GoalStatus - class jml2b.pog.lemma.GoalStatus.
This class provides constants and facilities to manage the status of a goal.
GoalStatus() - Constructor for class jml2b.pog.lemma.GoalStatus
Constructs by default a goal status.
GoalStatus(JpoInputStream) - Constructor for class jml2b.pog.lemma.GoalStatus
Constructs a non obvious goal from a .jpo file
GuardedModifies - class jml2b.structure.jml.GuardedModifies.
This class implements a guarded modifies clause.
GuardedModifies(Modifies) - Constructor for class jml2b.structure.jml.GuardedModifies
Constructs a guarded modifies.
garbage - Variable in class jml2b.structure.java.NamedNode
 
garbageIdent() - Method in class jml2b.formula.BinaryForm
 
garbageIdent() - Method in class jml2b.formula.Formula
Annotates all the fields that appear in the formula to declare them in the Atelier B files.
garbageIdent() - Method in class jml2b.formula.QuantifiedForm
 
garbageIdent() - Method in class jml2b.formula.TTypeForm
 
garbageIdent() - Method in class jml2b.formula.TerminalForm
 
garbageIdent() - Method in class jml2b.formula.TriaryForm
 
garbageIdent() - Method in class jml2b.formula.UnaryForm
 
garbageIdent() - Method in class jml2b.pog.lemma.ExsuresLemma
 
garbageIdent() - Method in class jml2b.pog.lemma.Goal
 
garbageIdent() - Method in interface jml2b.pog.lemma.ILemma
Annotates all the fields that appear in the lemma to declare them in the Atelier B files.
garbageIdent() - Method in class jml2b.pog.lemma.Proofs
Annotates all the fields that appear in the theorem to declare them in the Atelier B files.
garbageIdent() - Method in class jml2b.pog.lemma.SimpleLemma
 
gc(IJml2bConfiguration, boolean) - Method in class jml2b.pog.lemma.Proofs
Tries to suppress obvious goals, lemmas, theorems.
getABProject() - Method in class jml2b.Jml2bConfig
 
getAbsolutePath() - Method in class jml2b.util.JmlClassEntryFile
 
getAbsolutePath() - Method in class jml2b.util.JmlEntryFile
 
getAbsolutePath() - Method in class jml2b.util.JmlEntryFileInJar
 
getAbsolutePath() - Method in class jml2b.util.JmlFileEntry
 
getAbstractField() - Method in class jml2b.structure.jml.Depends
Returns the abstract field.
getAccessibleDepends() - Method in class jml2b.structure.java.Class
 
getAccessibleFields() - Method in class jml2b.structure.java.Class
 
getAncestorContent(Object) - Method in class jack.plugin.source.JmlMergeViewerContentProvider
 
getAncestorImage(Object) - Method in class jack.plugin.source.JmlMergeViewerContentProvider
 
getAncestorLabel(Object) - Method in class jack.plugin.source.JmlMergeViewerContentProvider
 
getAndLoadClass(IJml2bConfiguration, String) - Method in class jml2b.structure.java.Package
Return a reference to the class name.
getAndLoadPackage(String) - Method in class jml2b.structure.java.Package
 
getAnnotatedModifies() - Method in class jml2b.structure.java.Method
 
getAnnotatedPostcondition() - Method in class jml2b.structure.java.Method
 
getAnnotatedPrecondition() - Method in class jml2b.structure.java.Method
 
getArray(IJml2bConfiguration) - Static method in class jml2b.structure.java.Class
Return the class that is used to represent arrays.
getArray() - Method in class jml2b.structure.java.VarDeclParser
Returns the parsed variables as an array of fields.
getArraylength(IJml2bConfiguration) - Static method in class jml2b.formula.TerminalForm
 
getAssert(Vector) - Method in class jml2b.structure.statement.Expression
 
getAssert(Vector) - Method in class jml2b.structure.statement.StAssert
 
getAssert(Vector) - Method in class jml2b.structure.statement.StBlock
 
getAssert(Vector) - Method in class jml2b.structure.statement.StControlFlowBreak
 
getAssert(Vector) - Method in class jml2b.structure.statement.StDoWhile
 
getAssert(Vector) - Method in class jml2b.structure.statement.StFor
 
getAssert(Vector) - Method in class jml2b.structure.statement.StIf
 
getAssert(Vector) - Method in class jml2b.structure.statement.StImplementsLabel
 
getAssert(Vector) - Method in class jml2b.structure.statement.StLabel
 
getAssert(Vector) - Method in class jml2b.structure.statement.StSequence
 
getAssert(Vector) - Method in class jml2b.structure.statement.StSkip
 
getAssert(Vector) - Method in class jml2b.structure.statement.StSpecBlock
 
getAssert(Vector) - Method in class jml2b.structure.statement.StSwitch
 
getAssert(Vector) - Method in class jml2b.structure.statement.StTry
 
getAssert(Vector) - Method in class jml2b.structure.statement.StVarDecl
 
getAssert(Vector) - Method in class jml2b.structure.statement.Statement
 
getAssign() - Method in class jml2b.structure.AField
 
getAssign() - Method in class jml2b.structure.bytecode.ClassField
 
getAssign() - Method in class jml2b.structure.java.Field
Returns the Expression object corresponding to the assign clause of this field The assign clause of a field corresponds to its initialisation, when an initialisation is given during the declaration of the field.
getBName() - Method in class jml2b.pog.lemma.ExsuresLemma
Returns the name of the catched variable or a temporary variable if there is no catched variable
getBName() - Method in class jml2b.pog.util.IdentifierResolver
Returns the name to be used into the B lemmas.
getBName() - Method in class jml2b.pog.util.TemporaryField
Returns the name of the field.
getBName() - Method in class jml2b.structure.java.Field
Returns the B name of the field.
getBName() - Method in class jml2b.structure.java.NamedNode
 
getBasicType() - Method in class jml2b.formula.BinaryForm
 
getBasicType() - Method in class jml2b.formula.Formula
Returns the type of a formula
getBasicType() - Method in class jml2b.formula.QuantifiedForm
 
getBasicType() - Method in class jml2b.formula.TTypeForm
 
getBasicType() - Method in class jml2b.formula.TerminalForm
 
getBasicType() - Method in class jml2b.formula.TriaryForm
 
getBasicType() - Method in class jml2b.formula.UnaryForm
 
getBgcolor() - Method in class jack.plugin.edit.Box
 
getBody(IJml2bConfiguration) - Method in class jml2b.structure.java.Method
 
getBody() - Method in class jml2b.structure.statement.QuantifiedExp
 
getBody() - Method in class jml2b.structure.statement.StBlock
 
getBody() - Method in class jml2b.structure.statement.StLoops
 
getBoolean() - Static method in class jml2b.structure.java.Type
Returns a type corresponding to the boolean builtin type.
getByte() - Static method in class jml2b.structure.java.Type
 
getCalledMethods() - Method in class jml2b.structure.java.Method
 
getCaseNum() - Method in class jpov.structure.Lemma
Returns the case number into its englobing method.
getCasesPercent() - Method in class jpov.viewer.tree.TreeFilterWindow
Returns the ipper proof percentage bound for a case to be displayed
getChar() - Static method in class jml2b.structure.java.Type
Returns a type corresponding to the char builtin type.
getChildren(Object) - Method in class jpov.viewer.tree.TreeContentProvider
Returns the children of a node, that is: its classes for a JML file its static initialization, constructors and methods for a class its lemmas for a method its goals for a lemma
getClass(String) - Method in class jml2b.structure.java.Package
Search for the given class inside this package.
getClassCount(boolean) - Method in class jml2b.structure.java.Package
Return the number of classes in this package.
getClassPercent() - Method in class jpov.viewer.tree.TreeFilterWindow
Returns the upper proof percentage bound for a class to be displayed
getClasses() - Method in class jml2b.pog.printers.ClassResolver
 
getClasses() - Method in interface jml2b.pog.printers.IClassResolver
 
getClasses() - Method in class jml2b.structure.java.JmlFile
 
getClasses() - Method in class jml2b.structure.java.Package
 
getClasses() - Method in class jpov.structure.JmlFile
Returns the array of classes.
getClonedSpecCases(ParsedItem) - Method in class jml2b.structure.AMethod
 
getClonedSpecCases(ParsedItem) - Method in class jml2b.structure.bytecode.ClassMethod
 
getClonedSpecCases(ParsedItem) - Method in class jml2b.structure.java.Method
 
getColumn() - Method in class jml2b.exceptions.LinkException
 
getColumn() - Method in class jml2b.exceptions.TypeCheckException
 
getColumn() - Method in class jml2b.structure.java.ParsedItem
Returns the column.
getComment() - Method in class jml2b.pog.util.ColoredInfo
 
getCommentText() - Method in class jpov.viewer.source.Box
Returns the information associated with the box.
getConcreteFields() - Method in class jml2b.structure.jml.Depends
Returns the set of dependees.
getCond() - Method in class jml2b.structure.statement.QuestionExp
 
getConfig() - Method in class jml2b.structure.java.JmlFile
 
getConstraints() - Method in class jml2b.structure.java.Class
 
getConstructor(IJml2bConfiguration, Vector) - Method in class jml2b.structure.bytecode.ClassFile
 
getConstructor(IJml2bConfiguration, Vector) - Method in class jml2b.structure.java.AClass
 
getConstructor(Parameters) - Method in class jml2b.structure.java.Class
 
getConstructor(IJml2bConfiguration, Vector) - Method in class jml2b.structure.java.Class
Returns the constructor matching the given parameter types.
getConstructors() - Method in class jml2b.structure.java.Class
Returns an enumeration of the constructors defined by this class.
getConstructors() - Method in class jpov.structure.Class
Returns the constructors array.
getContents() - Method in class jml2b.util.JmlFileStream
 
getCreationDate() - Method in class jack.plugin.prove.ProofTask
Return the creation date of the task.
getCurrent() - Static method in class jack.plugin.prove.ProofView
 
getCurrentClass() - Method in class jml2b.link.LinkContext
 
getData(Object) - Method in class jml2b.structure.java.JmlFile
Retrieve data previously stored using storeData.
getDefault() - Static method in class jack.plugin.JackPlugin
Returns the shared instance.
getDefaultArrayInitialiser(Type) - Static method in class jml2b.structure.statement.WithTypeExp
Returns the formula corresponding to the default array element initializer
getDefaultConstructor() - Method in class jml2b.structure.bytecode.ClassFile
 
getDefaultConstructor() - Method in class jml2b.structure.java.AClass
 
getDefaultConstructor() - Method in class jml2b.structure.java.Class
Returns the default constructor for this class, if the class defines one.
getDefaultEnsures() - Method in class jack.plugin.JackJml2bConfiguration
 
getDefaultEnsures() - Method in interface jml2b.IJml2bConfiguration
Returns the default ensures clause
getDefaultEnsures() - Method in class jml2b.Jml2bConfig
 
getDefaultExsures() - Method in class jack.plugin.JackJml2bConfiguration
 
getDefaultExsures() - Method in interface jml2b.IJml2bConfiguration
Returns the default exsures clause
getDefaultExsures() - Method in class jml2b.Jml2bConfig
 
getDefaultExternalFile() - Method in class jack.plugin.JackJml2bConfiguration
 
getDefaultExternalFile() - Method in interface jml2b.IJml2bConfiguration
 
getDefaultExternalFile() - Method in class jml2b.Jml2bConfig
 
getDefaultInitialiser() - Method in class jml2b.structure.java.Field
 
getDefaultJmlEnsuresText(IProject) - Static method in class jack.plugin.JackJml2bConfiguration
Returns the default ensures clause for jml.
getDefaultJmlExsuresExceptions(IProject) - Static method in class jack.plugin.JackJml2bConfiguration
 
getDefaultJmlExsuresOther(IProject) - Static method in class jack.plugin.JackJml2bConfiguration
 
getDefaultJmlExsuresType(IProject) - Static method in class jack.plugin.JackJml2bConfiguration
Return the default exsures type for the given project.
getDefaultJmlModifies(IProject) - Static method in class jack.plugin.JackJml2bConfiguration
Returns the default modifies clause for jml specifications.
getDefaultJmlRequiresText(IProject) - Static method in class jack.plugin.JackJml2bConfiguration
Returns the default requires clause for jml if it is not set to requires true.
getDefaultLoopModifies() - Method in class jml2b.structure.java.Method
 
getDefaultModifies() - Method in class jack.plugin.JackJml2bConfiguration
 
getDefaultModifies() - Method in interface jml2b.IJml2bConfiguration
Returns the default modifies clause
getDefaultModifies() - Method in class jml2b.Jml2bConfig
 
getDefaultOutputDir() - Static method in class jack.plugin.JackPlugin
Returns the default output directory.
getDefaultRefDecl() - Static method in class jml2b.formula.BinaryForm
Returns the default type declaration for a reference
getDefaultRefDecl(Formula) - Static method in class jml2b.formula.BinaryForm
 
getDefaultRequires() - Method in class jack.plugin.JackJml2bConfiguration
 
getDefaultRequires() - Method in interface jml2b.IJml2bConfiguration
Returns the default requires clause
getDefaultRequires() - Method in class jml2b.Jml2bConfig
 
getDefiningClass() - Method in class jml2b.structure.bytecode.ClassField
 
getDefiningClass() - Method in class jml2b.structure.bytecode.ClassMethod
 
getDefiningClass() - Method in class jml2b.structure.java.Declaration
Returns the class that defines the declaration.
getDemoDecorator() - Static method in class jack.plugin.compile.CompilationUnitDecorator
 
getDepend() - Method in class jml2b.structure.jml.Represents
Returns the depends.
getDepends() - Method in class jml2b.structure.bytecode.ClassFile
 
getDepends() - Method in class jml2b.structure.java.AClass
 
getDepends() - Method in class jml2b.structure.java.Class
Returns an enumeration of the represents clauses defined in this class.
getDepends() - Method in class jml2b.structure.java.JmlFile
 
getDepends() - Method in class jpov.structure.JmlFile
 
getDimension() - Method in class jml2b.structure.java.Type
return the dimension of the type.
getDirectory() - Method in class jml2b.structure.java.Package
return the directory corresponding to this package.
getDirectory() - Method in class jpov.JpoFile
Returns the repository
getDisplayedName() - Method in class jml2b.pog.proofobligation.MethodPO
 
getDisplayedName() - Method in class jml2b.pog.proofobligation.ProofObligation
 
getDisplayedName() - Method in class jml2b.pog.proofobligation.StaticInitializationPO
 
getDisplayedName() - Method in class jml2b.pog.proofobligation.WellDefinedInvPO
 
getDisplayedName() - Method in class jml2b.pog.proofobligation.WellDefinedSpecPO
 
getE() - Method in class jml2b.structure.jml.SpecArrayExpr
 
getE1() - Method in class jml2b.structure.jml.SpecArrayDotDot
 
getE2() - Method in class jml2b.structure.jml.SpecArrayDotDot
 
getEhl() - Method in class jack.plugin.perspective.CaseExplorer
 
getElemType() - Method in class jml2b.formula.TTypeForm
 
getElemType() - Method in interface jml2b.structure.java.IType
 
getElemType() - Method in class jml2b.structure.java.Type
Returns the type of the elements of an array type.
getElements(Object) - Method in class jack.plugin.metrics.MetricsContentProvider
 
getElements(Object) - Method in class jack.plugin.prove.ProofContentProvider
 
getElements(Object) - Method in class jack.plugin.source.MethodListContentProvider
 
getElements(Object) - Method in class jpov.viewer.lemma.GoalContentProvider
If the inputElement is a goal, returns an array containing as first element the goal and as remaining elements each lines of the string resulting from the translatation of the goal.
getElements(Object) - Method in class jpov.viewer.lemma.HypContentProvider
If the inputElement is a lemma, returns the array of hypline containing the hypothesis corresponding to this lemma
getElements(Object) - Method in class jpov.viewer.tree.TreeContentProvider
 
getElementsName(Type) - Static method in class jml2b.formula.ElementsForm
Returns the xxxelements_n formula corresponding to a type.
getEndDate() - Method in class jack.plugin.prove.ProofTask
Returns the end date of the task.
getEndLine() - Method in class jml2b.structure.statement.StSpecBlock
 
getEnsures() - Method in class jml2b.structure.jml.SpecCase
Returns the content of the ensures clause.
getEnsuresAsExpression(IJml2bConfiguration) - Method in class jml2b.structure.java.Method
 
getErrorCount() - Static method in class jml2b.exceptions.ErrorHandler
Return the current error count.
getErrorDescription() - Method in class jack.plugin.RunnableWithError
Return a description of the error in case where hasSucceeded return false.
getErrorDescription() - Method in class jack.plugin.prove.ProofTask
Returns the description of the last error encountered.
getErrorDetails() - Method in class jack.plugin.RunnableWithError
Returns detail for the error, if available.
getErrorDetails() - Method in class jack.plugin.prove.ProofTask
Returns detail about the last error encountered.
getExceptionField() - Method in class jml2b.pog.lemma.ExsuresLemma
 
getExceptionType() - Method in class jml2b.pog.lemma.ExsuresLemma
Returns the exceptionType.
getExceptionType() - Method in class jml2b.structure.jml.Exsures
Returns the type of the exception.
getExp() - Method in class jml2b.formula.UnaryForm
Returns the leaf formula.
getExp() - Method in class jml2b.structure.statement.StAssert
 
getExp() - Method in class jml2b.structure.statement.UnaryExp
 
getExp() - Method in class jml2b.structure.statement.WithTypeExp
 
getExpression() - Method in class jml2b.structure.jml.Exsures
Returns the property ensured by this exsures clause.
getExsures(String, Vector) - Static method in class jml2b.structure.jml.Exsures
Stores the exsures clauses corresponding to str into v.
getExsures() - Method in class jml2b.structure.jml.SpecCase
Returns an Enumeration enumerating the content of the exsures clause.
getExsuresAsExpression(IJml2bConfiguration) - Method in class jml2b.structure.java.Method
 
getExsuresAsExpression() - Method in class jml2b.structure.jml.SpecCase
 
getF() - Method in class jml2b.pog.substitution.SubTypeof
Returns the formula corresponding to the extended typeof domain.
getF() - Method in class jpov.structure.VirtualFormula
Returns the f.
getF1() - Method in class jml2b.formula.TriaryForm
Returns the f1.
getFalse() - Static method in class jml2b.formula.Formula
Returns the formula false.
getFalse(IJml2bConfiguration) - Static method in class jml2b.pog.lemma.ExceptionalBehaviourStack
 
getFalse() - Static method in class jml2b.structure.statement.Expression
Returns the expression false.
getFgKeywords() - Method in class jack.plugin.edit.BCScanner
 
getFgKeywords() - Method in class jack.plugin.edit.JavaScanner
 
getFgcolor() - Method in class jack.plugin.edit.Box
 
getField(String) - Method in class jml2b.link.VarStack
Return the field with the given name.
getField() - Method in class jml2b.pog.substitution.SubMemberField
 
getField() - Method in class jml2b.pog.substitution.SubStaticOrLocalField
 
getField(String, AClass) - Method in class jml2b.structure.bytecode.ClassFile
 
getField(String) - Method in class jml2b.structure.java.AClass
Returns the field with the given name
getField(String, AClass) - Method in class jml2b.structure.java.AClass
 
getField(String, AClass) - Method in class jml2b.structure.java.Class
Gets the field named name if it is visible from the given class.
getField(int) - Method in class jml2b.structure.java.Parameters
 
getField() - Method in class jml2b.structure.jml.Exsures
Returns the field declared into the exsures clause.
getField() - Method in class jml2b.structure.jml.ModifiesIdent
Returns the field.
getField() - Method in class jml2b.structure.statement.QuantifiedVar
Returns the current field.
getFieldCount() - Method in class jml2b.structure.java.VarDeclParser
Returns the number of variables stored in the array.
getFields(Set) - Method in class jml2b.formula.BinaryForm
 
getFields(Set) - Method in class jml2b.formula.Formula
Collects the fields that occur in the formula.
getFields(Set) - Method in class jml2b.formula.QuantifiedForm
 
getFields(Set) - Method in class jml2b.formula.TTypeForm
 
getFields(Set) - Method in class jml2b.formula.TerminalForm
 
getFields(Set) - Method in class jml2b.formula.TriaryForm
 
getFields(Set) - Method in class jml2b.formula.UnaryForm
 
getFields(Set) - Method in class jml2b.pog.lemma.ExceptionalLemma
 
getFields(Set) - Method in class jml2b.pog.lemma.ExsuresLemma
 
getFields(Set) - Method in class jml2b.pog.lemma.Goal
 
getFields(Set) - Method in class jml2b.pog.lemma.Lemma
 
getFields(Set) - Method in class jml2b.pog.lemma.NormalLemma
 
getFields(Set) - Method in class jml2b.pog.lemma.Proofs
Collect the fields present in the current proof obligation.
getFields(Set) - Method in class jml2b.pog.lemma.SimpleLemma
 
getFields(Set) - Method in class jml2b.pog.lemma.TheoremList
 
getFields() - Method in class jml2b.structure.bytecode.ClassFile
 
getFields() - Method in class jml2b.structure.java.AClass
 
getFields() - Method in class jml2b.structure.java.Class
Returns an enumeration of the fields defined by the current class.
getFields() - Method in class jml2b.structure.jml.GuardedModifies
 
getFields() - Method in class jml2b.structure.jml.ModifiesClause
 
getFields() - Method in class jml2b.structure.jml.ModifiesList
 
getFields() - Method in class jpov.structure.Class
 
getFieldsV() - Method in class jml2b.structure.java.Class
 
getFile() - Method in class jml2b.util.FileUpdate
 
getFile() - Method in class jml2b.util.JmlClassEntryFile
 
getFile() - Method in class jml2b.util.JmlEntryFile
 
getFile() - Method in class jml2b.util.JmlEntryFileInJar
 
getFile() - Method in class jml2b.util.JmlFileEntry
 
getFileAST() - Method in class jml2b.structure.java.JmlFile
 
getFileGeneration(String) - Static method in class jack.plugin.JackPlugin
 
getFileName() - Method in class jack.plugin.prove.ProofTask
 
getFileName() - Method in class jml2b.structure.java.JmlFile
Return the filename corresponding to this file.
getFileName() - Method in class jpov.structure.JmlFile
Returns the currently displayed file
getFileNameAbsolutePath() - Method in class jml2b.structure.java.JmlFile
 
getFilePointer() - Method in class jml2b.util.JpoInputStream
 
getFilterType() - Method in class jack.plugin.metrics.MetricsFilterWindow
 
getFirstLine() - Method in class jml2b.structure.java.Class
 
getFirstLine() - Method in class jml2b.structure.java.Method
 
getFirstLine() - Method in class jpov.structure.Method
Returns the firstLine.
getFlatName() - Method in class jml2b.structure.java.JmlFile
Returns the "flat name" for this JmlFile.
getFlow() - Method in class jpov.structure.Lemma
Returns the array of boxes.
getFlow() - Method in class jpov.structure.LemmaHierarchy
 
getFlow() - Method in class jpov.structure.VirtualFormula
Returns the set of box associated to the formula.
getFormula() - Method in class jml2b.pog.lemma.Goal
Returns the goal
getFormula() - Method in class jml2b.pog.lemma.SimpleLemma
 
getFormula() - Method in class jml2b.pog.lemma.VirtualFormula
Returns the formula
getFormula() - Method in class jml2b.pog.util.ContextFromPureMethod
Returns the formula.
getFormula() - Method in class jpov.structure.Goal
Returns the formula.
getFormula() - Method in class jpov.viewer.lemma.HypLine
Returns the associated formula
getFormulaWithContext() - Method in class jml2b.pog.util.ContextFromPureMethod
Returns the result of the translation.
getFromString(String) - Static method in class jml2b.structure.statement.Expression
 
getFullyQualifiedName() - Method in class jml2b.structure.bytecode.ClassFile
 
getFullyQualifiedName() - Method in class jml2b.structure.java.AClass
 
getFullyQualifiedName() - Method in class jml2b.structure.java.Class
 
getFullyQualifiedName() - Method in class jml2b.structure.java.Package
Returns the fully qualified name of this package.
getGlobalMemberInvariant(IJml2bConfiguration) - Method in class jml2b.structure.java.Class
 
getGlobalMemberInvariantProof(IJml2bConfiguration) - Method in class jml2b.structure.java.Class
 
getGlobalStaticInvariant() - Method in class jml2b.structure.java.Class
Returns the global static invariant.
getGluingInvariant() - Method in class jml2b.structure.jml.Represents
Returns the gluing invariant.
getGm() - Method in class jml2b.structure.jml.ModifiesList
 
getGoal(int) - Method in class jml2b.pog.lemma.SimpleLemma
Returns a goal
getGoalType() - Method in class jpov.structure.Goal
Returns the origin of the goal
getGoalTypeString(byte, String) - Static method in class jml2b.pog.lemma.GoalOrigin
Returns a string describing the goal origin.
getGoals() - Method in class jml2b.pog.lemma.SimpleLemma
Returns the set of goals
getGoals() - Method in class jpov.structure.JmlFile
 
getGoals() - Method in class jpov.structure.Lemma
Returns the array of goals
getHyp() - Method in class jml2b.pog.lemma.Theorem
Returns the hypothesis
getHyp() - Method in class jpov.structure.Lemma
Returns the array of hypothesis.
getHyp() - Method in class jpov.structure.LemmaHierarchy
 
getHypSelection() - Method in class jpov.viewer.lemma.LemmaView
Return the selection corresponding to the currently selected hypothesis.
getHypTypeString(byte) - Static method in class jml2b.pog.lemma.VirtualFormula
Returns the string corresponding to an hypothesis type
getHypViewers() - Method in class jpov.viewer.lemma.LemmaView
Return an enumeration enumerating the different hypothesis viewers.
getIconDir() - Static method in class jack.plugin.JackPlugin
Returns the directory where the icons are stored.
getIdent() - Method in class jml2b.formula.TerminalForm
 
getIdent() - Method in class jml2b.structure.jml.ModifiesIdent
Returns the identidentifer.
getIdent() - Method in class jml2b.structure.statement.TerminalExp
Returns the identifier.
getImage(Object) - Method in class jack.plugin.source.MethodListLabelProvider
 
getImage(Object) - Method in class jpov.viewer.lemma.MyLabelProvider
Returns the image to display if the element corresponds to the first line of an hypothese or to a goal.
getImage(Object) - Method in class jpov.viewer.tree.TreeLabelProvider
Returns the image associated with the node depending of the proof rate and the fact that it is checked or not.
getImplements() - Method in class jml2b.structure.bytecode.ClassFile
 
getImplements() - Method in class jml2b.structure.java.AClass
 
getImplements() - Method in class jml2b.structure.java.Class
Returns an enumeration of the implemented interfaces.
getImportedClassPackage(String) - Method in class jml2b.link.LinkContext
return the package corresponding to the given imported class.
getImportedClassPackage(String) - Method in class jml2b.structure.java.JmlFile
return the package corresponding to the given imported class.
getImportedPackages() - Method in class jml2b.link.LinkContext
 
getImportedPackages() - Method in class jml2b.structure.java.JmlFile
 
getIndex(String) - Static method in class jml2b.languages.Languages
Returns the index of a given plugin name.
getIndex() - Method in class jml2b.pog.lemma.VirtualFormula
Returns the index of the formula
getIndex() - Method in class jml2b.pog.util.ColoredInfo
 
getIndex() - Method in class jpov.viewer.source.Box
 
getInfo() - Method in class jml2b.structure.AMethod
 
getInfo(String) - Method in class jml2b.structure.AMethod
 
getInfo() - Method in class jml2b.structure.bytecode.ClassMethod
 
getInfo(String) - Method in class jml2b.structure.bytecode.ClassMethod
 
getInfo() - Method in class jml2b.structure.java.Method
 
getInfo(String) - Method in class jml2b.structure.java.Method
 
getInfo() - Method in class jml2b.structure.jml.SpecCase
Returns the Java informations corresponding to this case
getInfo() - Method in class jml2b.structure.statement.StLoops
 
getInfo() - Method in class jpov.substitution.SubArrayElement
 
getInfo() - Method in class jpov.substitution.SubArrayElementSingle
 
getInfo() - Method in class jpov.substitution.SubArrayLength
Returns "arraylength == f"
getInfo() - Method in class jpov.substitution.SubForm
 
getInfo() - Method in class jpov.substitution.SubInstancesSet
If f is a singleton, returns "a new istance: f" else return "new instances: f".
getInfo() - Method in class jpov.substitution.SubInstancesSingle
 
getInfo() - Method in class jpov.substitution.SubMemberField
 
getInfo() - Method in class jpov.substitution.SubTmpVar
 
getInfo() - Method in class jpov.substitution.SubTypeofSet
Returns "typeof <- f t"
getInfo() - Method in class jpov.substitution.SubTypeofSingle
Returns "t f"
getInfo() - Method in interface jpov.substitution.Substitution
Returns the informations to displayed in the Java view to simulate the substitution
getInputStream() - Method in class jml2b.util.JmlEntryFile
 
getInputStream() - Method in class jml2b.util.JmlEntryFileInJar
 
getInstance() - Method in class jml2b.pog.substitution.SubMemberField
 
getInstanceConstraints() - Method in class jml2b.structure.java.Class
 
getInteger() - Static method in class jml2b.structure.java.Type
Returns a type corresponding to the int builtin type.
getInteractiveProverClass(String) - Static method in class jml2b.languages.Languages
Returns the interactive prover class instance for a given plugin name.
getInterfaces() - Method in class jml2b.pog.printers.ClassResolver
 
getInterfaces() - Method in interface jml2b.pog.printers.IClassResolver
 
getInvariant() - Method in class jml2b.structure.java.Invariant
Returns the expression corresponding to the invariant.
getInvariants() - Method in class jml2b.structure.java.Class
Returns an enumeration of the invariants defined by this class.
getJavaLang() - Static method in class jml2b.structure.java.Package
 
getJf() - Method in class jml2b.util.UpdatedJmlFile
 
getJmlFile() - Method in class jml2b.structure.java.ParsedItem
Returns the file.
getJmlFile() - Method in class jpov.JpoFile
Returns the associated JML file
getJmlFiles() - Method in class jml2b.pog.printers.ClassResolver
 
getJmlKeywordColor() - Static method in class jack.plugin.JackPlugin
 
getJmlParserTime() - Static method in class jml2b.structure.java.JmlFile
 
getJmlPath() - Method in class jack.plugin.JackJml2bConfiguration
 
getJmlPath(IProject) - Static method in class jack.plugin.JackPlugin
Returns the Jml search path preference.
getJmlPath() - Method in interface jml2b.IJml2bConfiguration
Returns the path where files have to be searched
getJmlPath() - Method in class jml2b.Jml2bConfig
 
getJpo(ICompilationUnit) - Static method in class jpov.PartialJpoFile
 
getJpoFile(ICompilationUnit) - Static method in class jack.plugin.JackPlugin
Returns the jpo file corresponding to the given compilation unit.
getJpoFile() - Method in class jack.plugin.perspective.CaseExplorer
 
getJpoFile() - Method in class jpov.structure.JmlFile
 
getJpoName() - Method in class jpov.JpoFile
Returns the JPO file name with the extension
getJpoPrefix(IFile) - Static method in class jack.plugin.JpovUtil
return the name of a .jpo file without its extension.
getLabels() - Method in class jml2b.structure.jml.SpecCase
Returns the labels.
getLabels() - Method in class jpov.viewer.tree.TreeItemSelection
Returns the set of labels
getLangNames() - Method in interface jml2b.structure.java.IJmlFile
 
getLangNames() - Method in class jml2b.structure.java.JmlFile
 
getLangNames() - Method in class jpov.structure.JmlFile
 
getLanguageClass(String) - Static method in class jml2b.languages.Languages
Returns the language class instance for a given plugin name.
getLanguagesNames() - Static method in class jml2b.languages.Languages
 
getLayout() - Method in class jack.plugin.perspective.CaseExplorer
 
getLayout() - Method in interface jack.plugin.perspective.ICaseExplorer
Returns the current layout
getLeft() - Method in class jml2b.formula.BinaryForm
Returns the left formula.
getLeft() - Method in class jml2b.formula.TriaryForm
Returns the left.
getLeft() - Method in class jml2b.structure.statement.BinaryExp
Returns the left expression.
getLeft() - Method in class jml2b.structure.statement.MethodCallExp
Returns the expression corresponding to the called method.
getLeft() - Method in class jml2b.structure.statement.QuestionExp
 
getLeftContent(Object) - Method in class jack.plugin.source.JmlMergeViewerContentProvider
 
getLeftE() - Method in class jml2b.structure.jml.ModifiesDot
 
getLeftImage(Object) - Method in class jack.plugin.source.JmlMergeViewerContentProvider
 
getLeftLabel(Object) - Method in class jack.plugin.source.JmlMergeViewerContentProvider
 
getLemma() - Method in class jml2b.pog.lemma.ExsuresLemma
Returns the lemma.
getLemma(int) - Method in class jml2b.pog.lemma.Proofs
 
getLemma(int) - Method in class jml2b.pog.lemma.TheoremList
Returns a lemma of a theorem of the list
getLemmaFilterWindow() - Method in class jpov.viewer.lemma.LemmaView
 
getLemmas() - Method in class jml2b.structure.java.Method
 
getLemmas() - Method in class jpov.structure.Method
Returns the lemmas.
getLemmas() - Method in class jpov.structure.Proofs
Return the lemmas array
getLemmasWithPo() - Method in class jpov.structure.LemmaHierarchy
 
getLemmasWithPo(int) - Method in class jpov.structure.Proofs
Returns an array containing lemmas with almost one goal
getLength() - Method in class jack.plugin.edit.JavaScanner
Returns the ending location of the current token in the document.
getLength() - Method in class jpov.viewer.source.Box
 
getLine() - Method in class jml2b.exceptions.LinkException
 
getLine() - Method in class jml2b.exceptions.TypeCheckException
 
getLine() - Method in class jml2b.structure.java.ParsedItem
Returns the line.
getLine() - Method in class jml2b.util.AddFileUpdate
 
getLine() - Method in class jml2b.util.FileUpdate
 
getLine() - Method in class jml2b.util.ReplaceFileUpdate
 
getLoadedFilesCount() - Static method in class jml2b.structure.java.JmlFile
 
getLocFlow() - Method in class jml2b.pog.lemma.Proofs
 
getLocHyp() - Method in class jml2b.pog.lemma.Proofs
Returns the hypothesis
getLoop(Vector) - Method in class jml2b.structure.statement.Expression
 
getLoop(Vector) - Method in class jml2b.structure.statement.StAssert
 
getLoop(Vector) - Method in class jml2b.structure.statement.StBlock
 
getLoop(Vector) - Method in class jml2b.structure.statement.StControlFlowBreak
 
getLoop(Vector) - Method in class jml2b.structure.statement.StDoWhile
 
getLoop(Vector) - Method in class jml2b.structure.statement.StFor
 
getLoop(Vector) - Method in class jml2b.structure.statement.StIf
 
getLoop(Vector) - Method in class jml2b.structure.statement.StImplementsLabel
 
getLoop(Vector) - Method in class jml2b.structure.statement.StLabel
 
getLoop(Vector) - Method in class jml2b.structure.statement.StSequence
 
getLoop(Vector) - Method in class jml2b.structure.statement.StSkip
 
getLoop(Vector) - Method in class jml2b.structure.statement.StSpecBlock
 
getLoop(Vector) - Method in class jml2b.structure.statement.StSwitch
 
getLoop(Vector) - Method in class jml2b.structure.statement.StTry
 
getLoop(Vector) - Method in class jml2b.structure.statement.StVarDecl
 
getLoop(Vector) - Method in class jml2b.structure.statement.Statement
 
getLoopAtLine(int) - Method in class jml2b.structure.java.Method
 
getLoopAtLine(int) - Method in class jml2b.structure.statement.StBlock
 
getLoopAtLine(int) - Method in class jml2b.structure.statement.StDoWhile
 
getLoopAtLine(int) - Method in class jml2b.structure.statement.StFor
 
getLoopAtLine(int) - Method in class jml2b.structure.statement.StSequence
 
getLoopAtLine(int) - Method in class jml2b.structure.statement.StTry
 
getLoopAtLine(int) - Method in class jml2b.structure.statement.Statement
 
getLoop_exsures() - Method in class jml2b.structure.statement.StLoops
Returns the loop exsures clause.
getLoop_invariant() - Method in class jml2b.structure.statement.StLoops
Returns the loop invariant.
getLoop_modifies() - Method in class jml2b.structure.statement.StLoops
Returns the loop modifies clause.
getLoop_variant() - Method in class jml2b.structure.statement.StLoops
 
getLtype() - Method in class jml2b.formula.BasicType
 
getM() - Method in class jml2b.structure.jml.GuardedModifies
Returns the modified store ref.
getM() - Method in class jml2b.structure.jml.ModifiesDot
Returns the member field.
getM() - Method in class jml2b.structure.jml.ModifiesLbrack
Returns the modified variable.
getMaxGoalType() - Static method in class jml2b.pog.lemma.GoalOrigin
Returns the number of goal origin types.
getMaxHypType() - Static method in class jml2b.pog.lemma.VirtualFormula
Returns the number of hypothese type
getMaxProofRunning() - Static method in class jack.plugin.JackPlugin
Returns the integer indicating the maximum number of running proof tasks.
getMemberInvariants() - Method in class jml2b.structure.bytecode.ClassFile
 
getMemberInvariants() - Method in class jml2b.structure.java.AClass
 
getMemberInvariants() - Method in class jml2b.structure.java.Class
Returns an enumeration of the member invariants.
getMessage() - Method in class jml2b.exceptions.LinkException
 
getMessage() - Method in class jml2b.exceptions.TypeCheckException
 
getMethod() - Method in class jml2b.pog.proofobligation.MethodPO
Returns the currentmethod.
getMethod(String, Parameters) - Method in class jml2b.structure.bytecode.ClassFile
 
getMethod(String, Parameters) - Method in class jml2b.structure.java.AClass
 
getMethod(String, Parameters) - Method in class jml2b.structure.java.Class
Searches for a method with the given name and parameters in the current class.
getMethodPercent() - Method in class jpov.viewer.tree.TreeFilterWindow
Returns the upper proof percentage bound for a method to be displayed.
getMethods() - Method in class jml2b.structure.java.Class
Returns an enumeration of the methods declared by the current class.
getMethods() - Method in class jpov.structure.Class
Returns the methods array.
getModifiers() - Method in class jml2b.structure.bytecode.ClassField
 
getModifiers() - Method in class jml2b.structure.bytecode.ClassFile
 
getModifiers() - Method in class jml2b.structure.bytecode.ClassMethod
 
getModifiers() - Method in class jml2b.structure.java.AClass
 
getModifiers() - Method in class jml2b.structure.java.Class
Returns the modifiers associated to the current class.
getModifiers() - Method in class jml2b.structure.java.Declaration
Returns the visibility modifiers associated to this declaration.
getModifiers() - Method in class jml2b.structure.jml.SpecCase
Returns the modifier associated to this SpecCase.
getModifies() - Method in class jml2b.structure.jml.SpecCase
Returns the content of the modifies clause.
getMultiCommentJmlColor() - Static method in class jack.plugin.JackPlugin
 
getName() - Method in class jml2b.pog.lemma.Theorem
Returns the name of the theorem.
getName() - Method in class jml2b.structure.AMethod
 
getName() - Method in class jml2b.structure.bytecode.ClassDefaultConstructor
 
getName() - Method in class jml2b.structure.bytecode.ClassField
 
getName() - Method in class jml2b.structure.bytecode.ClassFile
 
getName() - Method in class jml2b.structure.bytecode.ClassMethod
 
getName() - Method in class jml2b.structure.java.AClass
 
getName() - Method in class jml2b.structure.java.Class
Returns the name of the class.
getName() - Method in class jml2b.structure.java.Field
Returns the name of the field.
getName() - Method in class jml2b.structure.java.Identifier
 
getName() - Method in class jml2b.structure.java.Invariant
Returns the name of the invariant.
getName() - Method in class jml2b.structure.java.Method
 
getName() - Method in class jml2b.structure.java.NamedNode
 
getName() - Method in class jml2b.structure.java.Package
 
getName() - Method in class jml2b.structure.jml.Depends
 
getName() - Method in class jml2b.structure.jml.Represents
 
getName() - Method in class jml2b.util.JmlClassEntryFile
 
getName() - Method in class jml2b.util.JmlEntryFile
 
getName() - Method in class jml2b.util.JmlEntryFileInJar
 
getName() - Method in class jml2b.util.JmlFileEntry
 
getName() - Method in class jpov.JpoFile
Returns the JPO file name
getName() - Method in class jpov.PartialJpoFile
 
getName() - Method in class jpov.structure.Class
 
getName() - Method in class jpov.structure.Field
 
getName() - Method in class jpov.structure.Lemma
Returns the name of the method to which this case belongs.
getName() - Method in class jpov.structure.Method
 
getNameForModifies() - Method in interface jml2b.formula.IModifiesField
 
getNameForModifies() - Method in class jml2b.structure.AMethod
 
getNameForModifies() - Method in class jml2b.structure.statement.StLoops
 
getNameForModifies() - Method in class jml2b.structure.statement.StSpecBlock
 
getNbCheckedPo() - Method in class jpov.structure.Class
 
getNbCheckedPo() - Method in class jpov.structure.JmlFile
 
getNbCheckedPo() - Method in class jpov.structure.Lemma
 
getNbCheckedPo() - Method in class jpov.structure.Method
 
getNbCheckedPo() - Method in class jpov.structure.Proofs
 
getNbLanguages() - Static method in class jml2b.languages.Languages
 
getNbPOProved(String) - Method in class jpov.structure.PartialJmlFile
 
getNbPo() - Method in class jml2b.structure.java.JmlFile
 
getNbPo() - Method in class jpov.structure.Class
 
getNbPo() - Method in class jpov.structure.Goal
 
getNbPo() - Method in class jpov.structure.JmlFile
 
getNbPo() - Method in class jpov.structure.Lemma
 
getNbPo() - Method in class jpov.structure.LemmaHierarchy
 
getNbPo() - Method in class jpov.structure.Method
 
getNbPo() - Method in class jpov.structure.PartialJmlFile
 
getNbPo() - Method in class jpov.structure.Proofs
 
getNbPo() - Method in class jpov.structure.TreeObject
Returns the number of proof obligations for this node.
getNbPoProved(String) - Method in class jml2b.structure.java.JmlFile
 
getNbPoProved() - Method in class jml2b.structure.java.JmlFile
 
getNbPoProved() - Method in class jpov.structure.Class
 
getNbPoProved(String) - Method in class jpov.structure.Class
 
getNbPoProved(String) - Method in class jpov.structure.Goal
 
getNbPoProved() - Method in class jpov.structure.Goal
 
getNbPoProved(String) - Method in class jpov.structure.JmlFile
 
getNbPoProved() - Method in class jpov.structure.JmlFile
 
getNbPoProved() - Method in class jpov.structure.Lemma
 
getNbPoProved(String) - Method in class jpov.structure.Lemma
 
getNbPoProved(String) - Method in class jpov.structure.LemmaHierarchy
 
getNbPoProved() - Method in class jpov.structure.LemmaHierarchy
 
getNbPoProved() - Method in class jpov.structure.Method
 
getNbPoProved(String) - Method in class jpov.structure.Method
 
getNbPoProved() - Method in class jpov.structure.PartialJmlFile
 
getNbPoProved() - Method in class jpov.structure.Proofs
 
getNbPoProved(String) - Method in class jpov.structure.Proofs
 
getNbPoProved(String) - Method in class jpov.structure.TreeObject
Returns the number of proved proof obligations for this node.
getNbPoProved() - Method in class jpov.structure.TreeObject
Returns the number of proved proof obligations for this node.
getNewF() - Method in class jml2b.util.UpdatedJmlFile
 
getNext() - Method in class jml2b.formula.QuantifiedVarForm
 
getNext() - Method in class jml2b.structure.jml.ModifiesList
 
getNext() - Method in class jml2b.structure.statement.QuantifiedVar
Returns the next element of the list.
getNodeText() - Method in class jml2b.formula.TTypeForm
 
getNodeText() - Method in class jml2b.formula.TerminalForm
Returns the nodeText.
getNodeText() - Method in class jml2b.structure.statement.Expression
Returns the nodeText.
getNodeType() - Method in class jml2b.formula.Formula
Returns the nodeType.
getNodeType() - Method in class jml2b.structure.statement.Expression
Returns the nodeType.
getNodeType() - Method in class jml2b.structure.statement.StLoops
Returns the node type.
getNonAmbiguousName() - Method in class jml2b.formula.TerminalForm
 
getNormalizedEnsures(IJml2bConfiguration) - Method in class jml2b.structure.AMethod
 
getNormalizedEnsures(IJml2bConfiguration) - Method in class jml2b.structure.bytecode.ClassMethod
 
getNormalizedEnsures(IJml2bConfiguration) - Method in class jml2b.structure.java.Method
 
getNormalizedEnsures() - Method in class jml2b.structure.jml.SpecCase
Returns the ensures clause guarded by the requires clause
getNormalizedRequires(IJml2bConfiguration) - Method in class jml2b.structure.AMethod
 
getNormalizedRequires(IJml2bConfiguration) - Method in class jml2b.structure.bytecode.ClassMethod
 
getNormalizedRequires(IJml2bConfiguration) - Method in class jml2b.structure.java.Method
 
getNull() - Static method in class jml2b.formula.Formula
Returns the formula null.
getNull() - Static method in class jml2b.structure.statement.Expression
Returns the expression null.
getNum() - Method in class jpov.structure.Lemma
 
getNum() - Method in class jpov.viewer.lemma.HypLine
Returns the line number
getNumPos() - Method in class jack.plugin.prove.ProofTask
 
getNumPos() - Method in class jpov.JpoFile
Returns the number of proof obligations.
getNumToTry() - Method in class jack.plugin.prove.ProofTask
Returns the number of proof obligations that still have to be tried.
getNumber() - Method in class jpov.structure.Goal
Returns the number associated with this goal in the .po file of the Atelier B
getObject(IJml2bConfiguration) - Static method in class jml2b.structure.java.Type
Returns a type corresponding to the java.lang.Object class.
getObviousPoGeneration() - Static method in class jack.plugin.JackPlugin
Returns the boolean indicating obvious goal generation.
getObviousProverClass(String) - Static method in class jml2b.languages.Languages
Returns the obvious prover class instance for a given plugin name.
getOrigin() - Method in class jml2b.pog.lemma.GoalOrigin
Returns the origin of the goal.
getOrigin() - Method in class jml2b.pog.lemma.VirtualFormula
Returns the origin.
getOrigin() - Method in class jpov.structure.VirtualFormula
Returns the origin.
getOrigin() - Method in class jpov.viewer.lemma.HypLine
Returns the origin of the associated formula.
getOriginString() - Method in class jpov.structure.Goal
Returns a string describing the goal origin.
getOriginal() - Method in class jpov.structure.Goal
 
getOutputDir(IProject) - Static method in class jack.plugin.JackPlugin
Returns the ouput directory for the given project.
getOutputDir(String) - Static method in class jml2b.Jml2b
Returns a File object corresponding to the given directory.
getOwnFields() - Method in class jml2b.structure.bytecode.ClassFile
 
getOwnFields() - Method in class jml2b.structure.java.AClass
 
getOwnFields() - Method in class jml2b.structure.java.Class
Returns a vector containing all the fields defined by the current class and its super classes.
getPackage() - Method in class jml2b.link.LinkContext
 
getPackage() - Method in class jml2b.link.LinkInfo
 
getPackage() - Method in class jml2b.structure.bytecode.ClassFile
 
getPackage() - Method in class jml2b.structure.java.AClass
 
getPackage() - Method in class jml2b.structure.java.Class
Returns the package this class belongs to.
getPackage() - Method in class jml2b.structure.java.JmlFile
 
getPackage(String) - Method in class jml2b.structure.java.Package
Search for the given package inside this package.
getParameters() - Method in class jml2b.structure.java.Parameters
 
getParams() - Method in class jml2b.structure.AMethod
 
getParams() - Method in class jml2b.structure.bytecode.ClassDefaultConstructor
 
getParams() - Method in class jml2b.structure.bytecode.ClassMethod
 
getParams() - Method in class jml2b.structure.java.Method
 
getParamsString() - Method in class jml2b.structure.java.Method
 
getParent() - Method in class jml2b.structure.java.Package
 
getParent() - Method in class jpov.structure.TreeObject
Gets the parent of the node
getParent(Object) - Method in class jpov.viewer.tree.TreeContentProvider
 
getParsedItems() - Method in interface jml2b.structure.jml.JmlExpression
Returns the set of parsed items that correspond to this expression
getParsedItems() - Method in class jml2b.structure.jml.Represents
 
getParsedItems() - Method in class jml2b.structure.statement.ArrayInitializer
 
getParsedItems() - Method in class jml2b.structure.statement.BinaryExp
 
getParsedItems() - Method in class jml2b.structure.statement.Expression
Returns the set of parsed items that correspond to this expression
getParsedItems() - Method in class jml2b.structure.statement.IsSubtypeOfExp
 
getParsedItems() - Method in class jml2b.structure.statement.MethodCallExp
 
getParsedItems() - Method in class jml2b.structure.statement.QuantifiedExp
 
getParsedItems() - Method in class jml2b.structure.statement.QuantifiedVar
Returns the set of parsed items that correspond to this expression
getParsedItems() - Method in class jml2b.structure.statement.QuestionExp
 
getParsedItems() - Method in class jml2b.structure.statement.TTypeExp
 
getParsedItems() - Method in class jml2b.structure.statement.TerminalExp
 
getParsedItems() - Method in class jml2b.structure.statement.UnaryExp
 
getParsedItems() - Method in class jml2b.structure.statement.WithTypeExp
 
getPartialJmlFile() - Method in class jpov.PartialJpoFile
Returns the associated JML file
getPath() - Method in class jack.plugin.JackPathEditor
Returns the path list as an array of String.
getPmiName() - Method in class jml2b.structure.java.Method
 
getPmiName() - Method in class jpov.structure.Method
Returns the method pmi name
getPoProved() - Method in class jack.plugin.prove.ProofTask
Returns the number of proved proof obligations.
getPoTried() - Method in class jack.plugin.prove.ProofTask
Returns the number of proof obligations that have already been tried.
getPrecondition(IJml2bConfiguration, ModifiableSet, Vector, Vector) - Method in class jml2b.structure.statement.ArrayInitializer
 
getPrecondition(IJml2bConfiguration, ModifiableSet, Vector, Vector) - Method in class jml2b.structure.statement.BinaryExp
 
getPrecondition(IJml2bConfiguration, ModifiableSet, Vector, Vector) - Method in class jml2b.structure.statement.IsSubtypeOfExp
 
getPrecondition(IJml2bConfiguration, ModifiableSet, Vector, Vector) - Method in class jml2b.structure.statement.MethodCallExp
 
getPrecondition(IJml2bConfiguration, ModifiableSet, Vector, Vector) - Method in class jml2b.structure.statement.QuantifiedExp
 
getPrecondition(IJml2bConfiguration, ModifiableSet, Vector, Vector) - Method in class jml2b.structure.statement.QuestionExp
 
getPrecondition(IJml2bConfiguration, ModifiableSet, Vector, Vector) - Method in class jml2b.structure.statement.StAssert
 
getPrecondition(IJml2bConfiguration, ModifiableSet, Vector, Vector) - Method in class jml2b.structure.statement.StBlock
 
getPrecondition(IJml2bConfiguration, ModifiableSet, Vector, Vector) - Method in class jml2b.structure.statement.StControlFlowBreak
 
getPrecondition(IJml2bConfiguration, ModifiableSet, Vector, Vector) - Method in class jml2b.structure.statement.StDoWhile
 
getPrecondition(IJml2bConfiguration, ModifiableSet, Vector, Vector) - Method in class jml2b.structure.statement.StFor
 
getPrecondition(IJml2bConfiguration, ModifiableSet, Vector, Vector) - Method in class jml2b.structure.statement.StIf
 
getPrecondition(IJml2bConfiguration, ModifiableSet, Vector, Vector) - Method in class jml2b.structure.statement.StImplementsLabel
 
getPrecondition(IJml2bConfiguration, ModifiableSet, Vector, Vector) - Method in class jml2b.structure.statement.StLabel
 
getPrecondition(IJml2bConfiguration, ModifiableSet, Vector, Vector) - Method in class jml2b.structure.statement.StSequence
 
getPrecondition(IJml2bConfiguration, ModifiableSet, Vector, Vector) - Method in class jml2b.structure.statement.StSkip
 
getPrecondition(IJml2bConfiguration, ModifiableSet, Vector, Vector) - Method in class jml2b.structure.statement.StSpecBlock
 
getPrecondition(IJml2bConfiguration, ModifiableSet, Vector, Vector) - Method in class jml2b.structure.statement.StSwitch
 
getPrecondition(IJml2bConfiguration, ModifiableSet, Vector, Vector) - Method in class jml2b.structure.statement.StTry
 
getPrecondition(IJml2bConfiguration, ModifiableSet, Vector, Vector) - Method in class jml2b.structure.statement.StVarDecl
 
getPrecondition(IJml2bConfiguration, ModifiableSet, Vector, Vector) - Method in class jml2b.structure.statement.Statement
 
getPrecondition(IJml2bConfiguration, ModifiableSet, Vector, Vector) - Method in class jml2b.structure.statement.TTypeExp
 
getPrecondition(IJml2bConfiguration, ModifiableSet, Vector, Vector) - Method in class jml2b.structure.statement.TerminalExp
 
getPrecondition(IJml2bConfiguration, ModifiableSet, Vector, Vector) - Method in class jml2b.structure.statement.UnaryExp
 
getPrecondition(IJml2bConfiguration, ModifiableSet, Vector, Vector) - Method in class jml2b.structure.statement.WithTypeExp
 
getPrinterClass(String) - Static method in class jml2b.languages.Languages
Returns the printer class instance for a given plugin name.
getPriority() - Method in class jml2b.languages.java.JavaTranslationResult
 
getProofTaskClasses() - Static method in class jml2b.languages.Languages
Returns the enumeration of proof task classes
getProperty(IResource, QualifiedName, String) - Method in class jack.plugin.JackPlugin
Return the property property_name for the given resource.
getProverName() - Method in class jack.plugin.prove.ProofTask
return the name of the prover used by this ProofTask.
getProverStatus(String) - Method in class jml2b.pog.lemma.GoalStatus
Returns the prove force.
getProverStatus(String) - Method in class jpov.structure.Goal
 
getProverStatusClass(String) - Static method in class jml2b.languages.Languages
Returns the prover status class instance for a given plugin name.
getRefType() - Method in class jml2b.formula.TTypeForm
 
getRefType() - Method in interface jml2b.structure.java.IType
 
getRefType() - Method in class jml2b.structure.java.Type
Returns the reference type for references or array types.
getRelativeFile(File, File) - Static method in class jack.plugin.compile.PoGeneratorErrorHandler
Return the path of children relative to root.
getRepresents() - Method in class jml2b.structure.bytecode.ClassFile
 
getRepresents() - Method in class jml2b.structure.java.AClass
 
getRepresents() - Method in class jml2b.structure.java.Class
Returns an enumeration of the represents clauses defined in this class.
getRequires() - Method in class jml2b.structure.AMethod
 
getRequires() - Method in class jml2b.structure.bytecode.ClassMethod
 
getRequires() - Method in class jml2b.structure.java.Method
 
getRequires() - Method in class jml2b.structure.jml.SpecCase
Returns the content of the requires clause.
getResource(String) - Static method in class jack.plugin.JpovUtil
Return the eclipse resource corresponding to the given JmlFile.
getResourceBundle() - Method in class jack.plugin.JackPlugin
Returns the plugin's resource bundle,
getResourceString(String) - Static method in class jack.plugin.JackPlugin
Returns the string from the plugin's resource bundle, or 'key' if not found.
getReturnCode() - Method in class jack.plugin.compile.CompileMessageDialog
 
getReturnCode() - Method in class jack.plugin.edit.SaveMessageDialog
 
getReturnType() - Method in class jml2b.structure.AMethod
 
getReturnType() - Method in class jml2b.structure.bytecode.ClassDefaultConstructor
 
getReturnType() - Method in class jml2b.structure.bytecode.ClassMethod
 
getReturnType() - Method in class jml2b.structure.java.Method
 
getRight() - Method in class jml2b.formula.BinaryForm
Returns the right formula.
getRight() - Method in class jml2b.formula.TriaryForm
Returns the right.
getRight() - Method in class jml2b.structure.statement.BinaryExp
Returns the right expression.
getRight() - Method in class jml2b.structure.statement.MethodCallExp
 
getRight() - Method in class jml2b.structure.statement.QuestionExp
 
getRightContent(Object) - Method in class jack.plugin.source.JmlMergeViewerContentProvider
 
getRightImage(Object) - Method in class jack.plugin.source.JmlMergeViewerContentProvider
 
getRightLabel(Object) - Method in class jack.plugin.source.JmlMergeViewerContentProvider
 
getRmiUrl() - Method in class jml2b.Jml2bConfig
 
getRoot() - Static method in class jml2b.structure.java.Package
 
getRtype() - Method in class jml2b.formula.BasicType
 
getSa() - Method in class jml2b.structure.jml.ModifiesLbrack
 
getSelectedGoals() - Method in class jpov.viewer.tree.TreeItemSelection
 
getSelectedTable() - Method in class jpov.viewer.lemma.LemmaView
 
getSelection() - Method in class jack.plugin.ToolbarButton
Returns the current selection.
getSerializedImageRoots(IProject) - Static method in class jack.plugin.JackPlugin
Returns the list of fully qualifed class name corresponding to the additional roots used for generating the serialized image.
getSet() - Method in class jml2b.util.ModifiableSet
 
getShort() - Static method in class jml2b.structure.java.Type
 
getShowTypes(int) - Method in class jpov.viewer.tree.TreeFilterWindow
Returns whether a goal type should be displayed or not.
getSignature() - Method in class jml2b.structure.AMethod
 
getSignature() - Method in class jml2b.structure.bytecode.ClassDefaultConstructor
 
getSignature() - Method in class jml2b.structure.bytecode.ClassMethod
 
getSignature() - Method in class jml2b.structure.java.Method
 
getSignature() - Method in class jml2b.structure.java.Parameters
 
getSingleCommentJmlColor() - Static method in class jack.plugin.JackPlugin
 
getSp() - Method in class jml2b.structure.statement.StSpecBlock
 
getSpecBlock(Vector) - Method in class jml2b.structure.statement.Expression
 
getSpecBlock(Vector) - Method in class jml2b.structure.statement.StAssert
 
getSpecBlock(Vector) - Method in class jml2b.structure.statement.StBlock
 
getSpecBlock(Vector) - Method in class jml2b.structure.statement.StControlFlowBreak
 
getSpecBlock(Vector) - Method in class jml2b.structure.statement.StDoWhile
 
getSpecBlock(Vector) - Method in class jml2b.structure.statement.StFor
 
getSpecBlock(Vector) - Method in class jml2b.structure.statement.StIf
 
getSpecBlock(Vector) - Method in class jml2b.structure.statement.StImplementsLabel
 
getSpecBlock(Vector) - Method in class jml2b.structure.statement.StLabel
 
getSpecBlock(Vector) - Method in class jml2b.structure.statement.StSequence
 
getSpecBlock(Vector) - Method in class jml2b.structure.statement.StSkip
 
getSpecBlock(Vector) - Method in class jml2b.structure.statement.StSpecBlock
 
getSpecBlock(Vector) - Method in class jml2b.structure.statement.StSwitch
 
getSpecBlock(Vector) - Method in class jml2b.structure.statement.StTry
 
getSpecBlock(Vector) - Method in class jml2b.structure.statement.StVarDecl
 
getSpecBlock(Vector) - Method in class jml2b.structure.statement.Statement
 
getSpecCases(IJml2bConfiguration) - Method in class jml2b.structure.AMethod
 
getSpecCases(IJml2bConfiguration) - Method in class jml2b.structure.bytecode.ClassMethod
 
getSpecCases(IJml2bConfiguration) - Method in class jml2b.structure.java.Method
Returns the specCases elements.
getSpecCasesV(IJml2bConfiguration) - Method in class jml2b.structure.java.Method
Returns the specCases.
getSpecType() - Method in class jml2b.structure.java.Method
 
getStartDate() - Method in class jack.plugin.prove.ProofTask
Return the start date of teh task.
getStartLine() - Method in class jml2b.structure.statement.StSpecBlock
 
getStartOffset() - Method in class jack.plugin.edit.JavaScanner
Returns the starting location of the current token in the document.
getState() - Method in class jack.plugin.prove.ProofTask
Returns the state of the task.
getState() - Method in class jpov.structure.Goal
 
getStateType() - Method in class jml2b.structure.statement.Expression
Returns the stateType.
getStaticConstraints() - Method in class jml2b.structure.java.Class
 
getStaticFinalFieldsInvariant() - Method in class jml2b.structure.bytecode.ClassFile
 
getStaticFinalFieldsInvariant() - Method in class jml2b.structure.java.AClass
 
getStaticFinalFieldsInvariant() - Method in class jml2b.structure.java.Class
Returns an enumeration of the invariants corresponding to static final fields.
getStaticFinalFieldsInvariants() - Method in class jml2b.structure.bytecode.ClassFile
 
getStaticFinalFieldsInvariants() - Method in class jml2b.structure.java.AClass
 
getStaticFinalFieldsInvariants() - Method in class jml2b.structure.java.Class
 
getStaticInitLemmas() - Method in class jml2b.structure.java.Class
 
getStaticInitLemmas() - Method in class jpov.structure.Class
Returns the static initialization lemmas.
getStaticInvariants() - Method in class jml2b.structure.bytecode.ClassFile
 
getStaticInvariants() - Method in class jml2b.structure.java.AClass
 
getStaticInvariants() - Method in class jml2b.structure.java.Class
Returns an enumeration of the static invariants defined by this class.
getString() - Method in class jml2b.util.FileUpdate
 
getStringState() - Method in class jack.plugin.prove.ProofTask
 
getSubPackages() - Method in class jml2b.structure.java.Package
 
getSubType() - Method in class jml2b.structure.statement.IsSubtypeOfExp
 
getSubdirectory() - Method in class jack.plugin.JackJml2bConfiguration
 
getSubdirectory() - Method in interface jml2b.IJml2bConfiguration
Returns the directory where the files have to be read and write.
getSubdirectory() - Method in class jml2b.Jml2bConfig
 
getSubs() - Method in class jml2b.pog.lemma.Goal
Returns the set of substitutions.
getSubs() - Method in class jpov.structure.Goal
 
getSuper() - Method in class jml2b.structure.java.AClass
Returns a type corresponding to the type of the super class.
getSuperClass() - Method in class jml2b.structure.java.AClass
Returns the super class of the current class.
getSuperDefaultConstructor() - Method in class jml2b.structure.java.AClass
Returns the default constructor for the super class.
getSuperMethod() - Method in class jml2b.structure.java.Method
 
getT() - Method in class jml2b.pog.substitution.SubTypeof
Returns the formula corresponding to the value asociated to new domain.
getTag() - Method in class jml2b.formula.BasicType
 
getTag() - Method in class jml2b.formula.TTypeForm
 
getTag() - Method in interface jml2b.structure.java.IType
 
getTag() - Method in class jml2b.structure.java.Type
Returns the tag describing the type of the type.
getTargetedClass() - Method in class jml2b.structure.java.Type
Returns the class that is the type of the object or of the element of the type if it is an array.
getText(Object) - Method in class jack.plugin.source.MethodListLabelProvider
 
getText(int) - Method in class jpov.structure.Class
Returns the name of the class
getText(int) - Method in class jpov.structure.Goal
 
getText(int) - Method in class jpov.structure.JmlFile
 
getText(int) - Method in class jpov.structure.Lemma
 
getText(int) - Method in class jpov.structure.LemmaHierarchy
 
getText(int) - Method in class jpov.structure.Method
 
getText(int) - Method in class jpov.structure.Proofs
 
getText(int) - Method in class jpov.structure.StaticInitProofs
 
getText(int) - Method in class jpov.structure.TreeObject
Returns the displayed text for this node.
getText(int) - Method in class jpov.structure.WellDefInvProofs
 
getText(int) - Method in class jpov.structure.WellDefinedMethodProofs
 
getText(Object) - Method in class jpov.viewer.lemma.MyLabelProvider
Returns the text associated with an hypothese line or with the goal.
getText(Object) - Method in class jpov.viewer.tree.TreeLabelProvider
Returns the text associated with the node.
getTheorem(int) - Method in class jml2b.pog.lemma.Proofs
 
getTheorem(int) - Method in class jml2b.pog.lemma.TheoremList
Returns a theoram of the list
getThl() - Method in class jml2b.pog.lemma.Proofs
Returns the list of theorems.
getTranslationResultClass(String) - Static method in class jml2b.languages.Languages
Returns the translation result class instance for a given plugin name.
getTree() - Method in class jack.plugin.perspective.CaseExplorer
 
getTree() - Method in interface jack.plugin.perspective.ICaseExplorer
 
getTreeSelection() - Method in class jack.plugin.perspective.CaseExplorer
Returns the selected items
getTreeSelection() - Method in interface jack.plugin.perspective.ICaseExplorer
 
getTrue(IJml2bConfiguration) - Static method in class jml2b.pog.lemma.Theorem
 
getTrue() - Static method in class jml2b.structure.statement.Expression
Returns the expression true.
getType() - Method in class jml2b.formula.ElementsForm
Returns the B type of the formula.
getType() - Method in class jml2b.formula.QuantifiedVarForm
 
getType() - Method in class jml2b.link.LinkInfo
 
getType() - Method in class jml2b.structure.AField
 
getType(int) - Method in class jml2b.structure.IAParameters
 
getType(IJml2bConfiguration, Type) - Static method in class jml2b.structure.bytecode.ClassField
 
getType() - Method in class jml2b.structure.bytecode.ClassField
 
getType(int) - Method in class jml2b.structure.bytecode.ClassParameters
 
getType() - Method in class jml2b.structure.java.Field
Retursn the type of the field.
getType(int) - Method in class jml2b.structure.java.Parameters
 
getType() - Static method in class jml2b.structure.java.Type
Returns a type corresponding to the type builtin type.
getType() - Method in class jml2b.structure.statement.IsSubtypeOfExp
 
getType() - Method in class jml2b.structure.statement.WithTypeExp
 
getTypesException(Set) - Method in class jml2b.pog.lemma.ExceptionalLemma
 
getTypesException(Set) - Method in class jml2b.pog.lemma.ExsuresLemma
Adds the exception type to the set
getTypesException(Set) - Method in class jml2b.pog.lemma.Lemma
Collects all the exception type that are declared in the exsures lemma of this lemma.
getUniqString(String) - Static method in class jpov.UniqString
Returns the instance of a string stored in the table.
getUpdated(int) - Method in class jack.plugin.source.JmlClauseGenerator
 
getUpdater() - Method in class jml2b.structure.statement.StFor
Returns the updater statement.
getValue() - Method in class jml2b.structure.statement.BinaryExp
 
getValue() - Method in class jml2b.structure.statement.Expression
Return the value associated to a constant expression.
getValue() - Method in class jml2b.structure.statement.MethodCallExp
 
getValue() - Method in class jml2b.structure.statement.QuestionExp
 
getValue() - Method in class jml2b.structure.statement.TerminalExp
 
getValue() - Method in class jml2b.structure.statement.UnaryExp
 
getValue() - Method in class jml2b.structure.statement.WithTypeExp
 
getVar() - Method in class jml2b.formula.QuantifiedVarForm
 
getVars() - Method in class jml2b.structure.java.VarDeclParser
Returns an enumeration of the parsed variables.
getVars() - Method in class jml2b.structure.statement.QuantifiedExp
 
getVf() - Method in class jpov.structure.Goal
Returns the virtual formula.
getViewerFont() - Method in class jack.plugin.JackJml2bConfiguration
 
getViewerFont() - Static method in class jack.plugin.JackPlugin
 
getViewerFont() - Method in interface jml2b.IJml2bConfiguration
Returns the font data to use to display to source code text
getViewerFont() - Method in class jml2b.Jml2bConfig
 
getWarningCount() - Static method in class jml2b.exceptions.ErrorHandler
Return the current warning count.
getWellDefInvLemmas() - Method in class jml2b.structure.java.Class
 
getWellDefInvLemmas() - Method in class jpov.structure.Class
 
getWellDefPoGeneration() - Static method in class jack.plugin.JackPlugin
 
getWellDefinednessLemmas() - Method in class jml2b.structure.java.Method
 
getWellDefinednessLemmas() - Method in class jpov.structure.Method
 
getWindow() - Method in class jack.plugin.ToolbarButton
Returns the IWorkbenchWindow associated to this action.
getWorkspace() - Static method in class jack.plugin.JackPlugin
Returns the workspace instance.
getXOffset(StyledText) - Method in class jpov.viewer.source.Box
 
getYOffset(StyledText) - Method in class jpov.viewer.source.Box
 
getZero() - Static method in class jml2b.structure.statement.Expression
Returns the expression 0.
getsFlow(byte) - Method in class jml2b.pog.lemma.VirtualFormula
 
Overview  Package  Class  Use  Tree  Deprecated   Index  Help 
 PREV LETTER   NEXT LETTER FRAMES    NO FRAMES    
A B C D E F G H I J K L M N O P Q R S T U V W Z