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

F

FILTER_DESCRIPTOR - Static variable in class jpov.Icons

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

FINAL_IDENT - Static variable in interface jml2b.formula.IFormToken

Constant identifier with priority 250.

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

Constant corresponding to the state.

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

The first token indice

FLAT - Static variable in interface jack.plugin.perspective.ICaseExplorer

Layout corresponding to a flat presentation of the cases.

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

Substitution type corresponding to the substitution of a formula by a

FUNC - Static variable in class jml2b.formula.BasicType

Factory(String) - Method in interface jml2b.languages.ITranslationResult

Constructs a translation result from a string.

Factory(String) - Method in class jml2b.languages.java.JavaTranslationResult

Field - class jml2b.structure.java.Field.

Class representing fields.

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

Field(ParsedItem, Modifiers, Type, String, Expression) - Constructor for class jml2b.structure.java.Field

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

Field - class jpov.structure.Field.

Field(JpoInputStream) - Constructor for class jpov.structure.Field

FileUpdate - class jml2b.util.FileUpdate.

FileUpdate(File, String) - Constructor for class jml2b.util.FileUpdate

FileUpdateComparator - class jml2b.util.FileUpdateComparator.

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

Formula - class jml2b.formula.Formula.

This class describes a formula.

factory(IFile, ICompilationUnit) - Method in class jack.plugin.prove.ProofTask

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

factory() - Method in interface jml2b.pog.IProverStatus

factory(JpoInputStream) - Method in interface jml2b.pog.IProverStatus

factory(String[]) - Static method in class jml2b.util.JmlPathEntry

factory(ICaseExplorer) - Method in interface jpov.IInteractiveProver

field - Variable in class jml2b.structure.java.Identifier

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

Fields defined by the class.

fileName - Variable in class jml2b.structure.java.JmlFile

FileName of the corresponding file (if any)

fileSearchMisses - Static variable in class jml2b.structure.java.JmlLoader

Number of times a file is searched and not found.

finalize(IJml2bConfiguration, Formula, Expression, Formula, Formula, String, ColoredInfo, ColoredInfo) - Method in class jml2b.pog.lemma.Proofs

Finalize the proof obligations by adding the parameters typing in hypothesis adding the invariant coming from the final static field initialization in hypothesis adding the invariant in hypothesis adding the requires of the current method in hypothesis assigning a name

finalizeLoad() - Method in class jpov.JpoFile

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

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

finallyLab(IJml2bConfiguration, Statement, Proofs, LabeledProofsVector, LabeledProofsVector, ExceptionalBehaviourStack) - Method in class jml2b.pog.lemma.LabeledProofsVector

Applies a WP calculus on all the labeled proofs of the set.

finallyOnExceptionalBehaviour(IJml2bConfiguration, Statement, Proofs, LabeledProofsVector, LabeledProofsVector, ExceptionalBehaviourStack) - Method in class jml2b.pog.lemma.ExceptionalBehaviourStack

Calculate the ExceptionalProofs stack resulting from the application of the body on the current stack (used to proceed a finally).

finallyOnExceptionalBehaviour(IJml2bConfiguration, Statement, Proofs, LabeledProofsVector, LabeledProofsVector, ExceptionalBehaviourStack) - Method in class jml2b.pog.lemma.ExceptionalProofs

Calculate the ExceptionalProofs stack resulting from the application of the body on the current stack (used to proceed a finally).

findUsedLocHyp() - Method in class jml2b.pog.lemma.Proofs

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

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

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

Returns the first statement in a sequence.

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

formulaFactory(Formula) - Method in interface jml2b.languages.ILanguage

Returns a formula corresponding to the initial but converted in a translatable subclass of formula.

formulaFactory(Formula) - Method in class jml2b.languages.java.JavaLanguage

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

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

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

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

fresh() - Static method in class jml2b.structure.statement.Statement

Returns a fresh temporary variable.

freshObject() - Static method in class jml2b.structure.statement.Statement

Returns a fresh new object variable.

freshResult(String) - Static method in class jml2b.structure.statement.Statement

Returns a fresh returned from method call variable.