jpov.substitution
Class SubInstancesSet

java.lang.Object
  jpov.substitution.SubInstances
      jpov.substitution.SubInstancesSet

All Implemented Interfaces:

IFormToken, Substitution

public class SubInstancesSet

extends jpov.substitution.SubInstances

implements IFormToken

This class corresponds to the substituion of instances with: instances \/ f.

Author:

L. Burdy

Field Summary

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

SubInstancesSet(IJml2bConfiguration config, IJmlFile fi, JpoInputStream s)
Constructs a substitution for instances

Method Summary

java.lang.String	getInfo() If f is a singleton, returns "a new istance: f" else return "new instances: f".
void	save(IJml2bConfiguration config, JpoOutputStream s, IJmlFile jf) Saves the substitution in a .jpo file

Methods inherited from class java.lang.Object

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

Constructor Detail

SubInstancesSet

public SubInstancesSet(IJml2bConfiguration config,
                       IJmlFile fi,
                       JpoInputStream s)
                throws java.io.IOException,
                       LoadException

Constructs a substitution for instances

Method Detail

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

Throws:

java.io.IOException

getInfo

public java.lang.String getInfo()

If f is a singleton, returns "a new istance: f" else return "new instances: f".

Specified by:

getInfo in interface Substitution

Returns:

a string that is displayed with the initial formula corresponding to the goal.