001: // @(#)$Id: JMLObjectObjectPair.java 1.3 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 JMLObjectToObjectRelation} and {@link JMLObjectToObjectMap}.
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.3 $
030: * @author Gary T. Leavens
031: * @author Clyde Ruby
032: * @see JMLObjectToObjectRelation
033: * @see JMLObjectToObjectMap
034: */
035: //-@ immutable
036: public/*@ pure @*/class JMLObjectObjectPair 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 behavior
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 JMLObjectObjectPair(/*@ non_null @*/Object dv,
055: /*@ non_null @*/Object rv) throws NullPointerException {
056: if (dv == null) {
057: throw new NullPointerException("Attempt to create a"
058: + " JMLObjectObjectPair with null" + " key");
059: }
060: if (rv == null) {
061: throw new NullPointerException("Attempt to create a"
062: + " JMLObjectObjectPair with null" + " value");
063: }
064: key = dv;
065: value = rv;
066: }
067:
068: // inherit javadoc comment
069: /*@ also
070: @ public model_program {
071: @ return new JMLObjectObjectPair(key, value);
072: @ }
073: @*/
074: public Object clone() {
075: return new JMLObjectObjectPair(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 == dv);
083: @*/
084: public boolean keyEquals(Object dv) {
085: return key == 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 == rv);
093: @*/
094: public boolean valueEquals(Object rv) {
095: return value == 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 JMLObjectObjectPair;
104: @ ensures \result ==
105: @ ( ((JMLObjectObjectPair)obj).key == key
106: @ && ((JMLObjectObjectPair)obj).value == value );
107: @ also
108: @ public normal_behavior
109: @ requires obj == null || !(obj instanceof JMLObjectObjectPair);
110: @ ensures !\result;
111: @*/
112: public boolean equals(Object obj) {
113: if (obj != null && obj instanceof JMLObjectObjectPair) {
114: JMLObjectObjectPair pair = (JMLObjectObjectPair) obj;
115: return pair.key == key && pair.value == 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: };
|