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

S

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

Token correspoding to a sequence of two statements

SERIALIZED_IMAGE_PROPERTY - Static variable in class jack.plugin.JackPlugin

Name of the property corresponding to the image file used.

SHOW_ALL - Static variable in class jpov.viewer.tree.TreeFilterConfiguration

The default configuration Show all.

SHOW_CASES - Static variable in class jpov.viewer.tree.TreeFilterConfiguration

SHOW_UNPROVED - Static variable in class jpov.viewer.tree.TreeFilterConfiguration

The default configuration Show unproved.

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

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

SINGLE_COMMENT_JML_COLOR - Static variable in class jack.plugin.JackPlugin

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

Token correspoding to a skip

SOURCE_CASE_VIEWER_ID - Static variable in class jack.plugin.JackPlugin

The Id corresponding to

SPEC_PUBLIC - Static variable in interface jml2b.structure.java.ModFlags

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

Constant corresponding to the starting state.

STATE_LINKED - Static variable in interface jml2b.link.Linkable

STATE_LINKED_STATEMENTS - Static variable in interface jml2b.link.Linkable

STATE_LINKED_TYPE_CHECKED - Static variable in interface jml2b.link.Linkable

STATE_UNLINKED - Static variable in interface jml2b.link.Linkable

STATIC - Static variable in interface jml2b.structure.java.ModFlags

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

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

Formula origin corresponding to a static final field initialization

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

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

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

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

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

Goal origin value that corresponds to the proof of the requires clause of the super method.

SYNCHRONIZED - Static variable in interface jml2b.structure.java.ModFlags

SaveMessageDialog - class jack.plugin.edit.SaveMessageDialog.

Dialog that indicates that some files need to be saved before an action could occur.

Serializer - class jml2b.Serializer.

Simple application loading the java.lang classes and serializing them using the Java serialisation mechanism.

Serializer() - Constructor for class jml2b.Serializer

ShouldGenerateImageDialog - class jack.plugin.ShouldGenerateImageDialog.

Dialog that indicates that some files need to be saved before an action could occur.

SimpleLemma - class jml2b.pog.lemma.SimpleLemma.

This class implements a simple lemma, that is a set of goals

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

Constructs a lemma with an empty set of goals

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

Constructs a lemma from an expression.

SimpleLemma(Formula, GoalOrigin) - Constructor for class jml2b.pog.lemma.SimpleLemma

Constructs a lemma from a formula.

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

Constructs a lemma from a set of expression.

SimpleLemma(Vector) - Constructor for class jml2b.pog.lemma.SimpleLemma

Constructs a lemma from a loaded one.

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

Constructs a simple lemma containing only non obvious goals from a lemma.

SourceCaseViewer - class jack.plugin.perspective.SourceCaseViewer.

View that displays the source.

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

SourceProofObligation - class jml2b.pog.proofobligation.SourceProofObligation.

This abstract class describes a proof obligation and facilities to calculate them at source level.

SpecArray - class jml2b.structure.jml.SpecArray.

This class defines the possible indexes set of an array in the modifies clause.

SpecArrayDotDot - class jml2b.structure.jml.SpecArrayDotDot.

This class represents an indexes interval

SpecArrayExpr - class jml2b.structure.jml.SpecArrayExpr.

This class represents an index of an array

SpecArrayStar - class jml2b.structure.jml.SpecArrayStar.

This class describes all the indexes of an array that are declared to be potentially modified.

SpecCase - class jml2b.structure.jml.SpecCase.

This class implements a specification case, that is a labelled record of requires, modifies, ensures and exsures.

SpecCase(IJml2bConfiguration, Modifiers) - Constructor for class jml2b.structure.jml.SpecCase

SpecCase(IJml2bConfiguration) - Constructor for class jml2b.structure.jml.SpecCase

Construct an empty spec case.

SpecCase() - Constructor for class jml2b.structure.jml.SpecCase

SpecCase(IJml2bConfiguration, LinkContext) - Constructor for class jml2b.structure.jml.SpecCase

Construct and link an empty by default spec case.

SpecCase(Expression, ModifiesClause) - Constructor for class jml2b.structure.jml.SpecCase

StAssert - class jml2b.structure.statement.StAssert.

StBlock - class jml2b.structure.statement.StBlock.

This class implements a block statement

StControlFlowBreak - class jml2b.structure.statement.StControlFlowBreak.

This class implements a control flow break statement, that is a throw, a continue, a break or a return.

StDoWhile - class jml2b.structure.statement.StDoWhile.

StFor - class jml2b.structure.statement.StFor.

StIf - class jml2b.structure.statement.StIf.

StImplementsLabel - class jml2b.structure.statement.StImplementsLabel.

This class implements an implements label statement.

StLabel - class jml2b.structure.statement.StLabel.

StLoops - class jml2b.structure.statement.StLoops.

This abstract class implements a loop statement.

StSequence - class jml2b.structure.statement.StSequence.

This class implements a sequence of two statements.

StSequence(ParsedItem, Statement, Statement) - Constructor for class jml2b.structure.statement.StSequence

Constructs a sequence from another one.

StSkip - class jml2b.structure.statement.StSkip.

This class implements a skip statement.

StSkip() - Constructor for class jml2b.structure.statement.StSkip

Constructs a skip statement.

StSpecBlock - class jml2b.structure.statement.StSpecBlock.

This class implements a specified block.

StSwitch - class jml2b.structure.statement.StSwitch.

