jml2b.formula
Class Formula

java.lang.Object
  jml2b.util.Profiler
      jml2b.formula.Formula

All Implemented Interfaces:

IFormToken, java.io.Serializable

Direct Known Subclasses:

BinaryForm, QuantifiedForm, TerminalForm, TriaryForm, TTypeForm, UnaryForm

public abstract class Formula

extends Profiler

implements IFormToken, java.io.Serializable

This class describes a formula. A formula is the content of a lemma : an hypothesis or a goal.

Author:

L. Burdy

See Also:

Serialized Form

Field Summary

Fields inherited from interface jml2b.formula.IFormToken

ARRAY_ACCESS, ARRAY_RANGE, B_ACCOLADE, B_APPLICATION, B_ARRAY_EQUALS, B_BOOL, B_BTRUE, B_COUPLE, B_DOM, B_FUNCTION_EQUALS, B_IN, B_INTERVAL, B_OVERRIDING, B_SET_EQUALS, B_SUBSTRACTION_DOM, B_UNION, CONSTANT_FUNCTION, CONSTANT_FUNCTION_FUNCTION, EQUALS_ON_OLD_INSTANCES, EQUALS_ON_OLD_INSTANCES_ARRAY, FINAL_IDENT, GUARDED_SET, INTERSECTION_IS_NOT_EMPTY, IS_ARRAY, IS_MEMBER_FIELD, IS_STATIC_FIELD, Ja_ADD_OP, Ja_AND_OP, Ja_CHAR_LITERAL, Ja_COMMA, Ja_DIFFERENT_OP, Ja_DIV_OP, Ja_EQUALS_OP, Ja_GE_OP, Ja_GREATER_OP, Ja_IDENT, Ja_JAVA_BUILTIN_TYPE, Ja_LE_OP, Ja_LESS_OP, Ja_LITERAL_false, Ja_LITERAL_null, Ja_LITERAL_super, Ja_LITERAL_this, Ja_LITERAL_true, Ja_LNOT, Ja_MOD, Ja_MUL_OP, Ja_NEGATIVE_OP, Ja_NUM_INT, Ja_OR_OP, Ja_QUESTION, Ja_STRING_LITERAL, Ja_UNARY_NUMERIC_OP, Jm_AND_THEN, Jm_EXISTS, Jm_FORALL, Jm_IMPLICATION_OP, Jm_IS_SUBTYPE, Jm_OR_ELSE, Jm_T_OLD, Jm_T_RESULT, Jm_T_TYPE, LOCAL_ELEMENTS_DECL, LOCAL_VAR_DECL, MODIFIED_FIELD, NEW_OBJECT, T_CALLED_OLD, T_TYPE, T_VARIANT_OLD, toString

Method Summary

