001: // @(#)$Id: JMLEqualsValuePair.java 1.1.1.1 Mon, 09 May 2005 15:27:50 +0200 engelc $
002:
003: // Copyright (C) 1998, 1999 Iowa State University
004:
005: // This file is part of JML
006:
007: // JML is free software; you can redistribute it and/or modify
008: // it under the terms of the GNU General Public License as published by
009: // the Free Software Foundation; either version 2, or (at your option)
010: // any later version.
011:
012: // JML is distributed in the hope that it will be useful,
013: // but WITHOUT ANY WARRANTY; without even the implied warranty of
014: // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
015: // GNU General Public License for more details.
016:
017: // You should have received a copy of the GNU General Public License
018: // along with JML; see the file COPYING. If not, write to
019: // the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
020:
021: package org.jmlspecs.models;
022:
023: /** Pairs of {@link Object} and {@link JMLType}, used in the types
024: * {@link JMLEqualsToValueRelation} and {@link JMLEqualsToValueMap}.
025: *
026: * <p> In a pair the first element is called the "key" and the second
027: * the "value". Both the key and the value in a pair must be non-null.
028: *
029: * @version $Revision: 1.1.1.1 $
030: * @author Gary T. Leavens
031: * @author Clyde Ruby
032: * @see JMLEqualsToValueRelation
033: * @see JMLEqualsToValueMap
034: */
035: //-@ immutable
036: public/*@ pure @*/class JMLEqualsValuePair implements JMLType {
037:
038: /** The key of this pair.
039: */
040: public final/*@ non_null @*/Object key;
041:
042: /** The value of this pair.
043: */
044: public final/*@ non_null @*/JMLType value;
045:
046: //@ public invariant owner == null;
047:
048: /*@ also
049: @ ensures dv != null && rv != null;
050: @ signals (NullPointerException) dv == null || rv == null;
051: @*/
052: /** Initialize the key and value of this pair.
053: */
054: public JMLEqualsValuePair(/*@ non_null @*/Object dv,
055: /*@ non_null @*/JMLType rv) throws NullPointerException {
056: if (dv == null) {
057: throw new NullPointerException("Attempt to create a"
058: + " JMLEqualsValuePair with null" + " key");
059: }
060: if (rv == null) {
061: throw new NullPointerException("Attempt to create a"
062: + " JMLEqualsValuePair with null" + " value");
063: }
064: key = dv;
065: value = (JMLType) rv.clone();
066: }
067:
068: // inherit javadoc comment
069: /*@ also
070: @ public model_program {
071: @ return new JMLEqualsValuePair(key, value);
072: @ }
073: @*/
074: public Object clone() {
075: return new JMLEqualsValuePair(key, value);
076: }
077:
078: /** Tell whether this object's key is equal to the given key.
079: * @see #equals
080: */
081: /*@ public normal_behavior
082: @ ensures \result == (key.equals(dv));
083: @*/
084: public boolean keyEquals(Object dv) {
085: return key.equals(dv);
086: }
087:
088: /** Tell whether this object's key is equal to the given key.
089: * @see #equals
090: */
091: /*@ public normal_behavior
092: @ ensures \result == (value.equals(rv));
093: @*/
094: public boolean valueEquals(JMLType rv) {
095: return value.equals(rv);
096: }
097:
098: /** Test whether this object's value is equal to the given argument.
099: * @see #keyEquals
100: */
101: /*@ also
102: @ public normal_behavior
103: @ requires obj != null && obj instanceof JMLEqualsValuePair;
104: @ ensures \result ==
105: @ ( ((JMLEqualsValuePair)obj).key.equals(key)
106: @ && ((JMLEqualsValuePair)obj).value.equals(value) );
107: @ also
108: @ public normal_behavior
109: @ requires obj == null || !(obj instanceof JMLEqualsValuePair);
110: @ ensures !\result;
111: @*/
112: public boolean equals(Object obj) {
113: if (obj != null && obj instanceof JMLEqualsValuePair) {
114: JMLEqualsValuePair pair = (JMLEqualsValuePair) obj;
115: return pair.key.equals(key) && pair.value.equals(value);
116: } else {
117: return false;
118: }
119: }
120:
121: /** Return a hash code for this object.
122: */
123: public int hashCode() {
124: return key.hashCode() + value.hashCode();
125: }
126:
127: /** Return a string representation of this object.
128: */
129: public String toString() {
130: return (new String("(") + key + new String(", ") + value + new String(
131: ")"));
132: }
133: };
|