jml2b.formula
Class ModifiedFieldForm

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

All Implemented Interfaces:

IFormToken, java.io.Serializable

Direct Known Subclasses:

JavaModifiedFieldForm

public class ModifiedFieldForm

extends TerminalForm

Author:

L. Burdy

See Also:

Serialized Form

Field Summary

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

ModifiedFieldForm(AField f, IModifiesField m)

ModifiedFieldForm(ModifiedFieldForm f)

Methods inherited from class jml2b.formula.TerminalForm

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

Constructor Detail

ModifiedFieldForm

public ModifiedFieldForm(ModifiedFieldForm f)

ModifiedFieldForm

public ModifiedFieldForm(AField f,
                         IModifiesField m)