This class implements a switch statement

StTry - class jml2b.structure.statement.StTry.

This class implements a try catch finally statement or a try catch or a try finally statement.

StVarDecl - class jml2b.structure.statement.StVarDecl.

This class implements a set of local field declaration statement

StVarDecl(Vector) - Constructor for class jml2b.structure.statement.StVarDecl

Constructs a statement from a set of fields

Statement - class jml2b.structure.statement.Statement.

This class defines a Java statement.

StatementUtils - class jml2b.util.StatementUtils.

Utility class for handling statement operations

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

StaticInitProofs - class jpov.structure.StaticInitProofs.

StaticInitializationPO - class jml2b.pog.proofobligation.StaticInitializationPO.

This class describes a proof obligation for a static initialization and facilities to calculate them.

StaticInitializationPO(Class, Statement, Theorem, Theorem) - Constructor for class jml2b.pog.proofobligation.StaticInitializationPO

Constructs a proof obligation

StderrHandler - class jml2b.exceptions.StderrHandler.

A simple error handler that displays errors on stderr in the style of gcc: filename:line:message

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

SubArrayElement - class jml2b.pog.substitution.SubArrayElement.

This class corresponds to the substitution of xxxelements with a formula.

SubArrayElement(String, Formula) - Constructor for class jml2b.pog.substitution.SubArrayElement

Constructs a substitution

SubArrayElement - class jpov.substitution.SubArrayElement.

This class corresponds to the substitution of xxxelements with a formula.

SubArrayElement(IJml2bConfiguration, IJmlFile, JpoInputStream) - Constructor for class jpov.substitution.SubArrayElement

Constructs a substitution

SubArrayElementSingle - class jml2b.pog.substitution.SubArrayElementSingle.

This class corresponds to the substitution of xxxelements with a xxxelements <+ {f |-> xxxelements(f) <+ {i |-> v}}.

SubArrayElementSingle(ElementsForm, Formula, Formula, Formula) - Constructor for class jml2b.pog.substitution.SubArrayElementSingle

Constructs a substitution

SubArrayElementSingle - class jpov.substitution.SubArrayElementSingle.

This class corresponds to the substitution of xxxelements with a formula.

SubArrayElementSingle(IJml2bConfiguration, IJmlFile, JpoInputStream) - Constructor for class jpov.substitution.SubArrayElementSingle

Constructs a substitution

SubArrayLength - class jml2b.pog.substitution.SubArrayLength.

This class corresponds to the substitution of arraylength with a formula.

SubArrayLength(Formula) - Constructor for class jml2b.pog.substitution.SubArrayLength

Constructs a substitution

SubArrayLength - class jpov.substitution.SubArrayLength.

This class corresponds to the substitution of arraylength with a formula.

SubArrayLength(IJml2bConfiguration, IJmlFile, JpoInputStream) - Constructor for class jpov.substitution.SubArrayLength

Constructs a substitution

SubForm - class jml2b.pog.substitution.SubForm.

This class corresponds to the substitution of a formula by another.

SubForm(Formula, Formula) - Constructor for class jml2b.pog.substitution.SubForm

Constructs a substitution.

SubForm - class jpov.substitution.SubForm.

This class corresponds to the substitution of a formula by another.

SubForm(IJml2bConfiguration, IJmlFile, JpoInputStream) - Constructor for class jpov.substitution.SubForm

Constructs a substitution.

SubInstances - class jml2b.pog.substitution.SubInstances.

This class corresponds to the substitution of instances with: instances \/ f instances \/ {f}

SubInstancesSet - class jml2b.pog.substitution.SubInstancesSet.

This class corresponds to the substituion of instances with instances \/ f.

SubInstancesSet(Formula) - Constructor for class jml2b.pog.substitution.SubInstancesSet

Constructs a substitution for instances

SubInstancesSet - class jpov.substitution.SubInstancesSet.

This class corresponds to the substituion of instances with: instances \/ f.

SubInstancesSet(IJml2bConfiguration, IJmlFile, JpoInputStream) - Constructor for class jpov.substitution.SubInstancesSet

Constructs a substitution for instances

SubInstancesSingle - class jml2b.pog.substitution.SubInstancesSingle.

This class corresponds to the substituion of instances with instances \/ {f} corresponding to an instance creation.

SubInstancesSingle(Formula) - Constructor for class jml2b.pog.substitution.SubInstancesSingle

Constructs a substitution for instances

SubInstancesSingle - class jpov.substitution.SubInstancesSingle.

This class corresponds to the substituion of instances with instances \/ {f} corresponding to an instance creation.

SubInstancesSingle(IJml2bConfiguration, IJmlFile, JpoInputStream) - Constructor for class jpov.substitution.SubInstancesSingle

Constructs a substitution for instances

SubMemberField - class jml2b.pog.substitution.SubMemberField.

This class implements a substitution of a member field a by a <+ { b |-> c } corresponding to an affectation of a new value for a given instance.

SubMemberField(Formula, String, String, Formula) - Constructor for class jml2b.pog.substitution.SubMemberField

Constructs a substitution

SubMemberField(Formula, Formula, Formula, Formula) - Constructor for class jml2b.pog.substitution.SubMemberField

Constructs a substitution form another one or from a loaded one

SubMemberField - class jpov.substitution.SubMemberField.

This class implements a substitution of a member field a by a <+ { b |-> c } corresponding to an affectation of a new value for a given instance.

