jml2b.pog.substitution
Class SubMemberField

java.lang.Object
  jml2b.util.Profiler
      jml2b.pog.substitution.SubMemberField

All Implemented Interfaces:

IFormToken, Substitution

public class SubMemberField

extends Profiler

implements Substitution

This class implements a substitution of a member field a by a <+ { b |-> c } corresponding to an affectation of a new value for a given instance.

Author:

L. Burdy

Field Summary

Fields inherited from interface jml2b.pog.substitution.Substitution

ARRAY_ELEMENT, ARRAY_ELEMENT_SINGLE, ARRAY_LENGTH, FORM, INSTANCES_SET, INSTANCES_SINGLE, MEMBER_FIELD, TMP_VAR, TYPEOF_SET, TYPEOF_SINGLE

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

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

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

Method Summary

java.lang.Object	clone() Clones the substitution.
Formula	getField()
Formula	getInstance()
void	save(IJml2bConfiguration config, JpoOutputStream s, IJmlFile jf) Saves the substitution in a .jpo file
Formula	sub(Formula f) Apply the current substitution on a formula.
void	sub(Substitution s) Apply a substitution on the current substitution.

Methods inherited from class jml2b.util.Profiler

runGC

Methods inherited from class java.lang.Object

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

Constructor Detail

SubMemberField

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

Constructs a substitution

Parameters:

a - The initial member field

b - The new member field

c - The instance

d - The value

SubMemberField

public SubMemberField(Formula a,
                      Formula b,
                      Formula c,
                      Formula d)

Constructs a substitution form another one or from a loaded one

Parameters:

a - The initial member field

b - The new member field

c - The instance

d - The value

Method Detail

clone

public java.lang.Object clone()

Description copied from interface: Substitution

Clones the substitution.

Specified by:

clone in interface Substitution

sub

public Formula sub(Formula f)

Description copied from interface: Substitution

Apply the current substitution on a formula.

Specified by:

sub in interface Substitution

Parameters:

f - The formula on which the substitution is applied

Returns:

[old := b <+ {c |->d}]f

sub

public void sub(Substitution s)

Description copied from interface: Substitution

Apply a substitution on the current substitution.

Specified by:

sub in interface Substitution

Parameters:

s - The substitution to applied

save

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

Description copied from interface: Substitution

Saves the substitution in a .jpo file

Specified by:

save in interface Substitution

Parameters:

config -

s - output stream for the jpo file

jf -

Throws:

java.io.IOException

See Also:

jml2b.pog.NonObviousGoal#save(DataOutputStream, JmlFile, IJmlFile)

getField

public Formula getField()

getInstance

public Formula getInstance()