001: // @(#)$Id: JMLValueValuePair.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 JMLType} and {@link JMLType}, used in the types
024: * {@link JMLValueToValueRelation} and {@link JMLValueToValueMap}.
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 JMLValueToValueRelation
033: * @see JMLValueToValueMap
034: */
035: //-@ immutable
036: public/*@ pure @*/class JMLValueValuePair implements JMLType {
037:
038: /** The key of this pair.
039: */
040: public final/*@ non_null @*/JMLType key;
041:
042: /** The value of this pair.
043: */
044: public final/*@ non_null @*/JMLType value;
045:
046: //@ public invariant owner == null;
047:
048: /*@ public model_program {
049: @ assume dv != null && rv != null;
050: @ set owner = null;
051: @ key = (JMLType)dv.clone();
052: @ value = (JMLType)rv.clone();
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 JMLValueValuePair(/*@ non_null @*/JMLType dv,
061: /*@ non_null @*/JMLType rv) throws NullPointerException {
062: if (dv == null) {
063: throw new NullPointerException("Attempt to create a"
064: + " JMLValueValuePair with null" + " key");
065: }
066: if (rv == null) {
067: throw new NullPointerException("Attempt to create a"
068: + " JMLValueValuePair with null" + " value");
069: }
070: //@ assume dv != null && rv != null;
071: //@ set owner = null;
072: key = (JMLType) dv.clone();
073: value = (JMLType) rv.clone();
074: }
075:
076: // inherit javadoc comment
077: /*@ also
078: @ public model_program {
079: @ return new JMLValueValuePair(key, value);
080: @ }
081: @*/
082: public Object clone() {
083: return new JMLValueValuePair(key, value);
084: } // nowarn Post;
085:
086: /** Tell whether this object's key is equal to the given key.
087: * @see #equals
088: */
089: /*@ public normal_behavior
090: @ ensures \result == (key.equals(dv));
091: @*/
092: public boolean keyEquals(JMLType dv) {
093: return key.equals(dv);
094: }
095:
096: /** Tell whether this object's key is equal to the given key.
097: * @see #equals
098: */
099: /*@ public normal_behavior
100: @ ensures \result == (value.equals(rv));
101: @*/
102: public boolean valueEquals(JMLType rv) {
103: return value.equals(rv);
104: }
105:
106: /** Test whether this object's value is equal to the given argument.
107: * @see #keyEquals
108: */
109: /*@ also
110: @ public normal_behavior
111: @ requires obj != null && obj instanceof JMLValueValuePair;
112: @ ensures \result ==
113: @ ( ((JMLValueValuePair)obj).key.equals(key)
114: @ && ((JMLValueValuePair)obj).value.equals(value) );
115: @ also
116: @ public normal_behavior
117: @ requires obj == null || !(obj instanceof JMLValueValuePair);
118: @ ensures !\result;
119: @*/
120: public boolean equals(Object obj) {
121: if (obj != null && obj instanceof JMLValueValuePair) {
122: JMLValueValuePair pair = (JMLValueValuePair) obj;
123: return pair.key.equals(key) && pair.value.equals(value);
124: } else {
125: return false;
126: }
127: }
128:
129: /** Return a hash code for this object.
130: */
131: public int hashCode() {
132: return key.hashCode() + value.hashCode();
133: }
134:
135: /** Return a string representation of this object.
136: */
137: /*@ also
138: @ public normal_behavior
139: @ ensures (* \result is a string that starts with a '(' followed by
140: @ the strings representing key and value separated by
141: @ a comma and ends with a ')'
142: @ *);
143: @ for_example
144: @ public normal_example
145: @ requires (* key is 4 and value is 2 *);
146: @ ensures (* \result is the string "(4, 2)" *);
147: @*/
148: public String toString() {
149: return (new String("(") + key + new String(", ") + value + new String(
150: ")"));
151: }
152: };
|