SubMemberField(IJml2bConfiguration, IJmlFile, JpoInputStream) - Constructor for class jpov.substitution.SubMemberField

Constructs a substitution

SubStaticOrLocalField - class jml2b.pog.substitution.SubStaticOrLocalField.

SubStaticOrLocalField(Formula, Formula) - Constructor for class jml2b.pog.substitution.SubStaticOrLocalField

SubTmpVar - class jml2b.pog.substitution.SubTmpVar.

This class corresponds to the substitution of a tempory variable with a formula.

SubTmpVar(String, Formula) - Constructor for class jml2b.pog.substitution.SubTmpVar

Constructs a substitution.

SubTmpVar - class jpov.substitution.SubTmpVar.

This class corresponds to the substitution of a tempory variable with a formula.

SubTmpVar(IJml2bConfiguration, IJmlFile, JpoInputStream) - Constructor for class jpov.substitution.SubTmpVar

Constructs a substitution from a loaded .jpo file

SubTypeof - class jml2b.pog.substitution.SubTypeof.

This abstract class describes substitutions applied on typeof

SubTypeof(Formula, Formula) - Constructor for class jml2b.pog.substitution.SubTypeof

Constructs a substitution for typeof

SubTypeofSet - class jml2b.pog.substitution.SubTypeofSet.

This interface describes a substitution of typeof by typeof <+ f * {t}

SubTypeofSet(Formula, Formula) - Constructor for class jml2b.pog.substitution.SubTypeofSet

Constructs a substitution for typeof

SubTypeofSet - class jpov.substitution.SubTypeofSet.

This interface describes a substitution of typeof by typeof <+ f * {t}

SubTypeofSet(IJml2bConfiguration, IJmlFile, JpoInputStream) - Constructor for class jpov.substitution.SubTypeofSet

Constructs a substitution for typeof

SubTypeofSingle - class jml2b.pog.substitution.SubTypeofSingle.

This interface describes a substitution of typeof by typeof <+ {f |-> t}

SubTypeofSingle(Formula, Formula) - Constructor for class jml2b.pog.substitution.SubTypeofSingle

Constructs a substitution for typeof

SubTypeofSingle - class jpov.substitution.SubTypeofSingle.

This interface describes a substitution of typeof by typeof <+ {f |-> t}

SubTypeofSingle(IJml2bConfiguration, IJmlFile, JpoInputStream) - Constructor for class jpov.substitution.SubTypeofSingle

Constructs a substitution for typeof

Substitution - interface jml2b.pog.substitution.Substitution.

This interface describes a substitution.

Substitution - interface jpov.substitution.Substitution.

This interface provides method to save and display substitution applied to goals.

save() - Method in class jack.plugin.perspective.CaseExplorer

save() - Method in interface jack.plugin.perspective.ICaseExplorer

save(IOutputStream) - Method in class jml2b.formula.BasicType

save(IJml2bConfiguration, IOutputStream, IJmlFile) - Method in class jml2b.formula.BinaryForm

save(IJml2bConfiguration, IOutputStream, IJmlFile) - Method in class jml2b.formula.ElementsForm

save(IJml2bConfiguration, IOutputStream, IJmlFile) - Method in class jml2b.formula.Formula

Saves the formula in a .jpo file

save(IJml2bConfiguration, IOutputStream, IJmlFile) - Method in class jml2b.formula.QuantifiedForm

save(IJml2bConfiguration, IOutputStream, IJmlFile) - Method in class jml2b.formula.TTypeForm

save(IJml2bConfiguration, IOutputStream, IJmlFile) - Method in class jml2b.formula.TerminalForm

save(IJml2bConfiguration, IOutputStream, IJmlFile) - Method in class jml2b.formula.TriaryForm

save(IJml2bConfiguration, IOutputStream, IJmlFile) - Method in class jml2b.formula.UnaryForm

save(IOutputStream, TerminalForm) - Method in interface jml2b.languages.ILanguage

Saves a terminal formula in a jpo file.

save(IOutputStream, ITranslationResult) - Method in interface jml2b.languages.ILanguage

Saves the result of a translation in a jpo file.

save(IOutputStream, TerminalForm) - Method in class jml2b.languages.java.JavaLanguage

save(IOutputStream, ITranslationResult) - Method in class jml2b.languages.java.JavaLanguage

save(JpoOutputStream) - Method in class jml2b.pog.lemma.GoalOrigin

Saves the goal origin in a .jpo file

save(JpoOutputStream) - Method in class jml2b.pog.lemma.GoalStatus

Saves the goal status in the a .jpo file

save(IJml2bConfiguration, JpoOutputStream, JmlFile) - Method in class jml2b.pog.lemma.NonObviousGoal

Saves the goal in a .jpo file

save(IJml2bConfiguration, JpoOutputStream, JmlFile) - Method in class jml2b.pog.lemma.Proofs

Saves the proof in the a .jpo file

save(JpoOutputStream) - Method in class jml2b.pog.lemma.ProverStatus

Saves the goal status in the a .jpo file

save(IJml2bConfiguration, JpoOutputStream, JmlFile) - Method in class jml2b.pog.lemma.SimpleLemma

save(IJml2bConfiguration, JpoOutputStream, int, JmlFile) - Method in class jml2b.pog.lemma.VirtualFormula

Saves the virtual formula into a .jpo file

save(IJml2bConfiguration, JpoOutputStream, IJmlFile) - Method in class jml2b.pog.substitution.SubArrayElement

