Uses of Class
jml2b.formula.Formula

Packages that use Formula

jml2b.formula	Provides the classes necessary to create and manage formulas.
jml2b.languages
jml2b.languages.java
jml2b.pog	Provides the classes necessary to generate proof obligations.
jml2b.pog.lemma
jml2b.pog.proofobligation
jml2b.pog.substitution	Provides the classes necessary to create and manage substitutions.
jml2b.pog.util
jml2b.structure.java
jml2b.structure.jml	Provides the classes necessary to create and manage jml clauses such that depends, represents, specification cases, modifies and exsures.
jml2b.structure.statement	Provides the classes necessary to create and manage java and jml statements and expressions.
jpov.structure
jpov.viewer.lemma

Uses of Formula in jml2b.formula

Subclasses of Formula in jml2b.formula

class	BinaryForm This class implements binary formula.
class	ElementsForm This class implements terminal formulas that correspond to variables xxxelements_n, where xxx can be int, short, byte, boolean, char ou ref and n is a natural number.
class	ModifiedFieldForm
class	QuantifiedForm This class implements quantified formula: universal, existential or union.
class	TerminalForm This class implements terminal formula: identifiers, literal constants and builtin types.
class	TriaryForm This class implements tri-ary formula, that is conditional formula coming from the Java structure a ? b : c or equals with restricted domains formulas.
class	TTypeForm This class implements type formula.
class	UnaryForm This class implements unary Formula.

Methods in jml2b.formula that return Formula

Formula	BinaryForm.instancie(Formula b)
Formula	BinaryForm.sub(Formula a, Formula b, boolean subInCalledOld)
Formula	BinaryForm.suppressSpecialOld(int token)
Formula	BinaryForm.subIdent(java.lang.String a, Formula b)
Formula	BinaryForm.renameParam(Parameters signature, java.util.Vector newSignature)
Formula	BinaryForm.getLeft() Returns the left formula.
Formula	BinaryForm.getRight() Returns the right formula.
Formula	ElementsForm.getType() Returns the B type of the formula.
static Formula	Formula.getNull() Returns the formula null.
static Formula	Formula.getFalse() Returns the formula false.
static Formula	Formula.declarField(Field f) Returns the formula corresponding to a field declaration.
static Formula	Formula.create(IJml2bConfiguration config, JpoInputStream s, IJmlFile fi) Create a formula from a token read into a stream.
abstract Formula	Formula.instancie(Formula b) Replaces this with the parameter in the expression.
abstract Formula	Formula.sub(Formula a, Formula b, boolean subInCalledOld) Applies a substitution on a formula.
abstract Formula	Formula.suppressSpecialOld(int token) Suppress the called old pragmas.
abstract Formula	Formula.subIdent(java.lang.String a, Formula b) Applies a substitution on a formula.
Formula	Formula.oldParam(java.util.Vector signature) Encapsulates given parameters into an old pragma.
Formula	Formula.sub(Field a, Field b, boolean subInCalledOld) Applies a substitution on a formula.
Formula	Formula.renameParam(IAParameters signature, java.util.Vector newSignature) Renames the fields belonging to the parameter list with new names.
Formula	Formula.domainRestrict(java.util.Vector df) Applies successive domain restriction to the formula
Formula	QuantifiedForm.instancie(Formula b)
Formula	QuantifiedForm.sub(Formula a, Formula b, boolean subInCalledOld)
Formula	QuantifiedForm.suppressSpecialOld(int token)
Formula	QuantifiedForm.subIdent(java.lang.String a, Formula b)
Formula	QuantifiedVarForm.getType()
Formula	TTypeForm.instancie(Formula b)
Formula	TTypeForm.sub(Formula a, Formula b, boolean subInCalledOld)
Formula	TTypeForm.subIdent(java.lang.String a, Formula b)
Formula	TTypeForm.suppressSpecialOld(int token)
Formula	TerminalForm.instancie(Formula b)
Formula	TerminalForm.sub(Formula a, Formula b, boolean subInCalledOld)
Formula	TerminalForm.subIdent(java.lang.String a, Formula b)
Formula	TerminalForm.suppressSpecialOld(int token)
Formula	TriaryForm.instancie(Formula b)
Formula	TriaryForm.sub(Formula a, Formula b, boolean subInCalledOld)
Formula	TriaryForm.suppressSpecialOld(int token)
Formula	TriaryForm.subIdent(java.lang.String a, Formula b)
Formula	TriaryForm.getF1() Returns the f1.
Formula	TriaryForm.getLeft() Returns the left.
Formula	TriaryForm.getRight() Returns the right.
Formula	UnaryForm.sub(Formula a, Formula b, boolean subInCalledOld)
Formula	UnaryForm.suppressSpecialOld(int token)
Formula	UnaryForm.instancie(Formula b)
Formula	UnaryForm.subIdent(java.lang.String a, Formula b)
Formula	UnaryForm.getExp() Returns the leaf formula.

