jml2b.pog.substitution
Class SubTypeofSet

java.lang.Object
  jml2b.util.Profiler
      jml2b.pog.substitution.SubTypeof
          jml2b.pog.substitution.SubTypeofSet

All Implemented Interfaces:

IFormToken, Substitution

public class SubTypeofSet

extends SubTypeof

This interface describes a substitution of typeof by typeof <+ f * {t}

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

SubTypeofSet(Formula f, Formula t)
Constructs a substitution for typeof

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 p) Substitutes typeof with typeof <+ f * {t} in p.

Methods inherited from class jml2b.pog.substitution.SubTypeof

getF, getT, sub

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

SubTypeofSet

public SubTypeofSet(Formula f,
                    Formula t)

Constructs a substitution for typeof

Parameters:

f - The formula corresponding to the extended typeof domain

t - The formula corresponding to the value asociated to new domain

Method Detail

clone

public java.lang.Object clone()

Description copied from interface: Substitution

Clones the substitution.

Specified by:

clone in interface Substitution

Specified by:

clone in class SubTypeof

sub

public Formula sub(Formula p)

Substitutes typeof with typeof <+ f * {t} in p.

Parameters:

p - The formula on which the substitution is applied

Returns:

the substitued formula

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

Overrides:

save in class SubTypeof

Throws:

java.io.IOException