save(IJml2bConfiguration, JpoOutputStream, IJmlFile) - Method in class jml2b.pog.substitution.SubArrayElementSingle

save(IJml2bConfiguration, JpoOutputStream, IJmlFile) - Method in class jml2b.pog.substitution.SubArrayLength

save(IJml2bConfiguration, JpoOutputStream, IJmlFile) - Method in class jml2b.pog.substitution.SubForm

save(IJml2bConfiguration, JpoOutputStream, IJmlFile) - Method in class jml2b.pog.substitution.SubInstances

save(IJml2bConfiguration, JpoOutputStream, IJmlFile) - Method in class jml2b.pog.substitution.SubInstancesSet

save(IJml2bConfiguration, JpoOutputStream, IJmlFile) - Method in class jml2b.pog.substitution.SubInstancesSingle

save(IJml2bConfiguration, JpoOutputStream, IJmlFile) - Method in class jml2b.pog.substitution.SubMemberField

save(IJml2bConfiguration, JpoOutputStream, IJmlFile) - Method in class jml2b.pog.substitution.SubTmpVar

save(IJml2bConfiguration, JpoOutputStream, IJmlFile) - Method in class jml2b.pog.substitution.SubTypeof

save(IJml2bConfiguration, JpoOutputStream, IJmlFile) - Method in class jml2b.pog.substitution.SubTypeofSet

save(IJml2bConfiguration, JpoOutputStream, IJmlFile) - Method in class jml2b.pog.substitution.SubTypeofSingle

save(IJml2bConfiguration, JpoOutputStream, IJmlFile) - Method in interface jml2b.pog.substitution.Substitution

Saves the substitution in a .jpo file

save(JpoOutputStream, int, JmlFile) - Method in class jml2b.pog.util.ColoredInfo

Saves the colored info in a .jpo file if it is declared in a specified JML file

save(IJml2bConfiguration, JpoOutputStream, JmlFile) - Method in class jml2b.structure.java.Class

.jpo file

save(IJml2bConfiguration, JpoOutputStream) - Method in class jml2b.structure.java.JmlFile

.jpo file

save(IJml2bConfiguration, JpoOutputStream, JmlFile) - Method in class jml2b.structure.java.Method

.jpo file

save(JpoOutputStream) - Method in class jml2b.structure.java.ParsedItem

Saves the item in a .jpo file

save(DataOutputStream) - Method in class jml2b.util.JpoOutputStream

save() - Method in class jpov.JpoFile

Saves the file into a .jpo file and save the proof status into a .pmi file.

save(JpoOutputStream) - Method in class jpov.structure.Field

save(IJml2bConfiguration, JpoOutputStream) - Method in class jpov.structure.JmlFile

Saves the JML file into a .jpo file

save(IJml2bConfiguration, JpoOutputStream, IJmlFile) - Method in class jpov.substitution.SubArrayElement

save(IJml2bConfiguration, JpoOutputStream, IJmlFile) - Method in class jpov.substitution.SubArrayElementSingle

save(IJml2bConfiguration, JpoOutputStream, IJmlFile) - Method in class jpov.substitution.SubArrayLength

save(IJml2bConfiguration, JpoOutputStream, IJmlFile) - Method in class jpov.substitution.SubForm

save(IJml2bConfiguration, JpoOutputStream, IJmlFile) - Method in class jpov.substitution.SubInstancesSet

save(IJml2bConfiguration, JpoOutputStream, IJmlFile) - Method in class jpov.substitution.SubInstancesSingle

save(IJml2bConfiguration, JpoOutputStream, IJmlFile) - Method in class jpov.substitution.SubMemberField

save(IJml2bConfiguration, JpoOutputStream, IJmlFile) - Method in class jpov.substitution.SubTmpVar

save(IJml2bConfiguration, JpoOutputStream, IJmlFile) - Method in class jpov.substitution.SubTypeofSet

save(IJml2bConfiguration, JpoOutputStream, IJmlFile) - Method in class jpov.substitution.SubTypeofSingle

save(IJml2bConfiguration, JpoOutputStream, IJmlFile) - Method in interface jpov.substitution.Substitution

Saves the substitution in a .jpo file

save(JpoOutputStream, int) - Method in class jpov.viewer.source.Box

Saves the box to a .jpo file.

saveFileImage(JmlFile[], String) - Static method in class jml2b.Jml2b

Saves an image.

saveFiles(IJml2bConfiguration, JmlFile, IProgressMonitor, Vector, Vector, IClassResolver) - Static method in class jml2b.pog.Pog

saveLeftContent(Object, byte[]) - Method in class jack.plugin.source.JmlMergeViewerContentProvider

saveModifiedRessources(IWorkbenchPart, String, String) - Static method in class jack.plugin.edit.SaveMessageDialog

saveRightContent(Object, byte[]) - Method in class jack.plugin.source.JmlMergeViewerContentProvider

saveThl(IJml2bConfiguration, JpoOutputStream, JmlFile) - Method in class jml2b.pog.lemma.Proofs

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

Search a candidate file for the class name located in the package relative path pkg_path.

searchClass(String) - Method in class jml2b.structure.java.Package

searchLabel(Formula) - Method in class jml2b.pog.lemma.LabeledProofsVector

Search in the list of labeled proofs, the proof with the corresponding label or with a null label if the searched label is null.

seek(long) - Method in class jml2b.util.JpoInputStream

