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

P

PACKAGE - Static variable in class jml2b.link.LinkInfo

PRINTER_DESCRIPTOR - Static variable in class jpov.Icons

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

PROBLEM_MARKER_TYPE - Static variable in class jack.plugin.Generator

The type of markers that are used by Jack.

PROP - Static variable in class jml2b.formula.BasicType

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

PROVED - Static variable in class jml2b.pog.lemma.ProverStatus

Proof state value that corresponds to a goal that is proved.

PROVED - Static variable in class jpov.Icons

Image corresponding to the proved icon.

PROVED_IMAGES_COUNT - Static variable in class jpov.Icons

The number of image giving the informations concerning the proof rate of a node

PROVER_EXTENSION_ID - Static variable in class jack.plugin.JackPlugin

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

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

Package - class jml2b.structure.java.Package.

class representing packages.

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

Parameters - class jml2b.structure.java.Parameters.

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

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

ParseException - exception jml2b.exceptions.ParseException.

Exception class used to indicate error during the parsing phase.

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

Creates a new ParseException instance.

ParsedItem - class jml2b.structure.java.ParsedItem.

This class provides features to store informations that allow to locate a parsed items.

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

Constructs a default item.

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

Constructs an item from a JML file.

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

Constructs an item from a JML file and an AST node.

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

Constructs an item from another.

PartialJmlFile - class jpov.structure.PartialJmlFile.

This class implements the root node of the tree.

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

Constructs a jml file from loaded informations

PartialJpoFile - class jpov.PartialJpoFile.

This class defines a JPO file.

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

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

PoGenerator - class jack.plugin.compile.PoGenerator.

Class that calls jml2b in order to generate proof obligations.

PoGenerator(Iterator) - Constructor for class jack.plugin.compile.PoGenerator

Create a new PoGenerator allowing to generate proof obligations for the given compilation units.

PoGenerator(ICompilationUnit) - Constructor for class jack.plugin.compile.PoGenerator

PoGeneratorErrorHandler - class jack.plugin.compile.PoGeneratorErrorHandler.

Error handler that adds markers for errors instead of just printing errors to stderr.

PoGeneratorErrorHandler(IProject) - Constructor for class jack.plugin.compile.PoGeneratorErrorHandler

Pog - class jml2b.pog.Pog.

This class provides static methods allowing to run the proof obligations generation.

Pog() - Constructor for class jml2b.pog.Pog

PogException - exception jml2b.exceptions.PogException.

This kind of exception is thrown when a litteral float is found in specification part a loop in pure method called is found in specification part a memory overflow occurs during the WP calculus a class concerning RuntimeException cannot be loaded during the WP calculus.

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

Constructs an exception and add an error into the error handler.

Profiler - class jml2b.util.Profiler.

This class allows to profile the memory usage of JACK.

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

ProofClickListener - class jack.plugin.prove.ProofClickListener.

Listener that displays an error dialog when a double click on a proof task stopped with error occurs.

ProofClickListener() - Constructor for class jack.plugin.prove.ProofClickListener

ProofContentProvider - class jack.plugin.prove.ProofContentProvider.

Content provider for the proof task view.

ProofContentProvider() - Constructor for class jack.plugin.prove.ProofContentProvider

ProofObligation - class jml2b.pog.proofobligation.ProofObligation.

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

ProofObligation() - Constructor for class jml2b.pog.proofobligation.ProofObligation

ProofTask - class jack.plugin.prove.ProofTask.

Class corresponding to a proof task that must be (or is) performed.

ProofTask() - Constructor for class jack.plugin.prove.ProofTask

ProofTask(ICaseExplorer) - Constructor for class jack.plugin.prove.ProofTask

ProofView - class jack.plugin.prove.ProofView.

View that allows controling and showing proof tasks.

ProofView() - Constructor for class jack.plugin.prove.ProofView

Proofs - class jml2b.pog.lemma.Proofs.

This class describes all the proof obligations associated with a method or with the static initialisation.

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

Construct an empty proof.

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

Construct a proof from a lemma

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

Construct a proof from a theorem

Proofs - class jpov.structure.Proofs.

This class implements a node in the tree corresponding to the static initialization.

PropType - Static variable in class jml2b.formula.BasicType

ProveAction - class jack.plugin.prove.ProveAction.

Action allowing adding the selected file to the list of files that should be proved.

ProveAction() - Constructor for class jack.plugin.prove.ProveAction

ProverStatus - class jml2b.pog.lemma.ProverStatus.

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

param(IJml2bConfiguration, Vector, Expression, ExceptionalBehaviourStack) - Method in class jml2b.pog.lemma.Proofs

Renames the formal parameter of a called method by the calling parameters.

parameterDeclaration(Method) - Static method in class jml2b.pog.proofobligation.MethodPO

Returns the formula corresponding to the parameter declaration of the method.

parent - Variable in class jml2b.structure.java.Package

The parent package.

parse(IJml2bConfiguration) - Method in class jml2b.structure.bytecode.ClassDefaultConstructor

parse(IJml2bConfiguration) - Method in class jml2b.structure.bytecode.ClassField

