001: // @(#)$Id: JMLValueBagEnumerator.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: /** Enumerators for bags (i.e., multisets) of values.
026: *
027: * @version $Revision: 1.2 $
028: * @author Gary T. Leavens, with help from Albert Baker, Clyde Ruby,
029: * and others.
030: * @see JMLEnumeration
031: * @see JMLType
032: * @see JMLValueBag
033: * @see JMLEnumerationToIterator
034: */
035: //-@ immutable
036: public class JMLValueBagEnumerator implements JMLEnumeration,
037: JMLValueType {
038: /** The elements that have not yet been returned by nextElement.
039: */
040: //@ public model JMLValueBag uniteratedElems; in objectState;
041: /** The bag underlying this enumerator.
042: */
043: protected/*@ non_null @*/JMLValueBag currentBag;
044: //@ in uniteratedElems;
045:
046: /** The remaining count of repetitions that the current entry
047: * should be returned.
048: */
049: protected int currentCount;
050: //@ in uniteratedElems;
051:
052: /** The current entry.
053: */
054: protected JMLType currEntry;
055:
056: //@ in uniteratedElems;
057:
058: /*@ protected represents
059: @ uniteratedElems <- currentBag.removeAll(currEntry)
060: @ .insert(currEntry, currentCount);
061: @*/
062:
063: //@ protected invariant currentCount >= 0;
064: /*@ protected invariant currentCount > 0
065: @ ==> (* currEntry is holds an element, which may be null *);
066: @ protected invariant !currentBag.isEmpty()
067: @ ==> currentBag.has(currEntry)
068: @ && currentCount <= currentBag.count(currEntry);
069: @*/
070:
071: //@ protected invariant currentCount > 0 ==> moreElements;
072: /*@ protected invariant moreElements <==>
073: @ (currentCount > 0 || !currentBag.isEmpty());
074: @*/
075:
076: //@ public invariant elementType <: \type(JMLType);
077: /*@ public invariant
078: @ !uniteratedElems.isEmpty()
079: @ ==> uniteratedElems.elementType <: elementType;
080: @*/
081:
082: //@ public constraint returnsNull == \old(returnsNull);
083: /*@ public invariant
084: @ !returnsNull
085: @ ==> uniteratedElems.isEmpty() || !uniteratedElems.containsNull;
086: @*/
087:
088: /** Initialize this with the given bag.
089: */
090: /*@ normal_behavior
091: @ requires b != null;
092: @ assignable uniteratedElems;
093: @ assignable moreElements, elementType, returnsNull, owner;
094: @ ensures uniteratedElems.equals(b);
095: @ ensures owner == null;
096: @ ensures elementType == b.elementType;
097: @ ensures returnsNull == b.containsNull;
098: @*/
099: JMLValueBagEnumerator(/*@ non_null @*/JMLValueBag b) {
100: currentBag = b;
101: if (!currentBag.isEmpty()) {
102: currEntry = currentBag.choose();
103: currentCount = currentBag.count(currEntry);
104: } else {
105: currentCount = 0;
106: }
107: }
108:
109: /** Tells whether this enumerator has more uniterated elements.
110: */
111: /*@ also
112: @ public normal_behavior
113: @ ensures \result == !uniteratedElems.isEmpty();
114: @ ensures_redundantly \result == moreElements;
115: @ ensures_redundantly \result <==> !uniteratedElems.isEmpty();
116: @ ensures_redundantly \result <=!=> uniteratedElems.isEmpty();
117: @ ensures_redundantly \result != uniteratedElems.isEmpty();
118: @*/
119: public/*@ pure @*/boolean hasMoreElements() {
120: boolean ret = currentCount > 0 || !currentBag.isEmpty();
121: return ret;
122: }
123:
124: /** Return the next element in this, if there is one.
125: * @exception JMLNoSuchElementException when this is empty.
126: */
127: /*@ also
128: @ public normal_behavior
129: @ requires hasMoreElements();
130: @ assignable uniteratedElems, moreElements;
131: @ ensures \old(uniteratedElems).has((JMLType) \result)
132: @ && uniteratedElems.equals(\old(uniteratedElems)
133: @ .remove((JMLType) \result));
134: @ also
135: @ public exceptional_behavior
136: @ requires !hasMoreElements();
137: @ assignable \nothing;
138: @ signals (JMLNoSuchElementException);
139: @*/
140: public Object nextElement() throws JMLNoSuchElementException {
141: if (currentCount > 0 || !currentBag.isEmpty()) {
142: JMLType retValue;
143: if (currEntry == null) {
144: retValue = null;
145: } else {
146: retValue = (JMLType) currEntry.clone();
147: }
148: currentCount--;
149: if (currentCount <= 0) {
150: // The following gratiutious assignment is added because
151: // ESC/Java imagines that a callback may happen...
152: currentCount = 0;
153: currentBag = currentBag.removeAll(currEntry);
154: if (currentBag.isEmpty()) {
155: currentCount = 0;
156: } else {
157: currEntry = currentBag.choose();
158: currentCount = currentBag.count(currEntry);
159: }
160: }
161: return retValue;
162: } else {
163: throw new JMLNoSuchElementException(
164: "Tried to .nextElement() " + "with JMLValueBag "
165: + "Enumerator `off the end'");
166: }
167: }
168:
169: /** Return a clone of this enumerator.
170: */
171: public Object clone() {
172: return new JMLValueBagEnumerator(abstractValue());
173: }
174:
175: /** Return the abstract value of this bag enumerator.
176: */
177: protected/*@ pure non_null @*/JMLValueBag abstractValue() {
178: JMLValueBag absVal = currentBag;
179: if (currentCount > 0) {
180: absVal = currentBag.removeAll(currEntry).insert(currEntry,
181: currentCount);
182: }
183: return absVal;
184: }
185:
186: /** Return true just when this enumerator has the same state as
187: * the given argument..
188: */
189: public boolean equals(Object oth) {
190: if (oth == null || !(oth instanceof JMLValueBagEnumerator)) {
191: return false;
192: } else {
193: JMLValueBagEnumerator jb = (JMLValueBagEnumerator) oth;
194: return this .abstractValue().equals(jb.abstractValue());
195: }
196: }
197:
198: /** Return a hash code for this enumerator.
199: */
200: public int hashCode() {
201: return abstractValue().hashCode();
202: }
203: }
|