select(Viewer, Object, Object) - Method in class jpov.viewer.tree.TreeFilter

Selects the node tree to display the jml file is always displayed a class is displayed if its proof percent reach the wished rank a method is displayed if its proof percent reach the wished rank a case is displayed if its proof percent reach the wished rank a goal is displayed if its proof status and its origin correspond to displayed ones.

selectAll() - Method in class jpov.structure.Class

selectAll() - Method in class jpov.structure.JmlFile

selectAll() - Method in class jpov.structure.Lemma

selectAll() - Method in class jpov.structure.Method

selectLabel(Vector) - Method in class jml2b.pog.lemma.ExsuresLemma

selectLabel(Vector) - Method in class jml2b.pog.lemma.Lemma

Selects in the labelled lemmas, the cases corresponding to labels.

selectLabel(Vector) - Method in class jml2b.pog.lemma.Proofs

Selects in the lemmas corresponding to behaviours, the cases corresponding to labels.

selectLabel(Vector) - Method in class jml2b.pog.lemma.SimpleLemma

selectionChanged(IAction, ISelection) - Method in class jack.plugin.ToolbarButton

selectionChanged(IAction, ISelection) - Method in class jack.plugin.compile.VerifySourceAction

Update the selection accordingly to the selection changes within the editor.

selectionChanged(IAction, ISelection) - Method in class jack.plugin.edit.EditAction

selectionChanged(IAction, ISelection) - Method in class jack.plugin.metrics.MetricsAction

selectionChanged(IAction, ISelection) - Method in class jack.plugin.prove.ProveAction

selectionChanged(IAction, ISelection) - Method in class jack.plugin.source.AddJmlAction

Update the selection accordingly to the selection changes within the editor.

selectionChanged(SelectionChangedEvent) - Method in class jpov.viewer.tree.TreeItemSelection

If the selected item is a method, a lemma or a goal, sets the origin of the text viewer to the first line of the selected method.

setActivePart(IAction, IWorkbenchPart) - Method in class jack.plugin.compile.VerifySourceAction

setActivePart(IAction, IWorkbenchPart) - Method in class jack.plugin.edit.EditAction

setActivePart(IAction, IWorkbenchPart) - Method in class jack.plugin.metrics.MetricsAction

setActivePart(IAction, IWorkbenchPart) - Method in class jack.plugin.prove.ProveAction

Deprecated.

setActivePart(IAction, IWorkbenchPart) - Method in class jack.plugin.source.AddJmlAction

setApplySubstitution(boolean) - Method in class jpov.viewer.lemma.GoalContentProvider

setAssign(Expression) - Method in class jml2b.structure.java.Field

Sets the Expression object corresponding to the assign clause of the field.

setBox(ParsedItem) - Method in class jml2b.formula.TerminalForm

Sets the box.

setBox(ParsedItem) - Method in class jml2b.structure.java.ParsedItem

Deines an item from another.

setBuiltin(int) - Method in class jml2b.structure.java.Type

Set the current type to represent a builtin type of the type type_tag.

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

Set the current type to represent a builtin type of the typ described by the given string.

setCaseViewer(CaseExplorer) - Method in class jack.plugin.prove.ProveAction

setChecked() - Method in class jml2b.pog.lemma.GoalStatus

Sets the proof state to CHECKED.

setChecked() - Method in class jpov.structure.Class

setChecked() - Method in class jpov.structure.Goal

setChecked() - Method in class jpov.structure.JmlFile

setChecked() - Method in class jpov.structure.Lemma

setChecked() - Method in class jpov.structure.LemmaHierarchy

setChecked() - Method in class jpov.structure.Method

setChecked() - Method in class jpov.structure.Proofs

setChecked() - Method in class jpov.structure.TreeObject

Sets the node and its children to checked.

setClasses(String[]) - Method in class jack.plugin.ImageGenerator

setCurrentClass(AClass) - Method in class jml2b.link.LinkContext

setCurrentClass(Class) - Method in class jpov.viewer.lemma.LemmaFilterWindow

setDefaultExternalFile(boolean) - Method in class jack.plugin.JackJml2bConfiguration

setDefaultJmlEnsuresText(IProject, String) - Static method in class jack.plugin.JackJml2bConfiguration

setDefaultJmlEnsuresTrue(IProject, boolean) - Static method in class jack.plugin.JackJml2bConfiguration

setDefaultJmlExsuresExceptions(IProject, String[]) - Static method in class jack.plugin.JackJml2bConfiguration

setDefaultJmlExsuresOther(IProject, String) - Static method in class jack.plugin.JackJml2bConfiguration

setDefaultJmlExsuresType(IProject, int) - Static method in class jack.plugin.JackJml2bConfiguration

setDefaultJmlModifies(IProject, String) - Static method in class jack.plugin.JackJml2bConfiguration

setDefaultJmlRequiresText(IProject, String) - Static method in class jack.plugin.JackJml2bConfiguration

setDefaultJmlRequiresTrue(IProject, boolean) - Static method in class jack.plugin.JackJml2bConfiguration

setDefiningClass(AClass) - Method in class jml2b.structure.java.Declaration

Sets the class defining the declaration.

setDepends(Vector) - Method in class jml2b.structure.java.JmlFile

Sets the depends.

setEndOp(TreeItemSelection) - Method in class jack.plugin.prove.ProofTask

setEnsures(Expression) - Method in class jml2b.structure.jml.SpecCase