Methods in jml2b.formula with parameters of type Formula

static BinaryForm	BinaryForm.getDefaultRefDecl(Formula x)
Formula	BinaryForm.instancie(Formula b)
Formula	BinaryForm.sub(Formula a, Formula b, boolean subInCalledOld)
Formula	BinaryForm.subIdent(java.lang.String a, Formula b)
boolean	BinaryForm.is(Formula f)
static BinaryForm	Formula.or(Formula s1, Formula s2) Returns the disjunctive formula between the two parameters.
static BinaryForm	Formula.and(Formula s1, Formula s2) Returns the conjunctive formula between the two parameters.
static UnaryForm	Formula.not(Formula s1) Returns the negation of the parameter.
static BinaryForm	Formula.implies(Formula s1, Formula s2) Returns the implicative formula between the two parameters.
abstract Formula	Formula.instancie(Formula b) Replaces this with the parameter in the expression.
abstract Formula	Formula.sub(Formula a, Formula b, boolean subInCalledOld) Applies a substitution on a formula.
abstract Formula	Formula.subIdent(java.lang.String a, Formula b) Applies a substitution on a formula.
abstract boolean	Formula.is(Formula f) Returns whether the formula corresponds to a read formula.
Formula	QuantifiedForm.instancie(Formula b)
Formula	QuantifiedForm.sub(Formula a, Formula b, boolean subInCalledOld)
Formula	QuantifiedForm.subIdent(java.lang.String a, Formula b)
boolean	QuantifiedForm.is(Formula f)
Formula	TTypeForm.instancie(Formula b)
Formula	TTypeForm.sub(Formula a, Formula b, boolean subInCalledOld)
Formula	TTypeForm.subIdent(java.lang.String a, Formula b)
boolean	TTypeForm.is(Formula f)
Formula	TerminalForm.instancie(Formula b)
Formula	TerminalForm.sub(Formula a, Formula b, boolean subInCalledOld)
Formula	TerminalForm.subIdent(java.lang.String a, Formula b)
boolean	TerminalForm.is(Formula f)
Formula	TriaryForm.instancie(Formula b)
Formula	TriaryForm.sub(Formula a, Formula b, boolean subInCalledOld)
Formula	TriaryForm.subIdent(java.lang.String a, Formula b)
boolean	TriaryForm.is(Formula f)
Formula	UnaryForm.sub(Formula a, Formula b, boolean subInCalledOld)
Formula	UnaryForm.instancie(Formula b)
Formula	UnaryForm.subIdent(java.lang.String a, Formula b)
boolean	UnaryForm.is(Formula f)

Constructors in jml2b.formula with parameters of type Formula

BinaryForm(byte nodeType, Formula left, Formula right)
Constructs a binary formula from two formulas and a token.

