jml2b.formula
Class ElementsForm

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

All Implemented Interfaces:

IFormToken, java.io.Serializable

public final class ElementsForm

extends TerminalForm

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. The token associated with those formulas is Ja_IDENT

Author:

L. Burdy

See Also:

Serialized Form

Field Summary

static ElementsForm	booleanelements The formula booleanelements_n.
static ElementsForm	byteelements The formula byteelements_n.
static ElementsForm	charelements The formula charelements_n.
static ElementsForm[]	elements Array of all xxxelements_n formulas.
static int[]	elementsType Array of type corresponding to each xxxelements_n formula.
static ElementsForm	intelements The formula intelements_n.
static ElementsForm	refelements The formula refelements_n.
static ElementsForm	shortelements The formula shortelements_n.

Fields inherited from class jml2b.formula.TerminalForm

arraylength, elemtype, instances, j_int2byte, j_int2char, j_int2short, REFERENCES, 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

ElementsForm(ElementsForm e)

Method Summary

static void	clearSuffix() Resets all the suffix of the xxxelements_n formula to 0.
static ElementsForm	getElementsName(Type t) Returns the xxxelements_n formula corresponding to a type.
Formula	getType() Returns the B type of the formula.
void	save(IJml2bConfiguration config, IOutputStream s, IJmlFile jf) Saves the formula in a .jpo file

Methods inherited from class jml2b.formula.TerminalForm

clone, contains, equals, garbageIdent, getArraylength, getBasicType, getFields, getIdent, getNodeText, getNonAmbiguousName, instancie, is, isObvious, processIdent, setBox, sub, subIdent, suppressSpecialOld, 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

intelements

public static ElementsForm intelements

The formula intelements_n.

shortelements

public static ElementsForm shortelements

The formula shortelements_n.

byteelements

public static ElementsForm byteelements

The formula byteelements_n.

booleanelements

public static ElementsForm booleanelements

The formula booleanelements_n.

charelements

public static ElementsForm charelements

The formula charelements_n.

refelements

public static ElementsForm refelements

The formula refelements_n.

elements

public static ElementsForm[] elements

Array of all xxxelements_n formulas.

elementsType

public static int[] elementsType

Array of type corresponding to each xxxelements_n formula.

Constructor Detail

ElementsForm

public ElementsForm(ElementsForm e)

Method Detail

clearSuffix

public static void clearSuffix()

Resets all the suffix of the xxxelements_n formula to 0.

getElementsName

public static ElementsForm getElementsName(Type t)

Returns the xxxelements_n formula corresponding to a type.

Parameters:

t - The type of the elements of the searched array

Returns:

the xxxelements_n formula corresponding to t.

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

Overrides:

save in class TerminalForm

Throws:

java.io.IOException

getType

public Formula getType()

Returns the B type of the formula.

Returns:

the B type: a function of function.