001: // @(#)$Id: JMLValueToValueRelationImageEnumerator.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 and their relational images. This
026: * enumerator returns pairs of type {@link JMLValueValuePair},
027: * each of which has a "key" field of type {@link JMLType} and a
028: * "value" field of type {@link JMLValueSet}s containing {@link
029: * JMLType}.
030: *
031: * @version $Revision: 1.2 $
032: * @author Gary T. Leavens
033: * @see JMLEnumeration
034: * @see JMLValueType
035: * @see JMLValueToValueRelationEnumerator
036: * @see JMLValueToValueRelation
037: * @see JMLValueToValueMap
038: * @see JMLEnumerationToIterator
039: * @see JMLValueSet
040: */
041: //-@ immutable
042: public class JMLValueToValueRelationImageEnumerator implements
043: JMLEnumeration, JMLValueType {
044:
045: //@ public model JMLValueSet uniteratedImagePairs; in objectState;
046:
047: /** An enumerator for the image pairs in this relation.
048: */
049: protected/*@ non_null @*/JMLValueSetEnumerator pairEnum;
050:
051: //@ in uniteratedImagePairs;
052:
053: /*@ protected represents uniteratedImagePairs <- abstractValue();
054: @*/
055:
056: /*@ protected
057: @ invariant moreElements <==> pairEnum.moreElements;
058: @*/
059:
060: //@ public invariant elementType == \type(JMLValueValuePair);
061: //@ public invariant !returnsNull;
062: /** Initialize this with the given relation.
063: */
064: /*@ normal_behavior
065: @ requires rel != null;
066: @ assignable uniteratedImagePairs;
067: @ assignable moreElements, elementType, returnsNull, owner;
068: @ ensures uniteratedImagePairs.equals(rel.imagePairSet());
069: @ ensures owner == null;
070: @*/
071: JMLValueToValueRelationImageEnumerator(/*@ non_null @*/
072: JMLValueToValueRelation rel) {
073: pairEnum = rel.imagePairSet_.elements();
074: }
075:
076: /*@ normal_behavior
077: @ requires pEnum != null;
078: @ assignable uniteratedImagePairs;
079: @ assignable moreElements, elementType, returnsNull, owner;
080: @ ensures owner == null;
081: @*/
082: protected JMLValueToValueRelationImageEnumerator(/*@ non_null @*/
083: JMLValueSetEnumerator pEnum) {
084: pairEnum = (JMLValueSetEnumerator) pEnum.clone();
085: }
086:
087: /** Tells whether this enumerator has more uniterated elements.
088: * @see #nextElement
089: * @see #nextImagePair
090: */
091: /*@ also
092: @ public normal_behavior
093: @ ensures \result == !uniteratedImagePairs.isEmpty();
094: @*/
095: public boolean hasMoreElements() {
096: return pairEnum.hasMoreElements();
097: }
098:
099: /** Return the next image pair in this, if there is one.
100: * @exception JMLNoSuchElementException when this is empty.
101: * @see #hasMoreElements
102: * @see #nextImagePair
103: */
104: /*@ also
105: @ public normal_behavior
106: @ requires !uniteratedImagePairs.isEmpty();
107: @ assignable uniteratedImagePairs;
108: @ ensures \old(uniteratedImagePairs).has((JMLType)\result)
109: @ && uniteratedImagePairs
110: @ .equals(\old(uniteratedImagePairs).remove((JMLType)\result));
111: @ also
112: @ public exceptional_behavior
113: @ requires uniteratedImagePairs.isEmpty();
114: @ assignable \nothing;
115: @ signals (JMLNoSuchElementException);
116: @*/
117: public Object nextElement() throws JMLNoSuchElementException {
118: if (pairEnum.hasMoreElements()) {
119: Object o = pairEnum.nextElement();
120: //@ assume o != null && \typeof(o) == elementType;
121: return o;
122: } else {
123: throw new JMLNoSuchElementException();
124: }
125: }
126:
127: /** Return the next image pair in this, if there is one.
128: * @exception JMLNoSuchElementException when this is empty.
129: * @see #hasMoreElements
130: * @see #nextElement
131: */
132: /*@ public normal_behavior
133: @ requires !uniteratedImagePairs.isEmpty();
134: @ assignable uniteratedImagePairs, moreElements;
135: @ ensures \old(uniteratedImagePairs).has(\result)
136: @ && uniteratedImagePairs.equals(
137: @ \old(uniteratedImagePairs).remove(\result));
138: @ also
139: @ public exceptional_behavior
140: @ requires uniteratedImagePairs.isEmpty();
141: @ assignable \nothing;
142: @ signals (JMLNoSuchElementException);
143: @
144: @ also
145: @ modifies uniteratedImagePairs;
146: @ modifies moreElements;
147: @ ensures \old(moreElements);
148: @ signals (JMLNoSuchElementException) \old(!moreElements);
149: @*/
150: public/*@ non_null @*/JMLValueValuePair nextImagePair()
151: throws JMLNoSuchElementException {
152: Object p = nextElement();
153: JMLValueValuePair aPair = (JMLValueValuePair) p;
154: return aPair;
155: }
156:
157: /** Return a clone of this enumerator.
158: */
159: public Object clone() {
160: return new JMLValueToValueRelationImageEnumerator(pairEnum);
161: }
162:
163: /** Return true just when this enumerator has the same state as
164: * the given argument.
165: */
166: public boolean equals(Object oth) {
167: if (oth == null
168: || !(oth instanceof JMLValueToValueRelationImageEnumerator)) {
169: return false;
170: } else {
171: JMLValueToValueRelationImageEnumerator js = (JMLValueToValueRelationImageEnumerator) oth;
172: return abstractValue().equals(js.abstractValue());
173: }
174: }
175:
176: /** Return a hash code for this enumerator.
177: */
178: public int hashCode() {
179: return abstractValue().hashCode();
180: }
181:
182: /** Return the set of uniterated pairs from this enumerator.
183: */
184: protected/*@ spec_public pure @*//*@ non_null @*/
185: JMLValueSet abstractValue() {
186: JMLValueSet ret = new JMLValueSet();
187: JMLValueToValueRelationImageEnumerator enum2 = (JMLValueToValueRelationImageEnumerator) clone();
188: while (enum2.hasMoreElements()) {
189: JMLValueValuePair aPair = enum2.nextImagePair();
190: ret = ret.insert(aPair);
191: }
192: return ret;
193: }
194: }
|