QuantifiedForm(byte nodeType, QuantifiedVarForm vars, Formula body)
Constructs a quantified formula from a set of variables and a formula.

QuantifiedVarForm(TerminalForm var, Formula type)
Creates a list with one quantified variable.

QuantifiedVarForm(TerminalForm var, Formula type, QuantifiedVarForm next)
Creates a quantified variable list from another one.

TriaryForm(byte nodeType, Formula cond, Formula left, Formula right)
Constructs a question formula from three formulas.

UnaryForm(byte nodeType, Formula exp)
Constructs a unary formula from a formula and a token.

Uses of Formula in jml2b.languages

Methods in jml2b.languages with parameters of type Formula

ITranslatable

ILanguage.formulaFactory(Formula f) Returns a formula corresponding to the initial but converted in a translatable subclass of formula.

Uses of Formula in jml2b.languages.java

Subclasses of Formula in jml2b.languages.java

class	JavaBinaryForm
class	JavaModifiedFieldForm
class	JavaQuantifiedForm
class	JavaTerminalForm
class	JavaTriaryForm
class	JavaTTypeForm
class	JavaUnaryForm

Methods in jml2b.languages.java with parameters of type Formula

ITranslatable

JavaLanguage.formulaFactory(Formula f)

Uses of Formula in jml2b.pog

Methods in jml2b.pog that return Formula

static Formula

Pog.quantify(IJml2bConfiguration config, AClass c, java.util.Vector i) Quantifies the member invariant of a class for all instances of this class.

Uses of Formula in jml2b.pog.lemma

Methods in jml2b.pog.lemma that return Formula

Formula	Goal.getFormula() Returns the goal
Formula	SimpleLemma.getFormula()
Formula	VirtualFormula.getFormula() Returns the formula

Methods in jml2b.pog.lemma with parameters of type Formula

Proofs	ExceptionalBehaviourStack.throwException(Formula vv, Formula c) Returns the proof to prove to ensure that the thrown of an exception ensures the current proof.
Lemma	ExceptionalLemma.throwException(Formula vv, Formula c)
Lemma	ExsuresLemma.throwException(Formula vv, Formula c)
void	Goal.addImplicToGoal(Formula f, byte origin) Transforms the goal into an implication formula
Proofs	LabeledProofsVector.searchLabel(Formula lab) Search in the list of labeled proofs, the proof with the corresponding label or with a null label if the searched label is null.
void	LabeledProofsVector.add(Formula label, Proofs l) Add a new labeled proof at the beggining of the list.
Lemma	Lemma.throwException(Formula vv, Formula c) Returns the lemma to prove to ensure that the thrown of an exception ensures the current lemma.
void	Proofs.finalize(IJml2bConfiguration config, Formula param, Expression invStaticFinalFields, Formula hyp, Formula req, java.lang.String name, ColoredInfo b, ColoredInfo method) 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
Proofs	Proofs.quantify(java.lang.String var, Formula type) Quantifies the proof whith a variable.
Proofs	Proofs.quantify(java.lang.String var, Formula type, ColoredInfo b) Quantifies the proof whith a variable.
Proofs	Proofs.quantify(Formula var, Formula type)
Proofs	Proofs.quantify(Formula var, Formula type, ColoredInfo b) Quantifies the proof whith a variable.
void	Proofs.addHyp(Formula f, ColoredInfo b, byte origin) Adds new hypothesis.
void	Proofs.addHyp(Formula f, java.util.Vector b, byte origin) Adds new hypothesis.
void	Proofs.addHyp(Formula f) Adds new local hypothesis with no associated colored info.
void	SimpleLemma.addImplicToGoal(Formula f, byte origin) Transforms each goal into an implication formula

Constructors in jml2b.pog.lemma with parameters of type Formula

Goal(Formula f, GoalOrigin origin)
Constructs a goal from a formula and an origin.

SimpleLemma(Formula f, GoalOrigin origin)
Constructs a lemma from a formula.

