jml2b.formula
Class TerminalForm

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

All Implemented Interfaces:

IFormToken, java.io.Serializable

Direct Known Subclasses:

ElementsForm, JavaTerminalForm, ModifiedFieldForm

public class TerminalForm

extends Formula

This class implements terminal formula: identifiers, literal constants and builtin types. The node type can be

• Ja_IDENT
• FINAL_IDENT
• B_BTRUE
• Ja_CHAR_LITERAL
• Ja_NUM_INT
• Ja_LITERAL_false
• Ja_LITERAL_true
• Ja_JAVA_BUILTIN_TYPEs
• Ja_LITERAL_null
• Ja_LITERAL_this
• Ja_LITERAL_super
• Ja_STRING_LITERAL
• Jm_T_RESULT

Author:

L.Burdy

See Also:

Serialized Form

Field Summary

static TerminalForm	arraylength The formula arraylength.
static TerminalForm	elemtype The constant formula elemtype, In the B lemmas, elemtype is a function that assign the type of its element to an array instance.
static TerminalForm	instances The formula instances.
static TerminalForm	j_int2byte The constant formula j_int2byte, In the B lemmas, j_int2byte is a function that converts an int into a byte.
static TerminalForm	j_int2char The constant formula j_int2char, In the B lemmas, j_int2char is a function that converts an int into a char.
static TerminalForm	j_int2short The constant formula j_int2short, In the B lemmas, j_int2short is a function that converts an int into a short.
static TerminalForm	REFERENCES The constant formula REFERENCES.
static TerminalForm	typeof The formula typeof.

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

Constructor Summary

TerminalForm(byte nodeType)
Constructs a formula that is not a Java identifer.

TerminalForm(byte nodeType, java.lang.String nodeText)
Constructs a formula that is not a Java identifer.

TerminalForm(byte nodeType, java.lang.String nodeText, Identifier ident, boolean subident)
Constructs a terminal formula.

TerminalForm(Identifier ident)
Constructs a formula from a Java identifer.

TerminalForm(Identifier ident, java.lang.String subident)
Constructs a formula from a Java identifer and a postfix string.

TerminalForm(int v)
Constructs a formula that is a Ja_NUM_INT.

TerminalForm(java.lang.String nodeText)
Constructs a formula that is an identifier but not a Java identifer.

Method Summary

java.lang.Object	clone() Clones the formula.
int	contains(java.util.Vector selectedFields)
boolean	equals(java.lang.Object f) Returns whether the formula equals the parameter.
void	garbageIdent() Annotates all the fields that appear in the formula to declare them in the Atelier B files.
static TerminalForm	getArraylength(IJml2bConfiguration config)
BasicType	getBasicType() Returns the type of a formula
void	getFields(java.util.Set fields) Collects the fields that occur in the formula.
Identifier	getIdent()
java.lang.String	getNodeText() Returns the nodeText.
java.lang.String	getNonAmbiguousName()
Formula	instancie(Formula b) Replaces this with the parameter in the expression.
boolean	is(Formula f) Returns whether the formula corresponds to a read formula.
boolean	isObvious(boolean atTheEnd) Returns whether a formula is obvious.
void	processIdent() Collects all the indentifier of a formula to give them an index in the identifer array.
void	save(IJml2bConfiguration config, IOutputStream s, IJmlFile jf) Saves the formula in a .jpo file
void	setBox(ParsedItem box) Sets the box.
Formula	sub(Formula a, Formula b, boolean subInCalledOld) Applies a substitution on a formula.
Formula	subIdent(java.lang.String a, Formula b) Applies a substitution on a formula.
Formula	suppressSpecialOld(int token) Suppress the called old pragmas.
Expression	toExp()

Methods inherited from class jml2b.formula.Formula

and, create, declarField, domainRestrict, getFalse, getNodeType, getNull, implies, indent, isBFalse, matchAEqualsNull, not, oldParam, or, renameParam, sub, toJava, toLang, toVector

Methods inherited from class jml2b.util.Profiler

runGC

Methods inherited from class java.lang.Object

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

Field Detail

instances

public static TerminalForm instances

The formula instances. In the B lemmas, instances is the set of all current class instances.

typeof

public static TerminalForm typeof

The formula typeof. In the B lemmas, typeof is a function that assign a type to an instance.

arraylength

public static TerminalForm arraylength

The formula arraylength. In the B lemmas, arraylength is a function that assign the length to an array instance.

REFERENCES

public static TerminalForm REFERENCES

The constant formula REFERENCES. In the B lemmas, REFERENCES is the set of all existing or potential instances.

elemtype

public static TerminalForm elemtype

The constant formula elemtype, In the B lemmas, elemtype is a function that assign the type of its element to an array instance.

j_int2short

public static TerminalForm j_int2short

The constant formula j_int2short, In the B lemmas, j_int2short is a function that converts an int into a short.