parse(JmlFile, AST) - Method in class jml2b.structure.bytecode.ClassField

parse(IJml2bConfiguration) - Method in class jml2b.structure.bytecode.ClassFile

parse(IJml2bConfiguration) - Method in class jml2b.structure.bytecode.ClassMethod

parse(JmlFile, AST) - Method in class jml2b.structure.bytecode.ClassMethod

parse(JmlFile, AST) - Method in class jml2b.structure.java.Class

Initialise the content of the class from the given AST tree.

parse(JmlFile, AST) - Method in class jml2b.structure.java.Constructor

parse(JmlFile, AST) - Method in class jml2b.structure.java.Declaration

Parses the content of the declaration.

parse(JmlFile, AST) - Method in class jml2b.structure.java.Field

Deprecated. The VarDeclParser class should be used instead of this method.

parse(JmlFile, AST) - Method in class jml2b.structure.java.Invariant

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

Parse the file fills the package and import structures.

parse(JmlFile, AST) - Method in class jml2b.structure.java.Method

parse(AST) - Method in class jml2b.structure.java.Modifiers

Initialise the modifiers from the given AST.

parse(JmlFile, AST) - Method in class jml2b.structure.java.Parameters

parse(AST) - Method in class jml2b.structure.java.Type

create a type from the given AST.

parse(JmlFile, AST) - Method in class jml2b.structure.java.VarDeclParser

parse(JmlFile, AST) - Method in class jml2b.structure.jml.Depends

parse(JmlFile, AST) - Method in class jml2b.structure.jml.Represents

parse(AST) - Method in class jml2b.structure.statement.ArrayInitializer

parse(AST) - Method in class jml2b.structure.statement.BinaryExp

parse(AST) - Method in class jml2b.structure.statement.IsSubtypeOfExp

parse(AST) - Method in class jml2b.structure.statement.MethodCallExp

parse(AST) - Method in class jml2b.structure.statement.QuantifiedExp

parse(AST) - Method in class jml2b.structure.statement.QuestionExp

parse(AST) - Method in class jml2b.structure.statement.StAssert

Parses the assert statement.

parse(AST) - Method in class jml2b.structure.statement.StBlock

parse(AST) - Method in class jml2b.structure.statement.StControlFlowBreak

parse(AST) - Method in class jml2b.structure.statement.StDoWhile

parse(AST) - Method in class jml2b.structure.statement.StFor

parse(AST) - Method in class jml2b.structure.statement.StIf

parse(AST) - Method in class jml2b.structure.statement.StImplementsLabel

parse(AST) - Method in class jml2b.structure.statement.StLabel

parse(AST) - Method in class jml2b.structure.statement.StSequence

parse(AST) - Method in class jml2b.structure.statement.StSkip

parse(AST) - Method in class jml2b.structure.statement.StSpecBlock

parse(AST) - Method in class jml2b.structure.statement.StSwitch

parse(AST) - Method in class jml2b.structure.statement.StTry

parse(AST) - Method in class jml2b.structure.statement.StVarDecl

parse(AST) - Method in class jml2b.structure.statement.Statement

Parses an AST tree in order to instanciate the statement fields.

parse(AST) - Method in class jml2b.structure.statement.TTypeExp

parse(AST) - Method in class jml2b.structure.statement.TerminalExp

parse(AST) - Method in class jml2b.structure.statement.UnaryExp

parse(AST) - Method in class jml2b.structure.statement.WithTypeExp

parseBlockComments(String) - Method in class jack.plugin.edit.JavaLineStyler

parseEnsures(JmlFile, AST, int) - Method in class jml2b.structure.jml.SpecCase

Parses the content of the ensures clause, and returns the new value for first_line.

parseExsures(JmlFile, AST, int) - Method in class jml2b.structure.jml.SpecCase

Parse the content of an exsures clause, returning the new value for first_line.

parseLabel(Vector, AST, JmlFile) - Static method in class jml2b.structure.jml.SpecCase

Parses the label clause of a specification case.

parseLoopExsures(AST) - Method in class jml2b.structure.statement.StLoops

Parses a loop exsures clause.

parseLoopInvariant(AST) - Method in class jml2b.structure.statement.StLoops

Parses a loop invariant clause.

parseLoopVariant(AST) - Method in class jml2b.structure.statement.StLoops

Parses a loop variant clause.

parseModifies(JmlFile, AST, int) - Method in class jml2b.structure.jml.SpecCase

Parses the modifies clause, and returns the updated value of first_line.

parseModifies(JmlFile, AST) - Method in class jml2b.structure.statement.StLoops

Parses a modifies clause.

parseSpecBlock(JmlFile, AST) - Method in class jml2b.structure.jml.SpecCase

Parses the content of a lightweight spec case.

parseVarDecl(JmlFile, AST, Modifiers) - Static method in class jml2b.structure.java.Field

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

Calculated the proof percentage of this node

performDefaults() - Method in class jack.plugin.JackDefaultSpecEditor

Sets all the fields to default values.

performFinish() - Method in class jack.plugin.source.AddJmlClauseWizard

performOk(IProject) - Method in class jack.plugin.JackDefaultSpecEditor