setExceptionType(Type) - Method in class jml2b.pog.lemma.ExsuresLemma

Sets the exceptionType.

setExsure(Vector) - Method in class jml2b.structure.jml.SpecCase

setFileGenerated(String, boolean) - Method in class jack.plugin.JackJml2bConfiguration

setFileGenerated(String, boolean) - Method in interface jml2b.IJml2bConfiguration

setFileGenerated(String, boolean) - Method in class jml2b.Jml2bConfig

setFlag(int) - Method in class jml2b.structure.java.Modifiers

Sets the given flag(s).

setFocus() - Method in class jack.plugin.metrics.MetricsView

setFocus() - Method in class jack.plugin.perspective.CaseExplorer

setFocus() - Method in class jack.plugin.perspective.LemmaViewer

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

setFocus() - Method in class jack.plugin.prove.ProofView

setGoalMenu() - Method in class jack.plugin.perspective.CaseExplorer

setGoalMenu() - Method in interface jack.plugin.perspective.ICaseExplorer

setGoalText(Goal) - Method in interface jack.plugin.perspective.ILemmaViewer

Set the goal to display in the goal part of the view

setGoalText(Goal) - Method in class jack.plugin.perspective.LemmaViewer

Sets the goal to be displayed in the lemma views

setGoalText(Goal, boolean) - Method in class jpov.viewer.lemma.LemmaView

Sets the text to be displayed in the goal views

setHandler(ErrorHandler) - Static method in class jml2b.exceptions.ErrorHandler

Set the error handler that should be used.

setHypText(Lemma) - Method in interface jack.plugin.perspective.ILemmaViewer

Sets the hypotheses to be displayed in the lemma views

setHypText(LemmaHierarchy) - Method in interface jack.plugin.perspective.ILemmaViewer

Sets the hypotheses to be displayed in the lemma views

setHypText(Lemma) - Method in class jack.plugin.perspective.LemmaViewer

Sets the lemma to be displayed in the lemma views

setHypText(LemmaHierarchy) - Method in class jack.plugin.perspective.LemmaViewer

setHypText(Lemma) - Method in class jpov.viewer.lemma.LemmaView

Sets the text to be displayed in the hypothesis views

setHypText(LemmaHierarchy) - Method in class jpov.viewer.lemma.LemmaView

setJPov(JpoFile) - Method in class jack.plugin.prove.ProofTask

setJmlPath(IProject, String[]) - Static method in class jack.plugin.JackPlugin

Sets the jml search path for the given project.

setKeepPackage(boolean) - Method in class jml2b.structure.java.Package

setLemmaMenu() - Method in class jack.plugin.perspective.CaseExplorer

setLemmaMenu() - Method in interface jack.plugin.perspective.ICaseExplorer

setMethods(Object[]) - Method in class jack.plugin.source.JmlClauseGenerator

setModifiers(Modifiers) - Method in class jml2b.structure.jml.SpecCase

Sets the modifiers for the current SpecCase object.

setModifies(ModifiesClause) - Method in class jml2b.structure.jml.SpecCase

setMultipleGoalMenu() - Method in class jack.plugin.perspective.CaseExplorer

setMultipleGoalMenu() - Method in interface jack.plugin.perspective.ICaseExplorer

setNodeText(String) - Method in class jml2b.structure.statement.Expression

Sets the nodeText.

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

Sets the nodeType.

setNumber(int) - Method in class jml2b.pog.lemma.NonObviousGoal

Sets the goal number

setObvious(boolean) - Method in class jml2b.pog.lemma.Goal

setOrigin(byte) - Method in class jml2b.pog.lemma.VirtualFormula

Sets the origin.

setParsedItem(ParsedItem) - Method in class jml2b.structure.java.Field

setParsedItem(ParsedItem) - Method in class jml2b.structure.java.Type

setParsedItem(ParsedItem) - Method in class jml2b.structure.jml.Exsures

setParsedItem(ParsedItem) - Method in class jml2b.structure.jml.GuardedModifies

setParsedItem(ParsedItem) - Method in class jml2b.structure.jml.ModifiesClause

setParsedItem(ParsedItem) - Method in class jml2b.structure.jml.ModifiesEverything

setParsedItem(ParsedItem) - Method in class jml2b.structure.jml.ModifiesList

setParsedItem(ParsedItem) - Method in class jml2b.structure.jml.ModifiesNothing

setParsedItem(ParsedItem) - Method in class jml2b.structure.jml.SpecCase

setParsedItem(ParsedItem) - Method in class jml2b.structure.statement.ArrayInitializer

setParsedItem(ParsedItem) - Method in class jml2b.structure.statement.BinaryExp

setParsedItem(ParsedItem) - Method in class jml2b.structure.statement.Expression

setParsedItem(ParsedItem) - Method in class jml2b.structure.statement.IsSubtypeOfExp

setParsedItem(ParsedItem) - Method in class jml2b.structure.statement.MethodCallExp

setParsedItem(ParsedItem) - Method in class jml2b.structure.statement.QuantifiedExp

setParsedItem(ParsedItem) - Method in class jml2b.structure.statement.QuantifiedVar

setParsedItem(ParsedItem) - Method in class jml2b.structure.statement.QuestionExp

setParsedItem(ParsedItem) - Method in class jml2b.structure.statement.TTypeExp

setParsedItem(ParsedItem) - Method in class jml2b.structure.statement.TerminalExp

setParsedItem(ParsedItem) - Method in class jml2b.structure.statement.UnaryExp