static BinaryForm	and(Formula s1, Formula s2) Returns the conjunctive formula between the two parameters.
abstract java.lang.Object	clone() Clones the formula.
abstract int	contains(java.util.Vector selectedFields)
static Formula	create(IJml2bConfiguration config, JpoInputStream s, IJmlFile fi) Create a formula from a token read into a stream.
static Formula	declarField(Field f) Returns the formula corresponding to a field declaration.
Formula	domainRestrict(java.util.Vector df) Applies successive domain restriction to the formula
abstract boolean	equals(java.lang.Object f) Returns whether the formula equals the parameter.
abstract void	garbageIdent() Annotates all the fields that appear in the formula to declare them in the Atelier B files.
abstract BasicType	getBasicType() Returns the type of a formula
static Formula	getFalse() Returns the formula false.
abstract void	getFields(java.util.Set fields) Collects the fields that occur in the formula.
byte	getNodeType() Returns the nodeType.
static Formula	getNull() Returns the formula null.
static BinaryForm	implies(Formula s1, Formula s2) Returns the implicative formula between the two parameters.
static java.lang.String	indent(int i) Returns the string containing white spaces corresponding to an indentation
abstract Formula	instancie(Formula b) Replaces this with the parameter in the expression.
abstract boolean	is(Formula f) Returns whether the formula corresponds to a read formula.
boolean	isBFalse() Returns whether a formula corresponds to bfalse
abstract boolean	isObvious(boolean atTheEnd) Returns whether a formula is obvious.
boolean	matchAEqualsNull() Returns whether a formula matches with an equality with null
static UnaryForm	not(Formula s1) Returns the negation of the parameter.
Formula	oldParam(java.util.Vector signature) Encapsulates given parameters into an old pragma.
static BinaryForm	or(Formula s1, Formula s2) Returns the disjunctive formula between the two parameters.
abstract void	processIdent() Collects all the indentifier of a formula to give them an index in the identifer array.
Formula	renameParam(IAParameters signature, java.util.Vector newSignature) Renames the fields belonging to the parameter list with new names.
abstract void	save(IJml2bConfiguration config, IOutputStream s, IJmlFile jf) Saves the formula in a .jpo file
Formula	sub(Field a, Field b, boolean subInCalledOld) Applies a substitution on a formula.
abstract Formula	sub(Formula a, Formula b, boolean subInCalledOld) Applies a substitution on a formula.
abstract Formula	subIdent(java.lang.String a, Formula b) Applies a substitution on a formula.
abstract Formula	suppressSpecialOld(int token) Suppress the called old pragmas.
java.lang.String	toJava(int indent) Translates the formula into the Java language
ITranslationResult	toLang(java.lang.String language, int indent) Translates the formula into a given language.
java.util.Vector	toVector() Converts comma separated formulas into a set of formulas.

Methods inherited from class jml2b.util.Profiler

runGC

Methods inherited from class java.lang.Object

getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Method Detail

getNull

public static Formula getNull()

Returns the formula null.

Returns:

the formula null

getFalse

public static Formula getFalse()

Returns the formula false.

Returns:

the formula false

or

public static BinaryForm or(Formula s1,
                            Formula s2)

Returns the disjunctive formula between the two parameters.

Parameters:

s1 - left disjonctive formula

s2 - right disjonctive formula

Returns:

the formula s1 || s2

declarField

public static Formula declarField(Field f)

Returns the formula corresponding to a field declaration.

Parameters:

f - Field to declare.

Returns:

and

public static BinaryForm and(Formula s1,
                             Formula s2)

Returns the conjunctive formula between the two parameters.

Parameters:

s1 - left conjonctive formula

s2 - right conjonctive formula

Returns:

the formula s1 && s2

not

public static UnaryForm not(Formula s1)

Returns the negation of the parameter.

Parameters:

s1 - negated formula

Returns:

the formula ! s1

implies

public static BinaryForm implies(Formula s1,
                                 Formula s2)

Returns the implicative formula between the two parameters.

Parameters:

s1 - left implicative formula

s2 - right implicative formula

Returns:

the formula s1 ==> s2

create

public static Formula create(IJml2bConfiguration config,
                             JpoInputStream s,
                             IJmlFile fi)
                      throws java.io.IOException,
                             LoadException

Create a formula from a token read into a stream.

Parameters:

config - The current configuration

s - The input stream

fi - The JML file corresponding to the input stream.

Returns:

a new formula instanciated with the read token, ready to be parsed.

Throws:

java.io.IOException - if the end of the stream is reached before the formula has been read

LoadException - if the read token is unknown.

indent

public static java.lang.String indent(int i)

Returns the string containing white spaces corresponding to an indentation

Parameters:

i - The indentation number

Returns:

a string with a carriage return and i white spaces.

getBasicType

public abstract BasicType getBasicType()

Returns the type of a formula

Returns:

The basic type of ta formula.

clone

public abstract java.lang.Object clone()

Clones the formula.

Returns:

the cloned formula

processIdent

public abstract void processIdent()

Collects all the indentifier of a formula to give them an index in the identifer array. This array is then analyzed to give short name when it is possible to identifiers.

See Also:

jml2b.pog.IdentifierResolver#bIdents

instancie

public abstract Formula instancie(Formula b)

Replaces this with the parameter in the expression.

Parameters:

b - expression on which the method where the expression occurs is called.

Returns:

the modified expression

getFields

public abstract void getFields(java.util.Set fields)

Collects the fields that occur in the formula.

Parameters:

fields - The set a collected fields.

sub

public abstract Formula sub(Formula a,
                            Formula b,
                            boolean subInCalledOld)

Applies a substitution on a formula.

Parameters:

a - the substituted formula

b - the new formula

subInCalledOld - specify whether the substitution should also be applied in the called old construction

Returns:

the formula when the substitution has been applied.

suppressSpecialOld

public abstract Formula suppressSpecialOld(int token)

Suppress the called old pragmas. old pragma are substitued with called old into the specification of a called method in manner to be differentiated from the old pragma of the current method. After the treatment, the called old pragmas are suppressed.

Returns:

the formula with suppressed called old pragmas

subIdent

public abstract Formula subIdent(java.lang.String a,
                                 Formula b)

Applies a substitution on a formula.

Parameters:

a - the substituted string correspondingto an identifier

b - the new formula

Returns:

the formula when the substitution has been applied.

equals

public abstract boolean equals(java.lang.Object f)

Returns whether the formula equals the parameter.

Parameters:

f - the checked parameter

Returns:

true if the formula syntaxically equals the parameter, false otherwise

is

public abstract boolean is(Formula f)

Returns whether the formula corresponds to a read formula.

Parameters:

f - a read formula coming from a jpo file

Returns:

true if the formula equals to the read formula, false otherwise.

Throws:

MergeException

isObvious

public abstract boolean isObvious(boolean atTheEnd)

Returns whether a formula is obvious.

Returns:

true if the formula is considered as obvious, false otherwise

save

public abstract void save(IJml2bConfiguration config,
                          IOutputStream s,
                          IJmlFile jf)
                   throws java.io.IOException

Saves the formula in a .jpo file

Parameters:

config -

s - the ouputstream corresponding to a jpo file

jf -

Throws:

java.io.IOException - when the formula cannot be saved.

garbageIdent

public abstract void garbageIdent()

Annotates all the fields that appear in the formula to declare them in the Atelier B files.

contains

public abstract int contains(java.util.Vector selectedFields)

oldParam

public Formula oldParam(java.util.Vector signature)

Encapsulates given parameters into an old pragma.

Parameters:

signature - the signature of a called method

Returns:

the formula when the parameters have been encapsulated

toJava

public java.lang.String toJava(int indent)

Translates the formula into the Java language

Parameters:

indent - The current indentation

Returns:

the string corresponding to the translated formula.

toLang

public ITranslationResult toLang(java.lang.String language,
                                 int indent)
                          throws LanguageException

Translates the formula into a given language.

Parameters:

language - The language in which the formula should be translated.

indent - The current indentation

Returns:

the result of the translation

Throws:

LanguageException - when the language is unknown.

sub

public Formula sub(Field a,
                   Field b,
                   boolean subInCalledOld)

Applies a substitution on a formula.

Parameters:

a - the substituted field

b - the new field

subInCalledOld - specify whether the substitution should also be applied in the called old construction

Returns:

the formula when the substitution has been applied.

renameParam

public Formula renameParam(IAParameters signature,
                           java.util.Vector newSignature)
                    throws PogException

Renames the fields belonging to the parameter list with new names.

Parameters:

signature - the signature of the called method

newSignature - the list of new names

Returns:

the current formula renamed

Throws:

PogException

See Also:

jml2b.pog.Proofs#renameParam(Parameters, Vector)

isBFalse

public boolean isBFalse()

Returns whether a formula corresponds to bfalse

Returns:

true when the formula is false == true or true == false, false otherwise.

matchAEqualsNull

public boolean matchAEqualsNull()

Returns whether a formula matches with an equality with null

Returns:

true if the formula matches with a == null, false otherwise.

toVector

public java.util.Vector toVector()

Converts comma separated formulas into a set of formulas.

Returns:

the vector containing comme separated formulas

See Also:

BinaryForm.toVector()

domainRestrict

public Formula domainRestrict(java.util.Vector df)

Applies successive domain restriction to the formula

Parameters:

df - set of formula from which the formula should be restricted.

Returns:

the formula with domain restricted with the set of given formulas

getNodeType

public byte getNodeType()

Returns the nodeType.

Returns:

byte