001: // @(#)$Id: JMLObjectValuePair.java 1.1 Mon, 02 May 2005 14:31:03 +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 JMLObjectToValueRelation} and {@link JMLObjectToValueMap}.
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 $
030: * @author Gary T. Leavens
031: * @author Clyde Ruby
032: * @see JMLObjectToValueRelation
033: * @see JMLObjectToValueMap
034: */
035: //-@ immutable
036: public/*@ pure @*/class JMLObjectValuePair 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: /*@
049: @ ensures dv != null && rv != null;
050: @ signals (NullPointerException) dv == null || rv == null;
051: @*/
052: public JMLObjectValuePair(/*@ non_null @*/Object dv,
053: /*@ non_null @*/JMLType rv) throws NullPointerException {
054: if (dv == null) {
055: throw new NullPointerException("Attempt to create a"
056: + " JMLObjectValuePair with null" + " key");
057: }
058: if (rv == null) {
059: throw new NullPointerException("Attempt to create a"
060: + " JMLObjectValuePair with null" + " value");
061: }
062: key = dv;
063: value = (JMLType) rv.clone();
064: }
065:
066: public Object clone() {
067: return new JMLObjectValuePair(key, value);
068: }
069:
070: /*@ public normal_behavior
071: @ ensures \result == (key == dv);
072: @*/
073: public boolean keyEquals(Object dv) {
074: return key == dv;
075: }
076:
077: /*@ public normal_behavior
078: @ ensures \result == (value.equals(rv));
079: @*/
080: public boolean valueEquals(JMLType rv) {
081: return value.equals(rv);
082: }
083:
084: /*@ also
085: @ public normal_behavior
086: @ requires obj != null && obj instanceof JMLObjectValuePair;
087: @ ensures \result ==
088: @ ( ((JMLObjectValuePair)obj).key == key
089: @ && ((JMLObjectValuePair)obj).value.equals(value) );
090: @ also
091: @ public normal_behavior
092: @ requires obj == null || !(obj instanceof JMLObjectValuePair);
093: @ ensures !\result;
094: @*/
095: public boolean equals(Object obj) {
096: if (obj != null && obj instanceof JMLObjectValuePair) {
097: JMLObjectValuePair pair = (JMLObjectValuePair) obj;
098: return pair.key == key && pair.value.equals(value);
099: } else {
100: return false;
101: }
102: }
103:
104: public int hashCode() {
105: return key.hashCode() + value.hashCode();
106: }
107:
108: public String toString() {
109: return (new String("(") + key + new String(", ") + value + new String(
110: ")"));
111: }
112: };
|