VirtualFormula(byte origin, Formula f, ColoredInfo b)
Constructs a virtual formula

VirtualFormula(byte origin, Formula f, java.util.Vector b)
Constructs a virtual formula

Uses of Formula in jml2b.pog.proofobligation

Methods in jml2b.pog.proofobligation that return Formula

static Formula

MethodPO.parameterDeclaration(Method method) Returns the formula corresponding to the parameter declaration of the method.

Constructors in jml2b.pog.proofobligation with parameters of type Formula

ConstructorPO(Class c, java.lang.String s, Method m, Formula h1, Formula h2, ColoredInfo box, Statement b, Theorem p1, Theorem p7)
Constructs a proof obligation

MethodPO(Class c, Method m, Formula h1, Formula h2, ColoredInfo box, Statement b, Theorem p1, Theorem p7)
Constructs a proof obligation

Uses of Formula in jml2b.pog.substitution

Methods in jml2b.pog.substitution that return Formula

Formula	SubArrayElement.sub(Formula f)
Formula	SubArrayElementSingle.sub(Formula f)
Formula	SubArrayLength.sub(Formula p)
Formula	SubForm.sub(Formula f)
Formula	SubInstancesSet.sub(Formula p) Substitutes instances with instances \/ f
Formula	SubInstancesSingle.sub(Formula p) Substitute instances with instances \/ {f} into a given formula.
Formula	SubMemberField.sub(Formula f)
Formula	SubMemberField.getField()
Formula	SubMemberField.getInstance()
Formula	SubStaticOrLocalField.getField()
Formula	SubTmpVar.sub(Formula p)
Formula	SubTypeof.getF() Returns the formula corresponding to the extended typeof domain.
Formula	SubTypeof.getT() Returns the formula corresponding to the value asociated to new domain.
Formula	SubTypeofSet.sub(Formula p) Substitutes typeof with typeof <+ f * {t} in p.
Formula	SubTypeofSingle.sub(Formula p) Substitues typeof by typeof <+ {f |-> t} in p.
Formula	Substitution.sub(Formula f) Apply the current substitution on a formula.

Methods in jml2b.pog.substitution with parameters of type Formula

Formula	SubArrayElement.sub(Formula f)
Formula	SubArrayElementSingle.sub(Formula f)
Formula	SubArrayLength.sub(Formula p)
Formula	SubForm.sub(Formula f)
Formula	SubInstancesSet.sub(Formula p) Substitutes instances with instances \/ f
Formula	SubInstancesSingle.sub(Formula p) Substitute instances with instances \/ {f} into a given formula.
Formula	SubMemberField.sub(Formula f)
Formula	SubTmpVar.sub(Formula p)
Formula	SubTypeofSet.sub(Formula p) Substitutes typeof with typeof <+ f * {t} in p.
Formula	SubTypeofSingle.sub(Formula p) Substitues typeof by typeof <+ {f |-> t} in p.
Formula	Substitution.sub(Formula f) Apply the current substitution on a formula.

Constructors in jml2b.pog.substitution with parameters of type Formula

SubArrayElement(java.lang.String e, Formula n)
Constructs a substitution

SubArrayElementSingle(ElementsForm e, Formula a, Formula i, Formula v)
Constructs a substitution

SubArrayLength(Formula f)
Constructs a substitution

SubForm(Formula a, Formula b)
Constructs a substitution.

SubInstancesSet(Formula f)
Constructs a substitution for instances

SubInstancesSingle(Formula f)
Constructs a substitution for instances

SubMemberField(Formula a, java.lang.String b, java.lang.String c, Formula d)
Constructs a substitution

SubMemberField(Formula a, Formula b, Formula c, Formula d)
Constructs a substitution form another one or from a loaded one

SubStaticOrLocalField(Formula a, Formula b)

