jml2b.pog.substitution
Interface Substitution

All Superinterfaces:

IFormToken

All Known Implementing Classes:

SubArrayElement, SubArrayElementSingle, SubArrayLength, SubForm, SubInstances, SubMemberField, SubTmpVar, SubTypeof

public interface Substitution

extends IFormToken

This interface describes a substitution. Let a, b, c be formulas, a substitution can be the substitution of:

• an xxxelements by a
• arraylength by a
• a formula by a
• instances by instances \/ a
• instances by instances \/ {a}
• a temporary variable by a
• typeof by typeof <+ a * {b}
• typeof by typeof <+ a |-> b
• a member field by a <+ { b |-> c }

Author:

L. Burdy

Field Summary

static byte	ARRAY_ELEMENT Substitution type corresponding to the substitution of an xxxelements by a
static byte	ARRAY_ELEMENT_SINGLE
static byte	ARRAY_LENGTH Substitution type corresponding to the substitution of arraylength by a
static byte	FORM Substitution type corresponding to the substitution of a formula by a
static byte	INSTANCES_SET Substitution type corresponding to the substitution of instances by instances \/ a
static byte	INSTANCES_SINGLE Substitution type corresponding to the substitution of instances by instances \/ {a}
static byte	MEMBER_FIELD Substitution type corresponding to the substitution of a member field by a <+ { b |-> c }
static byte	TMP_VAR Substitution type corresponding to the substitution of a temporary variable by a
static byte	TYPEOF_SET Substitution type corresponding to the substitution of typeof by typeof <+ a * {b}
static byte	TYPEOF_SINGLE Substitution type corresponding to the substitution of typeof by typeof <+ a |-> b

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

java.lang.Object	clone() Clones the substitution.
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.

Field Detail

ARRAY_ELEMENT

public static final byte ARRAY_ELEMENT

Substitution type corresponding to the substitution of an xxxelements by a

See Also:

Constant Field Values

ARRAY_LENGTH

public static final byte ARRAY_LENGTH

Substitution type corresponding to the substitution of arraylength by a

See Also:

Constant Field Values

FORM

public static final byte FORM

Substitution type corresponding to the substitution of a formula by a

See Also:

Constant Field Values

INSTANCES_SET

public static final byte INSTANCES_SET

Substitution type corresponding to the substitution of instances by instances \/ a

See Also:

Constant Field Values

INSTANCES_SINGLE

public static final byte INSTANCES_SINGLE

Substitution type corresponding to the substitution of instances by instances \/ {a}

See Also:

Constant Field Values

TMP_VAR

public static final byte TMP_VAR

Substitution type corresponding to the substitution of a temporary variable by a

See Also:

Constant Field Values

TYPEOF_SET

public static final byte TYPEOF_SET

Substitution type corresponding to the substitution of typeof by typeof <+ a * {b}

See Also:

Constant Field Values

TYPEOF_SINGLE

public static final byte TYPEOF_SINGLE

Substitution type corresponding to the substitution of typeof by typeof <+ a |-> b

See Also:

Constant Field Values

MEMBER_FIELD

public static final byte MEMBER_FIELD

Substitution type corresponding to the substitution of a member field by a <+ { b |-> c }

See Also:

Constant Field Values

ARRAY_ELEMENT_SINGLE

public static final byte ARRAY_ELEMENT_SINGLE

See Also:

Constant Field Values

Method Detail

clone

public java.lang.Object clone()

Clones the substitution.

Returns:

the cloned substitution

sub

public Formula sub(Formula f)

Apply the current substitution on a formula.

Parameters:

f - The formula on which the substitution is applied

Returns:

the substitued formula

sub

public void sub(Substitution s)

Apply a substitution on the current substitution.

Parameters:

s - The substitution to applied

save

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

Saves the substitution in a .jpo file

Parameters:

config -

s - output stream for the jpo file

jf -

Throws:

java.io.IOException

See Also:

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