001: // @(#)$Id: JMLValueSetEnumerator.java 1.1 Mon, 02 May 2005 14:31:03 +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: /** An enumerator for sets of values.
026: *
027: * @version $Revision: 1.1 $
028: * @author Gary T. Leavens, with help from Albert Baker, Clyde Ruby,
029: * and others.
030: * @see JMLEnumeration
031: * @see JMLValueType
032: * @see JMLValueSet
033: * @see JMLEnumerationToIterator
034: */
035: //-@ immutable
036: public class JMLValueSetEnumerator implements JMLEnumeration,
037: JMLValueType {
038:
039: /** The elements that have not yet been returned by nextElement.
040: */
041: //@ public model JMLValueSet uniteratedElems; in objectState;
042: //@ public invariant uniteratedElems != null;
043: /** The list representing the elements that have not yet been
044: * returned by this enumerator.
045: */
046: protected JMLListValueNode currentNode;
047:
048: //@ in uniteratedElems;
049:
050: //@ protected represents uniteratedElems <- new JMLValueSet(currentNode);
051:
052: //@ protected invariant moreElements <==> currentNode != null;
053:
054: //@ public invariant elementType <: \type(JMLType);
055:
056: /*@ public invariant
057: @ !uniteratedElems.isEmpty()
058: @ ==> uniteratedElems.elementType <: elementType;
059: @*/
060:
061: //@ public constraint returnsNull == \old(returnsNull);
062: /*@ public invariant
063: @ !returnsNull
064: @ ==> uniteratedElems.isEmpty() || !uniteratedElems.containsNull;
065: @*/
066:
067: /** Initialize this with the given set.
068: */
069: /*@ normal_behavior
070: @ requires s != null;
071: @ assignable uniteratedElems;
072: @ modifies moreElements, elementType, returnsNull, owner;
073: @ ensures uniteratedElems.equals(s);
074: @ ensures owner == null;
075: @ ensures elementType == s.elementType;
076: @ ensures returnsNull == s.containsNull;
077: @*/
078: JMLValueSetEnumerator(/*@ non_null @*/JMLValueSet s) {
079: //@ set owner = null;
080: //@ set elementType = s.elementType;
081: //@ set returnsNull = s.containsNull;
082: currentNode = s.the_list;
083: }
084:
085: /** Tells whether this enumerator has more uniterated elements.
086: */
087: /*@ also
088: @ public normal_behavior
089: @ ensures \result == !uniteratedElems.isEmpty();
090: @*/
091: public/*@ pure @*/boolean hasMoreElements() {
092: return currentNode != null;
093: }
094:
095: /** Return the next element in this, if there is one.
096: * @exception JMLNoSuchElementException when this is empty.
097: */
098: /*@ also
099: @ public normal_behavior
100: @ requires hasMoreElements();
101: @ assignable uniteratedElems, moreElements;
102: @ ensures
103: @ (\result == null
104: @ ==> \old(uniteratedElems).has(null)
105: @ && uniteratedElems.equals(\old(uniteratedElems)
106: @ .remove(null)))
107: @ && (\result != null
108: @ ==> \old(uniteratedElems).has((JMLType) \result)
109: @ && uniteratedElems.equals(\old(uniteratedElems)
110: @ .remove((JMLType) \result)));
111: @ also
112: @ public exceptional_behavior
113: @ requires !hasMoreElements();
114: @ assignable \nothing;
115: @ signals (JMLNoSuchElementException);
116: @*/
117: public Object nextElement() throws JMLNoSuchElementException {
118: if (currentNode != null) {
119: JMLType retValue = currentNode.val;
120: //@ assume retValue != null ==> \typeof(retValue) <: elementType;
121: //@ assume retValue == null ==> returnsNull;
122: currentNode = currentNode.next;
123: return retValue;
124: } else {
125: throw new JMLNoSuchElementException(
126: "Tried to .nextElement() " + "with JMLValueSet "
127: + "Enumerator `off the end'");
128: }
129: }
130:
131: /** Return a clone of this enumerator.
132: */
133: public Object clone() {
134: return new JMLValueSetEnumerator(new JMLValueSet(currentNode));
135: } //@ nowarn Post;
136:
137: /** Return true just when this enumerator has the same state as
138: * the given argument.
139: */
140: public/*@ pure @*/boolean equals(Object oth) {
141: if (oth == null || !(oth instanceof JMLValueSetEnumerator)) {
142: return false;
143: } else {
144: JMLValueSetEnumerator js = (JMLValueSetEnumerator) oth;
145: if (currentNode == null) {
146: return js.currentNode == null;
147: } else {
148: return currentNode.equals(js.currentNode);
149: }
150: }
151: }
152:
153: /** Return a hash code for this enumerator.
154: */
155: public int hashCode() {
156: return currentNode == null ? 0 : currentNode.hashCode();
157: }
158: }
|