SubTmpVar(java.lang.String tmp, Formula f)
Constructs a substitution.

SubTypeof(Formula f, Formula t)
Constructs a substitution for typeof

SubTypeofSet(Formula f, Formula t)
Constructs a substitution for typeof

SubTypeofSingle(Formula f, Formula t)
Constructs a substitution for typeof

Uses of Formula in jml2b.pog.util

Methods in jml2b.pog.util that return Formula

Formula	ContextFromPureMethod.getFormulaWithContext() Returns the result of the translation.
Formula	ContextFromPureMethod.getFormula() Returns the formula.

Constructors in jml2b.pog.util with parameters of type Formula

ContextFromPureMethod(Formula f)
Constructs a context form a formula, the context is empty.

ContextFromPureMethod(ContextFromPureMethod c, Formula f)
Constructs a context from an existing context and a formula.

ContextFromPureMethod(java.lang.String f, Formula res, Type t, Formula ens)
Constructs a context from a method call without parameter.

ContextFromPureMethod(ContextFromPureMethod c, java.lang.String res, Formula f, Type t, Formula ens)
Constructs a context from a method call with parameter.

ContextFromPureMethod(ContextFromPureMethod c1, ContextFromPureMethod c2, Formula f)
Constructs a context from the translation of a binary operator.

ContextFromPureMethod(ContextFromPureMethod c1, ContextFromPureMethod c2, ContextFromPureMethod c3, Formula f)
Constructs a context from the translation of a 3-ary operator.

Uses of Formula in jml2b.structure.java

Methods in jml2b.structure.java that return Formula

Formula

Class.getGlobalMemberInvariant(IJml2bConfiguration config)

Uses of Formula in jml2b.structure.jml

Methods in jml2b.structure.jml that return Formula

Formula

JmlExpression.predToForm(IJml2bConfiguration config) Translates the expression into a formula

Methods in jml2b.structure.jml with parameters of type Formula

abstract SimpleLemma	ModifiesClause.modifiesLemmas(IJml2bConfiguration config, java.util.Vector fields, java.util.Vector nonModifiedFields, Formula[] nonModifiedxxxElements) Returns the lemmas concerning the proof of the modifies clause for the current method.
SimpleLemma	ModifiesEverything.modifiesLemmas(IJml2bConfiguration config, java.util.Vector fields, java.util.Vector nonModifiedFields, Formula[] nonModifiedxxxElements)
SimpleLemma	ModifiesList.modifiesLemmas(IJml2bConfiguration config, java.util.Vector fields, java.util.Vector nonModifiedFields, Formula[] nonModifiedxxxElements)
SimpleLemma	ModifiesNothing.modifiesLemmas(IJml2bConfiguration config, java.util.Vector fields, java.util.Vector nonModifiedFields, Formula[] nonModifiedxxxElements) Returns the lemma corresponding to proof that all the fields and all the array elements have not been modified.

Constructors in jml2b.structure.jml with parameters of type Formula

ModifiesDot(ParsedItem pi, Type t, Formula f, ModifiesIdent m)
Constructs a modified identifier from a formula and a modified field.

Uses of Formula in jml2b.structure.statement

Methods in jml2b.structure.statement that return Formula

Formula	Expression.exprToForm(IJml2bConfiguration config) Converts the expression into a formula.
Formula	Expression.predToForm(IJml2bConfiguration config) Converts the expression, considered as a predicate into a formula
static Formula	WithTypeExp.getDefaultArrayInitialiser(Type t) Returns the formula corresponding to the default array element initializer

Uses of Formula in jpov.structure

Methods in jpov.structure that return Formula

Formula	Goal.getFormula() Returns the formula.
Formula	Goal.getOriginal()
Formula	VirtualFormula.getF() Returns the f.

Uses of Formula in jpov.viewer.lemma

Methods in jpov.viewer.lemma that return Formula

Formula

HypLine.getFormula() Returns the associated formula