Updates the changes in the interface to the project properties.

performOk() - Method in class jack.plugin.JackProjectPropertyPage

Applies the changes performed in the dialog.

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

pog(JmlFile, IJml2bConfiguration, Vector, Vector, IProgressMonitor) - Method in class jml2b.pog.Pog

Generate the proof obligations associated with a JML file, calculate them and prove them with the obvious prover if requested.

pog(JmlFile[], IJml2bConfiguration) - Method in class jml2b.pog.Pog

Generates the proof obligations for all the JML files, calculate them and prove them with the obvious prover if requested.

pog(IJml2bConfiguration) - Method in class jml2b.pog.proofobligation.ConstructorPO

pog(IJml2bConfiguration) - Method in class jml2b.pog.proofobligation.MethodPO

Process the WP calculus on the proof obligations.

pog(IJml2bConfiguration) - Method in class jml2b.pog.proofobligation.ProofObligation

Process the WP calculus on the proof obligations.

pog(IJml2bConfiguration) - Method in class jml2b.pog.proofobligation.StaticInitializationPO

Process the WP calculus on the proof obligations.

pog(IJml2bConfiguration) - Method in class jml2b.pog.proofobligation.WellDefinedInvPO

pog(IJml2bConfiguration) - Method in class jml2b.pog.proofobligation.WellDefinedSpecPO

pop(int) - Method in class jml2b.pog.lemma.ExceptionalBehaviourStack

Pop elements from the stack

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

Remove the elem�ent at the top of the stack.

predToForm(IJml2bConfiguration) - Method in interface jml2b.structure.jml.JmlExpression

Translates the expression into a formula

predToForm(IJml2bConfiguration) - Method in class jml2b.structure.statement.Expression

Converts the expression, considered as a predicate into a formula

print(IClassResolver, JmlFile, File) - Method in interface jml2b.pog.printers.IPrinter

Writes an output file corresponding to the entry of a prover.

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

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

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

processIdent() - Method in class jml2b.formula.QuantifiedForm

processIdent() - Method in class jml2b.formula.TTypeForm

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

processIdent() - Method in class jml2b.formula.TriaryForm

processIdent() - Method in class jml2b.formula.UnaryForm

processIdent() - Method in class jml2b.structure.jml.Exsures

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

processIdent() - Method in class jml2b.structure.jml.ModifiesClause

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

processIdent() - Method in class jml2b.structure.jml.ModifiesEverything

processIdent() - Method in class jml2b.structure.jml.ModifiesList

processIdent() - Method in class jml2b.structure.jml.ModifiesNothing

processIdent() - Method in class jml2b.structure.statement.ArrayInitializer

processIdent() - Method in class jml2b.structure.statement.BinaryExp

processIdent() - Method in class jml2b.structure.statement.Expression

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

processIdent() - Method in class jml2b.structure.statement.IsSubtypeOfExp

processIdent() - Method in class jml2b.structure.statement.MethodCallExp

processIdent() - Method in class jml2b.structure.statement.QuantifiedExp

processIdent() - Method in class jml2b.structure.statement.QuestionExp

processIdent() - Method in class jml2b.structure.statement.TTypeExp

processIdent() - Method in class jml2b.structure.statement.TerminalExp

When this terminal expression is an identifier, a name index is assigned and its name is stored in the identifier array.

processIdent() - Method in class jml2b.structure.statement.UnaryExp

processIdent() - Method in class jml2b.structure.statement.WithTypeExp

prove(IJml2bConfiguration, JmlFile) - Method in interface jml2b.pog.IObviousProver

Prove and save the status of a jpo file.

proveObvious(Vector, boolean) - Method in class jml2b.pog.lemma.ExsuresLemma

proveObvious(Vector, boolean) - Method in class jml2b.pog.lemma.Goal

A goal is obvious if the formula is obvious, if the formula appears in the hypothesis or if the goal comes from an invariant and it has not been modified during the complete generation.

proveObvious(Vector, boolean) - Method in interface jml2b.pog.lemma.ILemma

Supress in the lemma the obvious goals.

proveObvious(boolean, boolean) - Method in class jml2b.pog.lemma.Proofs

Proves the obvious goals if asked.

proveObvious(Vector, boolean) - Method in class jml2b.pog.lemma.SimpleLemma

proveObvious(boolean) - Method in class jml2b.pog.proofobligation.MethodPO

proveObvious(boolean) - Method in class jml2b.pog.proofobligation.ProofObligation

Proves the obvious goals if asked.

proveObvious(boolean) - Method in class jml2b.pog.proofobligation.StaticInitializationPO

proveObvious(boolean) - Method in class jml2b.pog.proofobligation.WellDefinedInvPO

proveObvious(boolean) - Method in class jml2b.pog.proofobligation.WellDefinedSpecPO

provedImages - Static variable in class jpov.Icons

The array containing the images that give informations concerning the proof rate of a node

purgeObvious() - Method in class jml2b.structure.java.JmlFile

push(ExceptionalProofs) - Method in class jml2b.pog.lemma.ExceptionalBehaviourStack

Push an element on top of the stack

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

Create a new empty set of fields at the top of the stack.