001: // @(#)$Id: JMLObjectToValueRelationEnumerator.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 JMLType} 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 JMLObjectToValueRelationImageEnumerator
034: * @see JMLObjectToValueRelation
035: * @see JMLObjectToValueMap
036: * @see JMLEnumerationToIterator
037: * @see JMLValueSet
038: */
039: //-@ immutable
040: public class JMLObjectToValueRelationEnumerator 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: JMLObjectToValueRelationImageEnumerator 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 @*/JMLValueSetEnumerator 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(JMLObjectValuePair);
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: JMLObjectToValueRelationEnumerator(/*@ non_null @*/
085: JMLObjectToValueRelation rel) {
086: imagePairEnum = rel.imagePairs();
087: if (imagePairEnum.hasMoreElements()) {
088: JMLObjectValuePair p = imagePairEnum.nextImagePair();
089: key = p.key;
090: imageEnum = ((JMLValueSet) p.value).elements();
091: } else {
092: key = null;
093: imageEnum = (new JMLValueSet()).elements();
094: }
095: }
096:
097: //@ requires ipEnum != null;
098: //@ requires iEnum != null;
099: //@ requires (ipEnum.moreElements || iEnum.moreElements) ==> k != null;
100: protected JMLObjectToValueRelationEnumerator(
101: JMLObjectToValueRelationImageEnumerator ipEnum,
102: JMLValueSetEnumerator iEnum, Object k) {
103: imagePairEnum = (JMLObjectToValueRelationImageEnumerator) ipEnum
104: .clone();
105: imageEnum = (JMLValueSetEnumerator) iEnum.clone();
106: key = k;
107: }
108:
109: /** Tells whether this enumerator has more uniterated elements.
110: * @see #nextElement
111: * @see #nextPair
112: */
113: /*@ also
114: @ public normal_behavior
115: @ assignable \nothing;
116: @ ensures \result == !uniteratedPairs.isEmpty();
117: @*/
118: public/*@ pure @*/boolean hasMoreElements() {
119: return (imagePairEnum.hasMoreElements() || imageEnum
120: .hasMoreElements());
121: }
122:
123: /** Return the next image pair in this, if there is one.
124: * @exception JMLNoSuchElementException when this is empty.
125: * @see #hasMoreElements
126: * @see #nextPair
127: */
128: /*@ also
129: @ public normal_behavior
130: @ requires !uniteratedPairs.isEmpty();
131: @ assignable uniteratedPairs;
132: @ ensures \old(uniteratedPairs).has((JMLType)\result)
133: @ && uniteratedPairs.
134: @ equals(\old(uniteratedPairs).remove((JMLType)\result));
135: @ also
136: @ public exceptional_behavior
137: @ requires uniteratedPairs.isEmpty();
138: @ assignable \nothing;
139: @ signals (JMLNoSuchElementException);
140: @*/
141: public Object nextElement() throws JMLNoSuchElementException {
142: if (imageEnum.hasMoreElements()) {
143: Object v = imageEnum.nextElement();
144: return new JMLObjectValuePair(key, (JMLType) v);
145: } else if (imagePairEnum.hasMoreElements()) {
146: Object p = imagePairEnum.nextElement();
147: JMLObjectValuePair imagePair = (JMLObjectValuePair) p;
148: key = imagePair.key;
149: imageEnum = ((JMLValueSet) imagePair.value).elements();
150: Object v = imageEnum.nextElement();
151: return new JMLObjectValuePair(key, (JMLType) v);
152: } else {
153: throw new JMLNoSuchElementException();
154: }
155: }
156:
157: /** Return the next pair in this, if there is one.
158: * @exception JMLNoSuchElementException when this is empty.
159: * @see #hasMoreElements
160: * @see #nextElement
161: */
162: /*@ public normal_behavior
163: @ requires !uniteratedPairs.isEmpty();
164: @ assignable uniteratedPairs, moreElements;
165: @ ensures \old(uniteratedPairs).has(\result)
166: @ && uniteratedPairs
167: @ .equals(\old(uniteratedPairs).remove(\result));
168: @ also
169: @ public exceptional_behavior
170: @ requires uniteratedPairs.isEmpty();
171: @ assignable \nothing;
172: @ signals (JMLNoSuchElementException);
173: @
174: @ also
175: @ modifies uniteratedPairs;
176: @ modifies moreElements;
177: @ ensures \old(moreElements);
178: @ signals (JMLNoSuchElementException) \old(!moreElements);
179: @*/
180: public/*@ non_null @*/JMLObjectValuePair nextPair()
181: throws JMLNoSuchElementException {
182: Object p = nextElement();
183: JMLObjectValuePair aPair = (JMLObjectValuePair) p;
184: return aPair;
185: }
186:
187: /** Return a clone of this enumerator.
188: */
189: public Object clone() {
190: return new JMLObjectToValueRelationEnumerator(imagePairEnum,
191: imageEnum, key);
192: }
193:
194: /** Return true just when this enumerator has the same state as
195: * the given argument.
196: */
197: public/*@ pure @*/boolean equals(Object oth) {
198: if (oth == null
199: || !(oth instanceof JMLObjectToValueRelationEnumerator)) {
200: return false;
201: } else {
202: JMLObjectToValueRelationEnumerator js = (JMLObjectToValueRelationEnumerator) oth;
203: return abstractValue().equals(js.abstractValue());
204: }
205: }
206:
207: /** Return a hash code for this enumerator.
208: */
209: public/*@ pure @*/int hashCode() {
210: return abstractValue().hashCode();
211: }
212:
213: /** Return the set of uniterated pairs from this enumerator.
214: */
215: protected/*@ spec_public pure @*//*@ non_null @*/
216: JMLValueSet abstractValue() {
217: JMLValueSet ret = new JMLValueSet();
218: JMLObjectToValueRelationEnumerator enum2 = (JMLObjectToValueRelationEnumerator) clone();
219: while (enum2.hasMoreElements()) {
220: JMLObjectValuePair aPair = enum2.nextPair();
221: ret = ret.insert(aPair);
222: }
223: return ret;
224: }
225: }
|