001: // @(#)$Id: JMLObjectToObjectRelationEnumerator.java 1.2 Mon, 09 May 2005 15:27:50 +0200 engelc $
002:
003: // Copyright (C) 1998, 1999, 2002 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: import java.util.Enumeration;
024:
025: /** Enumerator for pairs of keys of type {@link Object} to
026: * values of type {@link Object} that form the associations in a
027: * relation.
028: *
029: * @version $Revision: 1.2 $
030: * @author Gary T. Leavens
031: * @see JMLEnumeration
032: * @see JMLValueType
033: * @see JMLObjectToObjectRelationImageEnumerator
034: * @see JMLObjectToObjectRelation
035: * @see JMLObjectToObjectMap
036: * @see JMLEnumerationToIterator
037: * @see JMLValueSet
038: */
039: //-@ immutable
040: public class JMLObjectToObjectRelationEnumerator implements
041: JMLEnumeration, JMLValueType {
042:
043: //@ public model JMLValueSet uniteratedPairs; in objectState;
044:
045: /** An enumerator for the image pairs in this relation.
046: */
047: protected/*@ non_null @*/
048: JMLObjectToObjectRelationImageEnumerator imagePairEnum;
049: //@ in uniteratedPairs;
050:
051: /** The current key for pairs being enumerated.
052: */
053: protected Object key;
054: //@ in uniteratedPairs;
055:
056: /** An enumerator for the range elements that are related to the
057: * key that have not yet been returned.
058: */
059: protected/*@ non_null @*/JMLObjectSetEnumerator imageEnum;
060:
061: //@ in uniteratedPairs;
062:
063: /*@ protected represents uniteratedPairs <- abstractValue();
064: @*/
065:
066: /*@ protected invariant moreElements
067: @ <==> imageEnum.moreElements|| imagePairEnum.moreElements;
068: @*/
069:
070: /*@ protected invariant moreElements ==> key != null;
071: @*/
072:
073: //@ public invariant elementType == \type(JMLObjectObjectPair);
074: //@ public invariant !returnsNull;
075: /** Initialize this with the given relation.
076: */
077: /*@ normal_behavior
078: @ requires rel != null;
079: @ assignable uniteratedPairs;
080: @ assignable moreElements, elementType, returnsNull, owner;
081: @ ensures uniteratedPairs.equals(rel.theRelation);
082: @ ensures owner == null;
083: @*/
084: JMLObjectToObjectRelationEnumerator(/*@ non_null @*/
085: JMLObjectToObjectRelation rel) {
086: imagePairEnum = rel.imagePairs();
087: if (imagePairEnum.hasMoreElements()) {
088: JMLObjectValuePair p = imagePairEnum.nextImagePair();
089: key = p.key;
090: imageEnum = ((JMLObjectSet) p.value).elements();
091: } else {
092: key = null;
093: imageEnum = (new JMLObjectSet()).elements();
094: }
095: }
096:
097: /*@ requires ipEnum != null;
098: @ requires iEnum != null;
099: @ requires (ipEnum.moreElements || iEnum.moreElements) ==> k != null;
100: @*/
101: protected JMLObjectToObjectRelationEnumerator(
102: JMLObjectToObjectRelationImageEnumerator ipEnum,
103: JMLObjectSetEnumerator iEnum, Object k) {
104: imagePairEnum = (JMLObjectToObjectRelationImageEnumerator) ipEnum
105: .clone();
106: imageEnum = (JMLObjectSetEnumerator) iEnum.clone();
107: key = k;
108: }
109:
110: /** Tells whether this enumerator has more uniterated elements.
111: * @see #nextElement
112: * @see #nextPair
113: */
114: /*@ also
115: @ public normal_behavior
116: @ assignable \nothing;
117: @ ensures \result == !uniteratedPairs.isEmpty();
118: @*/
119: public/*@ pure @*/boolean hasMoreElements() {
120: return (imagePairEnum.hasMoreElements() || imageEnum
121: .hasMoreElements());
122: }
123:
124: /** Return the next image pair in this, if there is one.
125: * @exception JMLNoSuchElementException when this is empty.
126: * @see #hasMoreElements
127: * @see #nextPair
128: */
129: /*@ also
130: @ public normal_behavior
131: @ requires !uniteratedPairs.isEmpty();
132: @ assignable uniteratedPairs;
133: @ ensures \old(uniteratedPairs).has((JMLType)\result)
134: @ && uniteratedPairs.
135: @ equals(\old(uniteratedPairs).remove((JMLType)\result));
136: @ also
137: @ public exceptional_behavior
138: @ requires uniteratedPairs.isEmpty();
139: @ assignable \nothing;
140: @ signals (JMLNoSuchElementException);
141: @*/
142: public Object nextElement() throws JMLNoSuchElementException {
143: if (imageEnum.hasMoreElements()) {
144: Object v = imageEnum.nextElement();
145: return new JMLObjectObjectPair(key, (Object) v);
146: } else if (imagePairEnum.hasMoreElements()) {
147: Object p = imagePairEnum.nextElement();
148: JMLObjectValuePair imagePair = (JMLObjectValuePair) p;
149: key = imagePair.key;
150: imageEnum = ((JMLObjectSet) imagePair.value).elements();
151: Object v = imageEnum.nextElement();
152: return new JMLObjectObjectPair(key, (Object) v);
153: } else {
154: throw new JMLNoSuchElementException();
155: }
156: }
157:
158: /** Return the next pair in this, if there is one.
159: * @exception JMLNoSuchElementException when this is empty.
160: * @see #hasMoreElements
161: * @see #nextElement
162: */
163: /*@ public normal_behavior
164: @ requires !uniteratedPairs.isEmpty();
165: @ assignable uniteratedPairs, moreElements;
166: @ ensures \old(uniteratedPairs).has(\result)
167: @ && uniteratedPairs
168: @ .equals(\old(uniteratedPairs).remove(\result));
169: @ also
170: @ public exceptional_behavior
171: @ requires uniteratedPairs.isEmpty();
172: @ assignable \nothing;
173: @ signals (JMLNoSuchElementException);
174: @
175: @ also
176: @ modifies uniteratedPairs;
177: @ modifies moreElements;
178: @ ensures \old(moreElements);
179: @ signals (JMLNoSuchElementException) \old(!moreElements);
180: @*/
181: public/*@ non_null @*/JMLObjectObjectPair nextPair()
182: throws JMLNoSuchElementException {
183: Object p = nextElement();
184: JMLObjectObjectPair aPair = (JMLObjectObjectPair) p;
185: return aPair;
186: }
187:
188: /** Return a clone of this enumerator.
189: */
190: public Object clone() {
191: return new JMLObjectToObjectRelationEnumerator(imagePairEnum,
192: imageEnum, key);
193: }
194:
195: /** Return true just when this enumerator has the same state as
196: * the given argument.
197: */
198: public/*@ pure @*/boolean equals(Object oth) {
199: if (oth == null
200: || !(oth instanceof JMLObjectToObjectRelationEnumerator)) {
201: return false;
202: } else {
203: JMLObjectToObjectRelationEnumerator js = (JMLObjectToObjectRelationEnumerator) oth;
204: return abstractValue().equals(js.abstractValue());
205: }
206: }
207:
208: /** Return a hash code for this enumerator.
209: */
210: public/*@ pure @*/int hashCode() {
211: return abstractValue().hashCode();
212: }
213:
214: /** Return the set of uniterated pairs from this enumerator.
215: */
216: protected/*@ spec_public pure @*//*@ non_null @*/
217: JMLValueSet abstractValue() {
218: JMLValueSet ret = new JMLValueSet();
219: JMLObjectToObjectRelationEnumerator enum2 = (JMLObjectToObjectRelationEnumerator) clone();
220: while (enum2.hasMoreElements()) {
221: JMLObjectObjectPair aPair = enum2.nextPair();
222: ret = ret.insert(aPair);
223: }
224: return ret;
225: }
226: }
|