j_int2byte

public static TerminalForm j_int2byte

The constant formula j_int2byte, In the B lemmas, j_int2byte is a function that converts an int into a byte.

j_int2char

public static TerminalForm j_int2char

The constant formula j_int2char, In the B lemmas, j_int2char is a function that converts an int into a char.

Constructor Detail

TerminalForm

public TerminalForm(byte nodeType,
                    java.lang.String nodeText,
                    Identifier ident,
                    boolean subident)

Constructs a terminal formula.

Parameters:

nodeType - The node type of this formula

nodeText - The string corresponding to this formula

ident - The identifier corresponding to this formula

subident - The postfix string associated with this formula

TerminalForm

public TerminalForm(byte nodeType)

Constructs a formula that is not a Java identifer.

Parameters:

nodeType - The node type of this formula

TerminalForm

public TerminalForm(byte nodeType,
                    java.lang.String nodeText)

Constructs a formula that is not a Java identifer.

Parameters:

nodeType - The node type of this formula

nodeText - The string corresponding to this formula

TerminalForm

public TerminalForm(int v)

Constructs a formula that is a Ja_NUM_INT.

Parameters:

v - The integer value

TerminalForm

public TerminalForm(java.lang.String nodeText)

Constructs a formula that is an identifier but not a Java identifer.

Parameters:

nodeText - The string corresponding to this formula

TerminalForm

public TerminalForm(Identifier ident)

Constructs a formula from a Java identifer.

Parameters:

ident - The identifier corresponding to this formula

TerminalForm

public TerminalForm(Identifier ident,
                    java.lang.String subident)

Constructs a formula from a Java identifer and a postfix string.

Parameters:

ident - The identifier corresponding to this formula

subident - The postfix string associated with this formula

Method Detail

getArraylength

public static TerminalForm getArraylength(IJml2bConfiguration config)
                                   throws Jml2bException

Throws:

Jml2bException

clone

public java.lang.Object clone()

Description copied from class: Formula

Clones the formula.

Specified by:

clone in class Formula

Returns:

the cloned formula

processIdent

public void processIdent()

Description copied from class: Formula

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.

Specified by:

processIdent in class Formula

See Also:

jml2b.pog.IdentifierResolver#bIdents

instancie

public Formula instancie(Formula b)

Description copied from class: Formula

Replaces this with the parameter in the expression.

Specified by:

instancie in class Formula

Parameters:

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

Returns:

the modified expression

garbageIdent

public void garbageIdent()

Description copied from class: Formula

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

Specified by:

garbageIdent in class Formula

getFields

public void getFields(java.util.Set fields)

Description copied from class: Formula

Collects the fields that occur in the formula.

Specified by:

getFields in class Formula

Parameters:

fields - The set a collected fields.

sub

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

Description copied from class: Formula

Applies a substitution on a formula.

Specified by:

sub in class 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.

subIdent

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

Description copied from class: Formula

Applies a substitution on a formula.

Specified by:

subIdent in class Formula

Parameters:

a - the substituted string correspondingto an identifier

b - the new formula

Returns:

the formula when the substitution has been applied.

equals

public boolean equals(java.lang.Object f)

Description copied from class: Formula

Returns whether the formula equals the parameter.

Specified by:

equals in class Formula

Parameters:

f - the checked parameter

Returns:

true if the formula syntaxically equals the parameter, false otherwise

is

public boolean is(Formula f)

Description copied from class: Formula

Returns whether the formula corresponds to a read formula.

Specified by:

is in class Formula

Parameters:

f - a read formula coming from a jpo file

Returns:

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

contains

public int contains(java.util.Vector selectedFields)

Specified by:

contains in class Formula

isObvious

public boolean isObvious(boolean atTheEnd)

Description copied from class: Formula

Returns whether a formula is obvious.

Specified by:

isObvious in class Formula

Returns:

true if the formula is considered as obvious, false otherwise

save

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

Description copied from class: Formula

Saves the formula in a .jpo file

Specified by:

save in class Formula

Parameters:

config -

s - the ouputstream corresponding to a jpo file

jf -

Throws:

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

getNonAmbiguousName

public java.lang.String getNonAmbiguousName()

suppressSpecialOld

public Formula suppressSpecialOld(int token)

Description copied from class: Formula

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.

Specified by:

suppressSpecialOld in class Formula

Returns:

the formula with suppressed called old pragmas

getNodeText

public java.lang.String getNodeText()

Returns the nodeText.

Returns:

String

setBox

public void setBox(ParsedItem box)

Sets the box.

Parameters:

box - The box to set

getBasicType

public BasicType getBasicType()

Description copied from class: Formula

Returns the type of a formula

Specified by:

getBasicType in class Formula

Returns:

The basic type of ta formula.

getIdent

public Identifier getIdent()

Returns:

toExp

public Expression toExp()