setParsedItem(ParsedItem) - Method in class jml2b.structure.statement.WithTypeExp

setPartial(String) - Method in class jack.plugin.prove.ProofTask

This method is called when the partial mode is called.

setPath(String[]) - Method in class jack.plugin.JackPathEditor

Set the path list to the given one.

setPmiName(String) - Method in class jml2b.structure.java.Method

setProved(int) - Method in class jml2b.pog.lemma.GoalStatus

Sets the proof state to PROVED.

setRange(String) - Method in class jack.plugin.edit.JavaScanner

setRequires(Expression) - Method in class jml2b.structure.java.Method

setRequires(Expression) - Method in class jml2b.structure.jml.SpecCase

setResultAdmitted(boolean) - Method in class jml2b.link.LinkContext

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

setScanner(JavaScanner) - Method in class jack.plugin.edit.JavaLineStyler

setSelected() - Method in class jpov.structure.Goal

setSerializedImageRoots(IProject, String[]) - Static method in class jack.plugin.JackPlugin

Sets the list of additional roots used for generating the serialized image.

setShortName() - Method in class jml2b.pog.util.IdentifierResolver

Indicates that the short name can be used.

setShouldGenerateImage(boolean) - Method in class jack.plugin.JackProjectPropertyPage

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

setStateType(Type) - Method in class jml2b.structure.statement.Expression

Sets the state type value.

setStatus(String, ProverStatus) - Method in class jml2b.pog.lemma.GoalStatus

setStatus(String, ProverStatus) - Method in class jpov.structure.Goal

Sets the goal status

setText(String) - Method in class jpov.structure.Lemma

setTopIndex(int) - Method in interface jack.plugin.perspective.ISourceCaseViewer

setTopIndex(int) - Method in class jack.plugin.perspective.SourceCaseViewer

setUnchecked() - Method in class jpov.structure.Class

setUnchecked() - Method in class jpov.structure.Goal

setUnchecked() - Method in class jpov.structure.JmlFile

setUnchecked() - Method in class jpov.structure.Lemma

setUnchecked() - Method in class jpov.structure.LemmaHierarchy

setUnchecked() - Method in class jpov.structure.Method

setUnchecked() - Method in class jpov.structure.Proofs

setUnchecked() - Method in class jpov.structure.TreeObject

Sets the node and its children to unchecked

setUnproved() - Method in class jml2b.pog.lemma.GoalStatus

Sets the proof state to UNPROVED.

setUnproved() - Method in class jml2b.pog.lemma.ProverStatus

Sets the proof state to UNPROVED.

setUnselected() - Method in class jpov.structure.Goal

setViewedFile(ICompilationUnit, SourceCaseViewer) - Method in class jack.plugin.perspective.CaseExplorer

Sets the currently viewed file.

setViewedFile(IFile, SourceCaseViewer) - Method in class jack.plugin.perspective.CaseExplorer

shortNameEquals(IdentifierResolver) - Method in class jml2b.pog.util.IdentifierResolver

Test whether the short name equals the parameter.

shortelements - Static variable in class jml2b.formula.ElementsForm

The formula shortelements_n.

shouldGenerateImage(Shell, JackProjectPropertyPage) - Static method in class jack.plugin.ShouldGenerateImageDialog

showAncestor(Object) - Method in class jack.plugin.source.JmlMergeViewerContentProvider

signature - Variable in class jml2b.structure.java.Parameters

vector containing fields corresponding to the signature

signatureToString(Enumeration) - Static method in class jml2b.structure.java.Type

Converts a signature to a string suitable for printing.

size() - Method in class jml2b.pog.lemma.ExceptionalBehaviourStack

Returns the size of the stack

size() - Method in class jml2b.util.JpoOutputStream

start() - Method in class jack.plugin.prove.ProofTask

staticFinalFieldInvariants - Variable in class jml2b.structure.java.Class

Static final fields declaration of the class.

staticInitLemmas - Variable in class jml2b.structure.java.Class

staticInvariants - Variable in class jml2b.structure.java.Class

Static invariants of the class.

stopAsSoonAsYouCanPlease() - Method in class jack.plugin.prove.ProofTask

Function that asks the thread to stop when he can.

storeData(Object, Object) - Method in class jml2b.structure.java.JmlFile

Store the data using key so that the information can be retrieved using getUserData.

sub(Formula, Formula, boolean) - Method in class jml2b.formula.BinaryForm

sub(Formula, Formula, boolean) - Method in class jml2b.formula.Formula

Applies a substitution on a formula.

sub(Field, Field, boolean) - Method in class jml2b.formula.Formula

Applies a substitution on a formula.

sub(Formula, Formula, boolean) - Method in class jml2b.formula.QuantifiedForm

sub(Formula, Formula, boolean) - Method in class jml2b.formula.TTypeForm

sub(Formula, Formula, boolean) - Method in class jml2b.formula.TerminalForm

sub(Formula, Formula, boolean) - Method in class jml2b.formula.TriaryForm

sub(Formula, Formula, boolean) - Method in class jml2b.formula.UnaryForm

sub(Substitution) - Method in class jml2b.pog.lemma.ExsuresLemma

sub(Substitution) - Method in class jml2b.pog.lemma.Goal

sub(Substitution) - Method in interface jml2b.pog.lemma.ILemma

Apply a substitution to the lemma.

sub(Substitution) - Method in class jml2b.pog.lemma.Proofs

