001: // @(#)$Id: JMLEqualsObjectPair.java 1.2 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 Object}, used in the types
024: * {@link JMLEqualsToObjectRelation} and {@link JMLEqualsToObjectMap}.
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.2 $
030: * @author Gary T. Leavens
031: * @author Clyde Ruby
032: * @see JMLEqualsToObjectRelation
033: * @see JMLEqualsToObjectMap
034: */
035: //-@ immutable
036: public/*@ pure @*/class JMLEqualsObjectPair 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 @*/Object value;
045:
046: //@ public invariant owner == null;
047:
048: /*@ public model_program {
049: @ assume dv != null && rv != null;
050: @ set owner = null;
051: @ key = dv;
052: @ value = rv;
053: @ }
054: @ also
055: @ ensures dv != null && rv != null;
056: @ signals (NullPointerException) dv == null || rv == null;
057: @*/
058: /** Initialize the key and value of this pair.
059: */
060: public JMLEqualsObjectPair(/*@ non_null @*/Object dv,
061: /*@ non_null @*/Object rv) throws NullPointerException {
062: if (dv == null) {
063: throw new NullPointerException("Attempt to create a"
064: + " JMLEqualsObjectPair with null" + " key");
065: }
066: if (rv == null) {
067: throw new NullPointerException("Attempt to create a"
068: + " JMLEqualsObjectPair with null" + " value");
069: }
070: key = dv;
071: value = rv;
072: }
073:
074: // inherit javadoc comment
075: /*@ also
076: @ public model_program {
077: @ return new JMLEqualsObjectPair(key, value);
078: @ }
079: @*/
080: public Object clone() {
081: return new JMLEqualsObjectPair(key, value);
082: }
083:
084: /** Tell whether this object's key is equal to the given key.
085: * @see #equals
086: */
087: /*@ public normal_behavior
088: @ ensures \result == (key.equals(dv));
089: @*/
090: public boolean keyEquals(Object dv) {
091: return key.equals(dv);
092: }
093:
094: /** Tell whether this object's key is equal to the given key.
095: * @see #equals
096: */
097: /*@ public normal_behavior
098: @ ensures \result == (value == rv);
099: @*/
100: public boolean valueEquals(Object rv) {
101: return value == rv;
102: }
103:
104: /** Test whether this object's value is equal to the given argument.
105: * @see #keyEquals
106: */
107: /*@ also
108: @ public normal_behavior
109: @ requires obj != null && obj instanceof JMLEqualsObjectPair;
110: @ ensures \result ==
111: @ ( ((JMLEqualsObjectPair)obj).key.equals(key)
112: @ && ((JMLEqualsObjectPair)obj).value == value );
113: @ also
114: @ public normal_behavior
115: @ requires obj == null || !(obj instanceof JMLEqualsObjectPair);
116: @ ensures !\result;
117: @*/
118: public boolean equals(Object obj) {
119: if (obj != null && obj instanceof JMLEqualsObjectPair) {
120: JMLEqualsObjectPair pair = (JMLEqualsObjectPair) obj;
121: return pair.key.equals(key) && pair.value == value;
122: } else {
123: return false;
124: }
125: }
126:
127: /** Return a hash code for this object.
128: */
129: public int hashCode() {
130: return key.hashCode() + value.hashCode();
131: }
132:
133: /** Return a string representation of this object.
134: */
135: public String toString() {
136: return (new String("(") + key + new String(", ") + value + new String(
137: ")"));
138: }
139: };
|