jml2b.pog.substitution
Class SubTypeof

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

All Implemented Interfaces:

IFormToken, Substitution

Direct Known Subclasses:

SubTypeofSet, SubTypeofSingle

public abstract class SubTypeof

extends Profiler

implements Substitution

This abstract class describes substitutions applied on typeof

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

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

Method Summary

abstract java.lang.Object	clone() Clones the substitution.
Formula	getF() Returns the formula corresponding to the extended typeof domain.
Formula	getT() Returns the formula corresponding to the value asociated to new domain.
void	save(IJml2bConfiguration config, JpoOutputStream s, IJmlFile jf) Saves the substitution in a .jpo file
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

Methods inherited from interface jml2b.pog.substitution.Substitution

sub

Constructor Detail

SubTypeof

public SubTypeof(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 abstract java.lang.Object clone()

Description copied from interface: Substitution

Clones the substitution.

Specified by:

clone in interface Substitution

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)

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

getF

public Formula getF()

Returns the formula corresponding to the extended typeof domain.

Returns:

f

getT

public Formula getT()

Returns the formula corresponding to the value asociated to new domain.

Returns:

t