Apply a substitution to the content of the proof.

sub(Substitution) - Method in class jml2b.pog.lemma.SimpleLemma

sub(Substitution) - Method in class jml2b.pog.lemma.TheoremList

Apply a substitution to the theorem list.

sub(Formula) - Method in class jml2b.pog.substitution.SubArrayElement

sub(Substitution) - Method in class jml2b.pog.substitution.SubArrayElement

sub(Formula) - Method in class jml2b.pog.substitution.SubArrayElementSingle

sub(Substitution) - Method in class jml2b.pog.substitution.SubArrayElementSingle

sub(Formula) - Method in class jml2b.pog.substitution.SubArrayLength

sub(Substitution) - Method in class jml2b.pog.substitution.SubArrayLength

sub(Formula) - Method in class jml2b.pog.substitution.SubForm

sub(Substitution) - Method in class jml2b.pog.substitution.SubForm

sub(Substitution) - Method in class jml2b.pog.substitution.SubInstances

sub(Formula) - Method in class jml2b.pog.substitution.SubInstancesSet

Substitutes instances with instances \/ f

sub(Formula) - Method in class jml2b.pog.substitution.SubInstancesSingle

Substitute instances with instances \/ {f} into a given formula.

sub(Formula) - Method in class jml2b.pog.substitution.SubMemberField

sub(Substitution) - Method in class jml2b.pog.substitution.SubMemberField

sub(Formula) - Method in class jml2b.pog.substitution.SubTmpVar

sub(Substitution) - Method in class jml2b.pog.substitution.SubTmpVar

sub(Substitution) - Method in class jml2b.pog.substitution.SubTypeof

sub(Formula) - Method in class jml2b.pog.substitution.SubTypeofSet

Substitutes typeof with typeof <+ f * {t} in p.

sub(Formula) - Method in class jml2b.pog.substitution.SubTypeofSingle

Substitues typeof by typeof <+ {f |-> t} in p.

sub(Formula) - Method in interface jml2b.pog.substitution.Substitution

Apply the current substitution on a formula.

sub(Substitution) - Method in interface jml2b.pog.substitution.Substitution

Apply a substitution on the current substitution.

subField(Field, Field) - Method in class jml2b.structure.statement.ArrayInitializer

subField(Field, Field) - Method in class jml2b.structure.statement.BinaryExp

subField(Field, Field) - Method in class jml2b.structure.statement.Expression

subField(Field, Field) - Method in class jml2b.structure.statement.IsSubtypeOfExp

subField(Field, Field) - Method in class jml2b.structure.statement.MethodCallExp

subField(Field, Field) - Method in class jml2b.structure.statement.QuantifiedExp

subField(Field, Field) - Method in class jml2b.structure.statement.QuestionExp

subField(Field, Field) - Method in class jml2b.structure.statement.TTypeExp

subField(Field, Field) - Method in class jml2b.structure.statement.TerminalExp

subField(Field, Field) - Method in class jml2b.structure.statement.UnaryExp

subField(Field, Field) - Method in class jml2b.structure.statement.WithTypeExp

subIdent(String, Formula) - Method in class jml2b.formula.BinaryForm

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

Applies a substitution on a formula.

subIdent(String, Formula) - Method in class jml2b.formula.QuantifiedForm

subIdent(String, Formula) - Method in class jml2b.formula.TTypeForm

subIdent(String, Formula) - Method in class jml2b.formula.TerminalForm

subIdent(String, Formula) - Method in class jml2b.formula.TriaryForm

subIdent(String, Formula) - Method in class jml2b.formula.UnaryForm

subResult(String) - Method in class jml2b.structure.statement.ArrayInitializer

subResult(String) - Method in class jml2b.structure.statement.BinaryExp

subResult(String) - Method in class jml2b.structure.statement.Expression

subResult(String) - Method in class jml2b.structure.statement.IsSubtypeOfExp

subResult(String) - Method in class jml2b.structure.statement.MethodCallExp

subResult(String) - Method in class jml2b.structure.statement.QuantifiedExp

subResult(String) - Method in class jml2b.structure.statement.QuestionExp

subResult(String) - Method in class jml2b.structure.statement.TTypeExp

subResult(String) - Method in class jml2b.structure.statement.TerminalExp

subResult(String) - Method in class jml2b.structure.statement.UnaryExp

subResult(String) - Method in class jml2b.structure.statement.WithTypeExp

suppressSpecialOld(int) - Method in class jml2b.formula.BinaryForm

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

Suppress the called old pragmas.

suppressSpecialOld(int) - Method in class jml2b.formula.QuantifiedForm

suppressSpecialOld(int) - Method in class jml2b.formula.TTypeForm

suppressSpecialOld(int) - Method in class jml2b.formula.TerminalForm

suppressSpecialOld(int) - Method in class jml2b.formula.TriaryForm

suppressSpecialOld(int) - Method in class jml2b.formula.UnaryForm

suppressSpecialOld(int) - Method in class jml2b.pog.lemma.ExsuresLemma

suppressSpecialOld(int) - Method in class jml2b.pog.lemma.Goal

suppressSpecialOld(int) - Method in interface jml2b.pog.lemma.ILemma

Suppress the Called Old expressions.

suppressSpecialOld(int) - Method in class jml2b.pog.lemma.Proofs

Suppress the Called Old expressions in the proof.

suppressSpecialOld(int) - Method in class jml2b.pog.lemma.SimpleLemma