gt: 			if (string.length() > STRING_COMPRESS_THRESHOLD) {
context: package keel.Algorithms.ImbalancedClassification.Resampling.SMOTE_RSB.Rough_Sets;
  
  import java.io.Serializable;
  import java.text.ParseException;
  import java.text.SimpleDateFormat;
  import java.util.Date;
  import java.util.Enumeration;
  import java.util.Hashtable;
  import java.util.Properties;
  import java.io.StreamTokenizer;
  import java.io.StringReader;
  import java.io.IOException;
  
  /**
   * Class for handling an attribute. Once an attribute has been created, it can't
   * be changed.
   * <p>
   * 
   * Three attribute types are supported:
   * <ul>
   * <li> numeric:
   * <ul>
   * This type of attribute represents a floating-point number.
   * </ul>
   * <li> nominal:
   * <ul>
   * This type of attribute represents a fixed set of nominal values.
   * </ul>
   * <li> string:
   * <ul>
   * This type of attribute represents a dynamically expanding set of nominal
   * values. String attributes are not used by the learning schemes in Weka. They
   * can be used, for example, to store an identifier with each instance in a
   * dataset.
   * </ul>
   * </ul>
   * Typical usage (code from the main() method of this class):
   * <p>
   * 
   * <code>
   * ... <br>
   *
   * // Create numeric attributes "length" and "weight" <br>
   * Attribute length = new Attribute("length"); <br>
   * Attribute weight = new Attribute("weight"); <br><br>
   * 
   * // Create vector to hold nominal values "first", "second", "third" <br>
   * FastVector my_nominal_values = new FastVector(3); <br>
   * my_nominal_values.addElement("first"); <br>
   * my_nominal_values.addElement("second"); <br>
   * my_nominal_values.addElement("third"); <br><br>
   *
   * // Create nominal attribute "position" <br>
   * Attribute position = new Attribute("position", my_nominal_values);<br>
   *
   * ... <br>
   * </code>
   * <p>
   * 
   * @author Eibe Frank (eibe@cs.waikato.ac.nz)
   * @version $Revision: 1.1 $
   */
  public class Attribute implements Copyable, Serializable {
  
  	/** Constant set for numeric attributes. */
  	public static final int REAL = 0;
  
  	/** Constant set for nominal attributes. */
  	public static final int NOMINAL = 1;
  
  	/** Constant set for attributes with string values. */
  	public static final int STRING = 2;
  
  	/** Constant set for attributes with date values. */
  	public static final int DATE = 3;
  
  	/** Constant set for relation-valued attributes. */
  	public static final int RELATIONAL = 4;
  
  	/** Constant set for symbolic attributes. */
  	public static final int ORDERING_SYMBOLIC = 0;
  
  	/** Constant set for ordered attributes. */
  	public static final int ORDERING_ORDERED = 1;
  
  	/** Constant set for modulo-ordered attributes. */
  	public static final int ORDERING_MODULO = 2;
  
  	/** The keyword used to denote the start of an arff attribute declaration */
  	static String ARFF_ATTRIBUTE = "@attribute";
  
  	/** A keyword used to denote a numeric attribute */
  	static String ARFF_ATTRIBUTE_INTEGER = "integer";
  
  	/** A keyword used to denote a numeric attribute */
  	/**static String ARFF_ATTRIBUTE_REAL = "real";
  
  	/** A keyword used to denote a numeric attribute */
  	static String ARFF_ATTRIBUTE_REAL = "real";
  
  	/** The keyword used to denote a string attribute */
  	static String ARFF_ATTRIBUTE_STRING = "string";
  
  	/** The keyword used to denote a date attribute */
  	static String ARFF_ATTRIBUTE_DATE = "date";
  
  	/** The keyword used to denote a relation-valued attribute */
  	static String ARFF_ATTRIBUTE_RELATIONAL = "relational";
  
  	/** The keyword used to denote the end of the declaration of a subrelation */
  	static String ARFF_END_SUBRELATION = "@end";
  
  	/** Strings longer than this will be stored compressed. */
  	private static final int STRING_COMPRESS_THRESHOLD = 200;
  
  	/** The attribute's name. */
  	private/* @ spec_public non_null @ */String m_Name;
  
  	/** The attribute's type. */
  	private/* @ spec_public @ */int m_Type;
  	/*
  	 * @ invariant m_Type == NUMERIC || m_Type == DATE || m_Type == STRING ||
  	 * m_Type == NOMINAL || m_Type == RELATIONAL;
  	 */
  
  	/** The attribute's values (if nominal or string). */
  	private/* @ spec_public @ */FastVector m_Values;
  
  	/** Mapping of values to indices (if nominal or string). */
  	private Hashtable m_Hashtable;
  
  	/** The header information for a relation-valued attribute. */
  	private Instances m_Header;
  
  	/** Date format specification for date attributes */
  	private SimpleDateFormat m_DateFormat;
  
  	/** The attribute's index. */
  	private/* @ spec_public @ */int m_Index;
  
  	/** The attribute's metadata. */
  	private ProtectedProperties m_Metadata;
  
  	/** The attribute's ordering. */
  	private int m_Ordering;
  
  	/** Whether the attribute is regular. */
  	private boolean m_IsRegular;
  
  	/** Whether the attribute is averagable. */
  	private boolean m_IsAveragable;
  
  	/** Whether the attribute has a zeropoint. */
  	private boolean m_HasZeropoint;
  
  	/** The attribute's weight. */
  	private double m_Weight;
  
  	/** The attribute's lower numeric bound. */
  	private double m_LowerBound;
  
  	/** Whether the lower bound is open. */
  	private boolean m_LowerBoundIsOpen;
  
  	/** The attribute's upper numeric bound. */
  	private double m_UpperBound;
  
  	/** Whether the upper bound is open */
  	private boolean m_UpperBoundIsOpen;
  
  	/**
  	 * Constructor for a numeric attribute.
  	 * 
  	 * @param attributeName
  	 *            the name for the attribute
  	 */
  	// @ requires attributeName != null;
  	// @ ensures m_Name == attributeName;
  	public Attribute(String attributeName) {
  
  		this(attributeName, new ProtectedProperties(new Properties()));
  	}
  
  	/**
  	 * Constructor for a numeric attribute, where metadata is supplied.
  	 * 
  	 * @param attributeName
  	 *            the name for the attribute
  	 * @param metadata
  	 *            the attribute's properties
  	 */
  	// @ requires attributeName != null;
  	// @ requires metadata != null;
  	// @ ensures m_Name == attributeName;
  	public Attribute(String attributeName, ProtectedProperties metadata) {
  
  		m_Name = attributeName;
  		m_Index = -1;
  		m_Values = null;
  		m_Hashtable = null;
  		m_Header = null;
  		m_Type = REAL;
  		setMetadata(metadata);
  	}
  
  	/**
  	 * Constructor for a date attribute.
  	 * 
  	 * @param attributeName
  	 *            the name for the attribute
  	 * @param dateFormat
  	 *            a string suitable for use with SimpleDateFormatter for parsing
  	 *            dates.
  	 */
  	// @ requires attributeName != null;
  	// @ requires dateFormat != null;
  	// @ ensures m_Name == attributeName;
  	public Attribute(String attributeName, String dateFormat) {
  
  		this(attributeName, dateFormat, new ProtectedProperties(
  				new Properties()));
  	}
  
  	/**
  	 * Constructor for a date attribute, where metadata is supplied.
  	 * 
  	 * @param attributeName
  	 *            the name for the attribute
  	 * @param dateFormat
  	 *            a string suitable for use with SimpleDateFormatter for parsing
  	 *            dates.
  	 * @param metadata
  	 *            the attribute's properties
  	 */
  	// @ requires attributeName != null;
  	// @ requires dateFormat != null;
  	// @ requires metadata != null;
  	// @ ensures m_Name == attributeName;
  	public Attribute(String attributeName, String dateFormat,
  			ProtectedProperties metadata) {
  
  		m_Name = attributeName;
  		m_Index = -1;
  		m_Values = null;
  		m_Hashtable = null;
  		m_Header = null;
  		m_Type = DATE;
  		if (dateFormat != null) {
  			m_DateFormat = new SimpleDateFormat(dateFormat);
  		} else {
  			m_DateFormat = new SimpleDateFormat("yyyy-MM-dd'T'HH:mm:ss");
  		}
  		m_DateFormat.setLenient(false);
  		setMetadata(metadata);
  	}
  
  	/**
  	 * Constructor for nominal attributes and string attributes. If a null
  	 * vector of attribute values is passed to the method, the attribute is
  	 * assumed to be a string.
  	 * 
  	 * @param attributeName
  	 *            the name for the attribute
  	 * @param attributeValues
  	 *            a vector of strings denoting the attribute values. Null if the
  	 *            attribute is a string attribute.
  	 */
  	// @ requires attributeName != null;
  	// @ ensures m_Name == attributeName;
  	public Attribute(String attributeName, FastVector attributeValues) {
  
  		this(attributeName, attributeValues, new ProtectedProperties(
  				new Properties()));
  	}
  
  	/**
  	 * Constructor for nominal attributes and string attributes, where metadata
  	 * is supplied. If a null vector of attribute values is passed to the
  	 * method, the attribute is assumed to be a string.
  	 * 
  	 * @param attributeName
  	 *            the name for the attribute
  	 * @param attributeValues
  	 *            a vector of strings denoting the attribute values. Null if the
  	 *            attribute is a string attribute.
  	 * @param metadata
  	 *            the attribute's properties
  	 */
  	// @ requires attributeName != null;
  	// @ requires metadata != null;
  	/*
  	 * @ ensures m_Name == attributeName; ensures m_Index == -1; ensures
  	 * attributeValues == null && m_Type == STRING || attributeValues != null &&
  	 * m_Type == NOMINAL && m_Values.size() == attributeValues.size(); signals
  	 * (IllegalArgumentException ex) (* if duplicate strings in attributeValues
  	 * *);
  	 */
  	public Attribute(String attributeName, FastVector attributeValues,
  			ProtectedProperties metadata) {
  
  		m_Name = attributeName;
  		m_Index = -1;
  		if (attributeValues == null) {
  			m_Values = new FastVector();
  			m_Hashtable = new Hashtable();
  			m_Header = null;
  			m_Type = STRING;
  		} else {
  			m_Values = new FastVector(attributeValues.size());
  			m_Hashtable = new Hashtable(attributeValues.size());
  			m_Header = null;
  			for (int i = 0; i < attributeValues.size(); i++) {
  				Object store = attributeValues.elementAt(i);
  				if (((String) store).length() > STRING_COMPRESS_THRESHOLD) {
  					try {
  						store = new SerializedObject(attributeValues
  								.elementAt(i), true);
  					} catch (Exception ex) {
  						System.err
  								.println("Couldn't compress nominal attribute value -"
  										+ " storing uncompressed.");
  					}
  				}
  				if (m_Hashtable.containsKey(store)) {
  					throw new IllegalArgumentException("A nominal attribute ("
  							+ attributeName + ") cannot"
  							+ " have duplicate labels (" + store + ").");
  				}
  				m_Values.addElement(store);
  				m_Hashtable.put(store, new Integer(i));
  			}
  			m_Type = NOMINAL;
  		}
  		setMetadata(metadata);
  	}
  
  	/**
  	 * Constructor for relation-valued attributes.
  	 * 
  	 * @param attributeName
  	 *            the name for the attribute
  	 * @param header
  	 *            an Instances object specifying the header of the relation.
  	 */
  	public Attribute(String attributeName, Instances header) {
  
  		this(attributeName, header, new ProtectedProperties(new Properties()));
  	}
  
  	/**
  	 * Constructor for relation-valued attributes.
  	 * 
  	 * @param attributeName
  	 *            the name for the attribute
  	 * @param header
  	 *            an Instances object specifying the header of the relation.
  	 * @param metadata
  	 *            the attribute's properties
  	 */
  	public Attribute(String attributeName, Instances header,
  			ProtectedProperties metadata) {
  
  		if (header.numInstances() > 0) {
  			throw new IllegalArgumentException("Header for relation-valued "
  					+ "attribute should not contain " + "any instances");
  		}
  		m_Name = attributeName;
  		m_Index = -1;
  		m_Values = new FastVector();
  		m_Hashtable = null;
  		m_Header = header;
  		m_Type = RELATIONAL;
  		setMetadata(metadata);
  	}
  
  	/**
  	 * Produces a shallow copy of this attribute.
  	 * 
  	 * @return a copy of this attribute with the same index
  	 */
  	// @ also ensures \result instanceof Attribute;
  	public/* @ pure non_null @ */Object copy() {
  
  		Attribute copy = new Attribute(m_Name);
  
  		copy.m_Index = m_Index;
  		copy.m_Type = m_Type;
  		copy.m_Values = m_Values;
  		copy.m_Hashtable = m_Hashtable;
  		copy.m_DateFormat = m_DateFormat;
  		copy.m_Header = m_Header;
  		copy.setMetadata(m_Metadata);
  
  		return copy;
  	}
  
  	/**
  	 * Returns an enumeration of all the attribute's values if the attribute is
  	 * nominal, string, or relation-valued, null otherwise.
  	 * 
  	 * @return enumeration of all the attribute's values
  	 */
  	public final/* @ pure @ */Enumeration enumerateValues() {
  
  		if (isNominal() || isString()) {
  			final Enumeration ee = m_Values.elements();
  			return new Enumeration() {
  				public boolean hasMoreElements() {
  					return ee.hasMoreElements();
  				}
  
  				public Object nextElement() {
  					Object oo = ee.nextElement();
  					if (oo instanceof SerializedObject) {
  						return ((SerializedObject) oo).getObject();
  					} else {
  						return oo;
  					}
  				}
  			};
  		}
  		return null;
  	}
  
  	/**
  	 * Tests if given attribute is equal to this attribute.
  	 * 
  	 * @param other
  	 *            the Object to be compared to this attribute
  	 * @return true if the given attribute is equal to this attribute
  	 */
  	public final/* @ pure @ */boolean equals(Object other) {
  
  		if ((other == null) || !(other.getClass().equals(this.getClass()))) {
  			return false;
  		}
  		Attribute att = (Attribute) other;
  		if (!m_Name.equals(att.m_Name)) {
  			return false;
  		}
  		if (isNominal() && att.isNominal()) {
  			if (m_Values.size() != att.m_Values.size()) {
  				return false;
  			}
  			for (int i = 0; i < m_Values.size(); i++) {
  				if (!m_Values.elementAt(i).equals(att.m_Values.elementAt(i))) {
  					return false;
  				}
  			}
  			return true;
  		}
  		if (isRelationValued() && att.isRelationValued()) {
  			if (!m_Header.equalHeaders(att.m_Header)) {
  				return false;
  			}
  			return true;
  		}
  		return (type() == att.type());
  	}
  
  	/**
  	 * Returns the index of this attribute.
  	 * 
  	 * @return the index of this attribute
  	 */
  	// @ ensures \result == m_Index;
  	public final/* @ pure @ */int index() {
  
  		return m_Index;
  	}
  
  	/**
  	 * Returns the index of a given attribute value. (The index of the first
  	 * occurence of this value.)
  	 * 
  	 * @param value
  	 *            the value for which the index is to be returned
  	 * @return the index of the given attribute value if attribute is nominal or
  	 *         a string, -1 if it is not or the value can't be found
  	 */
  	public final int indexOfValue(String value) {
  
  		if (!isNominal() && !isString())
  			return -1;
  		Object store = value;
  		if (value.length() > STRING_COMPRESS_THRESHOLD) {
  			try {
  				store = new SerializedObject(value, true);
  			} catch (Exception ex) {
  				System.err.println("Couldn't compress string attribute value -"
  						+ " searching uncompressed.");
  			}
  		}
  		Integer val = (Integer) m_Hashtable.get(store);
  		if (val == null)
  			return -1;
  		else
  			return val.intValue();
  	}
  
  	/**
  	 * Test if the attribute is nominal.
  	 * 
  	 * @return true if the attribute is nominal
  	 */
  	// @ ensures \result <==> (m_Type == NOMINAL);
  	public final/* @ pure @ */boolean isNominal() {
  
  		return (m_Type == NOMINAL);
  	}
  
  	/**
  	 * Tests if the attribute is numeric.
  	 * 
  	 * @return true if the attribute is numeric
  	 */
  	// @ ensures \result <==> ((m_Type == NUMERIC) || (m_Type == DATE));
  	public final/* @ pure @ */boolean isReal() {
  
  		return ((m_Type == REAL) || (m_Type == DATE));
  	}
  
  	/**
  	 * Tests if the attribute is relation valued.
  	 * 
  	 * @return true if the attribute is relation valued
  	 */
  	// @ ensures \result <==> (m_Type == RELATIONAL);
  	public final/* @ pure @ */boolean isRelationValued() {
  
  		return (m_Type == RELATIONAL);
  	}
  
  	/**
  	 * Tests if the attribute is a string.
  	 * 
  	 * @return true if the attribute is a string
  	 */
  	// @ ensures \result <==> (m_Type == STRING);
  	public final/* @ pure @ */boolean isString() {
  
  		return (m_Type == STRING);
  	}
  
  	/**
  	 * Tests if the attribute is a date type.
  	 * 
  	 * @return true if the attribute is a date type
  	 */
  	// @ ensures \result <==> (m_Type == DATE);
  	public final/* @ pure @ */boolean isDate() {
  
  		return (m_Type == DATE);
  	}
  
  	/**
  	 * Returns the attribute's name.
  	 * 
  	 * @return the attribute's name as a string
  	 */
  	// @ ensures \result == m_Name;
  	public final/* @ pure @ */String name() {
  
  		return m_Name;
  	}
  
  	/**
  	 * Returns the number of attribute values. Returns 0 for attributes that are
  	 * not either nominal, string, or relation-valued.
  	 * 
  	 * @return the number of attribute values
  	 */
  	public final/* @ pure @ */int numValues() {
  
  		if (!isNominal() && !isString() && !isRelationValued()) {
  			return 0;
  		} else {
  			return m_Values.size();
  		}
  	}
  
  	/**
  	 * Returns a description of this attribute in ARFF format. Quotes strings if
  	 * they contain whitespace characters, or if they are a question mark.
  	 * 
  	 * @return a description of this attribute as a string
  	 */
  	public final String toString() {
  
  		StringBuffer text = new StringBuffer();
  
  		text.append(ARFF_ATTRIBUTE).append(" ").append(Utils.quote(m_Name))
  				.append(" ");
  		switch (m_Type) {
  		case NOMINAL:
  			text.append('{');
  			Enumeration enu = enumerateValues();
  			while (enu.hasMoreElements()) {
  				text.append(Utils.quote((String) enu.nextElement()));
  				if (enu.hasMoreElements())
  					text.append(',');
  			}
  			text.append('}');
  			break;
  		case REAL:
  			text.append(ARFF_ATTRIBUTE_REAL);
  			break;
  		case STRING:
  			text.append(ARFF_ATTRIBUTE_STRING);
  			break;
  		case DATE:
  			text.append(ARFF_ATTRIBUTE_DATE).append(" ").append(
  					Utils.quote(m_DateFormat.toPattern()));
  			break;
  		case RELATIONAL:
  			text.append(ARFF_ATTRIBUTE_RELATIONAL).append("\n");
  			Enumeration enm = m_Header.enumerateAttributes();
  			while (enm.hasMoreElements()) {
  				text.append(enm.nextElement()).append("\n");
  			}
  			text.append(ARFF_END_SUBRELATION).append(" ").append(m_Name);
  			break;
  		default:
  			text.append("UNKNOWN");
  			break;
  		}
  		return text.toString();
  	}
  
  	/**
  	 * Returns the attribute's type as an integer.
  	 * 
  	 * @return the attribute's type.
  	 */
  	// @ ensures \result == m_Type;
  	public final/* @ pure @ */int type() {
  
  		return m_Type;
  	}
  
  	/**
  	 * Returns a value of a nominal or string attribute. Returns an empty string
  	 * if the attribute is neither a string nor a nominal attribute.
  	 * 
  	 * @param valIndex
  	 *            the value's index
  	 * @return the attribute's value as a string
  	 */
  	public final/* @ non_null pure @ */String value(int valIndex) {
  
  		if (!isNominal() && !isString()) {
  			return "";
  		} else {
  			Object val = m_Values.elementAt(valIndex);
  			// //// If we're storing strings compressed, uncompress it.
  			if (val instanceof SerializedObject) {
  				val = ((SerializedObject) val).getObject();
  			}
  			return (String) val;
  		}
  	}
  
  	/**
  	 * Returns the header info for a relation-valued attribute, null if the
  	 * attribute is not relation-valued.
  	 *
  	 * @return the attribute's value as an Instances object
  	 */
  	public final/* @ non_null pure @ */Instances relation() {
  
  		if (!isRelationValued()) {
  			return null;
  		} else {
  			return m_Header;
  		}
  	}
  
  	/**
  	 * Returns a value of a relation-valued attribute. Returns null if the
  	 * attribute is not relation-valued.
  	 * 
  	 * @param valIndex
  	 *            the value's index
  	 * @return the attribute's value as an Instances object
  	 */
  	public final/* @ non_null pure @ */Instances relation(int valIndex) {
  
  		if (!isRelationValued()) {
  			return null;
  		} else {
  			return (Instances) m_Values.elementAt(valIndex);
  		}
  	}
  
  	/**
  	 * Constructor for a real attribute with a particular index.
  	 * 
  	 * @param attributeName
  	 *            the name for the attribute
  	 * @param index
  	 *            the attribute's index
  	 */
  	// @ requires attributeName != null;
  	// @ requires index >= 0;
  	// @ ensures m_Name == attributeName;
  	// @ ensures m_Index == index;
  	Attribute(String attributeName, int index) {
  
  		this(attributeName);
  		m_Index = index;
  	}
  
  	/**
  	 * Constructor for date attributes with a particular index.
  	 * 
  	 * @param attributeName
  	 *            the name for the attribute
  	 * @param dateFormat
  	 *            a string suitable for use with SimpleDateFormatter for parsing
  	 *            dates. Null for a default format string.
  	 * @param index
  	 *            the attribute's index
  	 */
  	// @ requires attributeName != null;
  	// @ requires index >= 0;
  	// @ ensures m_Name == attributeName;
  	// @ ensures m_Index == index;
  	Attribute(String attributeName, String dateFormat, int index) {
  
  		this(attributeName, dateFormat);
  		m_Index = index;
  	}
  
  	/**
  	 * Constructor for nominal attributes and string attributes with a
  	 * particular index. If a null vector of attribute values is passed to the
  	 * method, the attribute is assumed to be a string.
  	 * 
  	 * @param attributeName
  	 *            the name for the attribute
  	 * @param attributeValues
  	 *            a vector of strings denoting the attribute values. Null if the
  	 *            attribute is a string attribute.
  	 * @param index
  	 *            the attribute's index
  	 */
  	// @ requires attributeName != null;
  	// @ requires index >= 0;
  	// @ ensures m_Name == attributeName;
  	// @ ensures m_Index == index;
  	Attribute(String attributeName, FastVector attributeValues, int index) {
  
  		this(attributeName, attributeValues);
  		m_Index = index;
  	}
  
  	/**
  	 * Constructor for a relation-valued attribute with a particular index.
  	 * 
  	 * @param attributeName
  	 *            the name for the attribute
  	 * @param header
  	 *            the header information for this attribute
  	 * @param index
  	 *            the attribute's index
  	 */
  	// @ requires attributeName != null;
  	// @ requires index >= 0;
  	// @ ensures m_Name == attributeName;
  	// @ ensures m_Index == index;
  	Attribute(String attributeName, Instances header, int index) {
  
  		this(attributeName, header);
  		m_Index = index;
  	}
  
  	/**
  	 * Adds a string value to the list of valid strings for attributes of type
  	 * STRING and returns the index of the string.
  	 * 
  	 * @param value
  	 *            The string value to add
  	 * @return the index assigned to the string, or -1 if the attribute is not
  	 *         of type Attribute.STRING
  	 */
  	/*
  	 * @ requires value != null; ensures isString() && 0 <= \result && \result <
  	 * m_Values.size() || ! isString() && \result == -1;
  	 */
  	public int addStringValue(String value) {
  
  		if (!isString()) {
  			return -1;
  		}
  		Object store = value;
  
  		if (value.length() > STRING_COMPRESS_THRESHOLD) {
  			try {
  				store = new SerializedObject(value, true);
  			} catch (Exception ex) {
  				System.err.println("Couldn't compress string attribute value -"
  						+ " storing uncompressed.");
  			}
  		}
  		Integer index = (Integer) m_Hashtable.get(store);
  		if (index != null) {
  			return index.intValue();
  		} else {
  			int intIndex = m_Values.size();
  			m_Values.addElement(store);
  			m_Hashtable.put(store, new Integer(intIndex));
  			return intIndex;
  		}
  	}
  
  	/**
  	 * Adds a string value to the list of valid strings for attributes of type
  	 * STRING and returns the index of the string. This method is more efficient
  	 * than addStringValue(String) for long strings.
  	 * 
  	 * @param src
  	 *            The Attribute containing the string value to add.
  	 * @param index
  	 *            index the index of the string value in the source attribute.
  	 * @return the index assigned to the string, or -1 if the attribute is not
  	 *         of type Attribute.STRING
  	 */
  	/*
  	 * @ requires src != null; requires 0 <= index && index <
  	 * src.m_Values.size(); ensures isString() && 0 <= \result && \result <
  	 * m_Values.size() || ! isString() && \result == -1;
  	 */
  	public int addStringValue(Attribute src, int index) {
  
  		if (!isString()) {
  			return -1;
  		}
  		Object store = src.m_Values.elementAt(index);
  		Integer oldIndex = (Integer) m_Hashtable.get(store);
  		if (oldIndex != null) {
  			return oldIndex.intValue();
  		} else {
  			int intIndex = m_Values.size();
  			m_Values.addElement(store);
  			m_Hashtable.put(store, new Integer(intIndex));
  			return intIndex;
  		}
  	}
  
  	/**
  	 * Adds a relation to a relation-valued attribute.
  	 * 
  	 * @param value
  	 *            The value to add
  	 * @return the index assigned to the value, or -1 if the attribute is not of
  	 *         type Attribute.RELATIONAL
  	 */
  	public int addRelation(Instances value) {
  
  		if (!isRelationValued()) {
  			return -1;
  		}
  		if (!m_Header.equalHeaders(value)) {
  			throw new IllegalArgumentException("Incompatible value for "
  					+ "relation-valued attribute.");
  		}
  		int intIndex = m_Values.size();
  		m_Values.addElement(value);
  		return intIndex;
  	}
  
  	/**
  	 * Adds an attribute value. Creates a fresh list of attribute values before
  	 * adding it.
  	 * 
  	 * @param value
  	 *            the attribute value
  	 */
  	final void addValue(String value) {
  
  		m_Values = (FastVector) m_Values.copy();
  		m_Hashtable = (Hashtable) m_Hashtable.clone();
  		forceAddValue(value);
  	}
  
  	/**
  	 * Produces a shallow copy of this attribute with a new name.
  	 * 
  	 * @param newName
  	 *            the name of the new attribute
  	 * @return a copy of this attribute with the same index
  	 */
  	// @ requires newName != null;
  	// @ ensures \result.m_Name == newName;
  	// @ ensures \result.m_Index == m_Index;
  	// @ ensures \result.m_Type == m_Type;
  	final/* @ pure non_null @ */Attribute copy(String newName) {
  
  		Attribute copy = new Attribute(newName);
  
  		copy.m_Index = m_Index;
  		copy.m_DateFormat = m_DateFormat;
  		copy.m_Type = m_Type;
  		copy.m_Values = m_Values;
  		copy.m_Hashtable = m_Hashtable;
  		copy.m_Header = m_Header;
  		copy.setMetadata(m_Metadata);
  
  		return copy;
  	}
  
  	/**
  	 * Removes a value of a nominal, string, or relation-valued attribute.
  	 * Creates a fresh list of attribute values before removing it.
  	 * 
  	 * @param index
  	 *            the value's index
  	 * @exception IllegalArgumentException
  	 *                if the attribute is not of the correct type
  	 */
  	// @ requires isNominal() || isString() || isRelationValued();
  	// @ requires 0 <= index && index < m_Values.size();
  	final void delete(int index) {
  
  		if (!isNominal() && !isString() && !isRelationValued())
  			throw new IllegalArgumentException("Can only remove value of "
  					+ "nominal, string or relation-" + " valued attribute!");
  		else {
  			m_Values = (FastVector) m_Values.copy();
  			m_Values.removeElementAt(index);
  			if (!isRelationValued()) {
  				Hashtable hash = new Hashtable(m_Hashtable.size());
  				Enumeration enu = m_Hashtable.keys();
  				while (enu.hasMoreElements()) {
  					Object string = enu.nextElement();
  					Integer valIndexObject = (Integer) m_Hashtable.get(string);
  					int valIndex = valIndexObject.intValue();
  					if (valIndex > index) {
  						hash.put(string, new Integer(valIndex - 1));
  					} else if (valIndex < index) {
  						hash.put(string, valIndexObject);
  					}
  				}
  				m_Hashtable = hash;
  			}
  		}
  	}
  
  	/**
  	 * Adds an attribute value.
  	 * 
  	 * @param value
  	 *            the attribute value
  	 */
  	// @ requires value != null;
  	// @ ensures m_Values.size() == \old(m_Values.size()) + 1;
  	final void forceAddValue(String value) {
  
  		Object store = value;
  		if (value.length() > STRING_COMPRESS_THRESHOLD) {
  			try {
  				store = new SerializedObject(value, true);
  			} catch (Exception ex) {
  				System.err.println("Couldn't compress string attribute value -"
  						+ " storing uncompressed.");
  			}
  		}
  		m_Values.addElement(store);
  		m_Hashtable.put(store, new Integer(m_Values.size() - 1));
  	}
  
  	/**
  	 * Sets the index of this attribute.
  	 * 
  	 * @param the
  	 *            index of this attribute
  	 */
  	// @ requires 0 <= index;
  	// @ assignable m_Index;
  	// @ ensures m_Index == index;
  	final void setIndex(int index) {
  
  		m_Index = index;
  	}
  
  	/**
  	 * Sets a value of a nominal attribute or string attribute. Creates a fresh
  	 * list of attribute values before it is set.
  	 * 
  	 * @param index
  	 *            the value's index
  	 * @param string
  	 *            the value
  	 * @exception IllegalArgumentException
  	 *                if the attribute is not nominal or string.
  	 */
  	// @ requires string != null;
  	// @ requires isNominal() || isString();
  	// @ requires 0 <= index && index < m_Values.size();
  	final void setValue(int index, String string) {
  
  		switch (m_Type) {
  		case NOMINAL:
  		case STRING:
  			m_Values = (FastVector) m_Values.copy();
  			m_Hashtable = (Hashtable) m_Hashtable.clone();
  			Object store = string;
  