001: // @(#)$Id: JMLValueSequenceEnumerator.java 1.2 Mon, 09 May 2005 15:27:50 +0200 engelc $
002:
003: // Copyright (C) 1998, 1999 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 sequences 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 JMLObjectSequence
033: * @see JMLValueSequence
034: * @see JMLEnumerationToIterator
035: */
036: //-@ immutable
037: public class JMLValueSequenceEnumerator implements JMLEnumeration,
038: JMLValueType {
039:
040: /** The elements that have not yet been returned by nextElement.
041: */
042: //@ public model JMLValueSequence uniteratedElems; in objectState;
043: //@ public invariant uniteratedElems != null;
044: /** The list representing the elements yet to be returned.
045: */
046: protected JMLListValueNode currentNode;
047: //@ in uniteratedElems;
048:
049: /** The number of elements remaining to return.
050: */
051: protected/*@ spec_public @*/int remaining;
052:
053: //@ in uniteratedElems;
054:
055: /*@ protected represents uniteratedElems
056: @ <- new JMLValueSequence(currentNode, remaining);
057: @*/
058:
059: //@ public invariant moreElements <==> remaining != 0;
060: //@ public invariant remaining >= 0;
061: //@ protected invariant currentNode == null <==> remaining == 0;
062: //@ public invariant elementType <: \type(JMLType);
063: /*@ public invariant
064: @ !uniteratedElems.isEmpty()
065: @ ==> uniteratedElems.elementType <: elementType;
066: @*/
067:
068: //@ public constraint returnsNull == \old(returnsNull);
069: /*@ public invariant
070: @ !returnsNull
071: @ ==> uniteratedElems.isEmpty() || !uniteratedElems.containsNull;
072: @*/
073:
074: /** Initialize this with the given sequence.
075: */
076: /*@ normal_behavior
077: @ requires s != null;
078: @ assignable uniteratedElems;
079: @ assignable moreElements, elementType, returnsNull, owner;
080: @ ensures uniteratedElems.equals(s);
081: @ ensures owner == null;
082: @ ensures elementType == s.elementType;
083: @ ensures returnsNull == s.containsNull;
084: @*/
085: JMLValueSequenceEnumerator(/*@ non_null @*/JMLValueSequence s) {
086: remaining = s.int_length();
087: currentNode = s.theSeq;
088: }
089:
090: /** Tells whether this enumerator has more uniterated elements.
091: */
092: /*@ also
093: @ public normal_behavior
094: @ ensures \result == !uniteratedElems.isEmpty();
095: @ ensures \result <==> remaining > 0;
096: @*/
097: public/*@ pure @*/boolean hasMoreElements() {
098: return currentNode != null;
099: }
100:
101: /** Return the next element in the sequence, counting up, if there is one.
102: * @exception JMLNoSuchElementException when this is empty.
103: */
104: /*@ also
105: @ public normal_behavior
106: @ requires hasMoreElements();
107: @ assignable uniteratedElems, moreElements;
108: @ ensures \old(uniteratedElems).itemAt(0).equals(\result)
109: @ && uniteratedElems.equals(\old(uniteratedElems).trailer());
110: @ also
111: @ public exceptional_behavior
112: @ requires !hasMoreElements();
113: @ assignable \nothing;
114: @ signals (JMLNoSuchElementException);
115: @ also
116: @ protected normal_behavior
117: @ requires remaining > 0;
118: @ assignable uniteratedElems, moreElements;
119: @ assignable_redundantly currentNode, remaining;
120: @ ensures currentNode == \old(currentNode.next)
121: @ && remaining == \old(remaining - 1);
122: @*/
123: public Object nextElement() throws JMLNoSuchElementException {
124: if (currentNode != null) {
125: JMLType retValue = currentNode.val;
126: currentNode = currentNode.next;
127: remaining = remaining - 1;
128: return retValue;
129: } else {
130: throw new JMLNoSuchElementException(
131: "Tried to .nextElement() "
132: + "with JMLValueSequence "
133: + "Enumerator `off the end'");
134: }
135: }
136:
137: /** Return a clone of this enumerator.
138: */
139: public Object clone() {
140: return new JMLValueSequenceEnumerator(new JMLValueSequence(
141: currentNode, remaining));
142: }
143:
144: /** Return true just when this enumerator has the same state as
145: * the given argument..
146: */
147: public boolean equals(Object oth) {
148: if (oth == null || !(oth instanceof JMLValueSequenceEnumerator)) {
149: return false;
150: } else {
151: JMLValueSequenceEnumerator js = (JMLValueSequenceEnumerator) oth;
152: if (currentNode == null) {
153: return js.currentNode == null;
154: } else {
155: return currentNode.equals(js.currentNode);
156: }
157: }
158: }
159:
160: /** Return a hash code for this enumerator.
161: */
162: public int hashCode() {
163: return currentNode == null ? 0 : currentNode.hashCode();
164: }
165: }
|