001: // @(#)$Id: JMLValueToEqualsRelationImageEnumerator.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 JMLEqualsSet}s containing {@link
029: * Object}.
030: *
031: * @version $Revision: 1.2 $
032: * @author Gary T. Leavens
033: * @see JMLEnumeration
034: * @see JMLValueType
035: * @see JMLValueToEqualsRelationEnumerator
036: * @see JMLValueToEqualsRelation
037: * @see JMLValueToEqualsMap
038: * @see JMLEnumerationToIterator
039: * @see JMLValueSet
040: */
041: //-@ immutable
042: public class JMLValueToEqualsRelationImageEnumerator 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: JMLValueToEqualsRelationImageEnumerator(/*@ non_null @*/
072: JMLValueToEqualsRelation 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 JMLValueToEqualsRelationImageEnumerator(/*@ 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: return o;
121: } else {
122: throw new JMLNoSuchElementException();
123: }
124: }
125:
126: /** Return the next image pair in this, if there is one.
127: * @exception JMLNoSuchElementException when this is empty.
128: * @see #hasMoreElements
129: * @see #nextElement
130: */
131: /*@ public normal_behavior
132: @ requires !uniteratedImagePairs.isEmpty();
133: @ assignable uniteratedImagePairs, moreElements;
134: @ ensures \old(uniteratedImagePairs).has(\result)
135: @ && uniteratedImagePairs.equals(
136: @ \old(uniteratedImagePairs).remove(\result));
137: @ also
138: @ public exceptional_behavior
139: @ requires uniteratedImagePairs.isEmpty();
140: @ assignable \nothing;
141: @ signals (JMLNoSuchElementException);
142: @
143: @ also
144: @ modifies uniteratedImagePairs;
145: @ modifies moreElements;
146: @ ensures \old(moreElements);
147: @ signals (JMLNoSuchElementException) \old(!moreElements);
148: @*/
149: public/*@ non_null @*/JMLValueValuePair nextImagePair()
150: throws JMLNoSuchElementException {
151: Object p = nextElement();
152: JMLValueValuePair aPair = (JMLValueValuePair) p;
153: return aPair;
154: }
155:
156: /** Return a clone of this enumerator.
157: */
158: public Object clone() {
159: return new JMLValueToEqualsRelationImageEnumerator(pairEnum);
160: }
161:
162: /** Return true just when this enumerator has the same state as
163: * the given argument.
164: */
165: public boolean equals(Object oth) {
166: if (oth == null
167: || !(oth instanceof JMLValueToEqualsRelationImageEnumerator)) {
168: return false;
169: } else {
170: JMLValueToEqualsRelationImageEnumerator js = (JMLValueToEqualsRelationImageEnumerator) oth;
171: return abstractValue().equals(js.abstractValue());
172: }
173: }
174:
175: /** Return a hash code for this enumerator.
176: */
177: public int hashCode() {
178: return abstractValue().hashCode();
179: }
180:
181: /** Return the set of uniterated pairs from this enumerator.
182: */
183: protected/*@ spec_public pure @*//*@ non_null @*/
184: JMLValueSet abstractValue() {
185: JMLValueSet ret = new JMLValueSet();
186: JMLValueToEqualsRelationImageEnumerator enum2 = (JMLValueToEqualsRelationImageEnumerator) clone();
187: while (enum2.hasMoreElements()) {
188: JMLValueValuePair aPair = enum2.nextImagePair();
189: ret = ret.insert(aPair);
190: }
191: return ret;
192: }
193: }
|