001: // @(#)$Id: JMLEnumerationToIterator.java 1.1.1.1 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: /** A wrapper that makes any {@link JMLEnumeration} into a {@link
024: * JMLIterator} that does not support the remove operation.
025: *
026: * @version $Revision: 1.1.1.1 $
027: * @author Gary T. Leavens
028: * @see JMLEnumeration
029: * @see JMLIterator
030: * @see java.util.Iterator
031: */
032: //-@ immutable
033: public class JMLEnumerationToIterator implements JMLIterator {
034:
035: protected final/*@ spec_public non_null @*/JMLEnumeration theEnumeration;
036:
037: //@ maps theEnumeration.objectState \into objectState;
038:
039: /*@ public represents moreElements <- theEnumeration.hasMoreElements();
040: @ public represents_redundantly
041: @ moreElements <- theEnumeration.moreElements;
042: @*/
043:
044: /** Initialize this iterator with the given Enumeration. The
045: * enumeration is cloned.
046: */
047: /*@ public normal_behavior
048: @ requires e != null;
049: @ assignable owner, theEnumeration, elementType, moreElements;
050: @ assignable returnsNull;
051: @ ensures theEnumeration.equals(e);
052: @ ensures owner == null;
053: @*/
054: public JMLEnumerationToIterator(/*@ non_null @*/JMLEnumeration e) {
055: Object o = e.clone();
056: theEnumeration = (JMLEnumeration) o;
057: }
058:
059: /** Tells whether this has more uniterated elements.
060: */
061: /*@ also
062: @ public normal_behavior
063: @ ensures \result == theEnumeration.moreElements;
064: @ ensures_redundantly \result == theEnumeration.moreElements;
065: @*/
066: public/*@ pure @*/boolean hasNext() {
067: return theEnumeration.hasMoreElements();
068: }
069:
070: /** Return the next element in this, if there is one.
071: * @exception JMLNoSuchElementException when this is empty.
072: */
073: /*@ also
074: @ public normal_behavior
075: @ requires moreElements;
076: @ requires_redundantly hasNext();
077: @ assignable objectState, moreElements, remove_called_since;
078: @ also
079: @ public exceptional_behavior
080: @ requires !moreElements;
081: @ requires_redundantly !hasNext();
082: @ assignable \nothing;
083: @ signals (JMLNoSuchElementException);
084: @*/
085: public Object next() throws JMLNoSuchElementException {
086: Object result = theEnumeration.nextElement();
087: return result;
088: }
089:
090: /** The remove operation is not supported in this type.
091: * So remove always throws an UnsupportedOperationException.
092: */
093: /*@ also
094: @ signals (UnsupportedOperationException);
095: @*/
096: public void remove() throws UnsupportedOperationException {
097: throw new UnsupportedOperationException();
098: }
099:
100: /** Return a clone of this iterator.
101: */
102: public/*@ pure @*/Object clone() {
103: Object o = theEnumeration.clone();
104: return new JMLEnumerationToIterator((JMLEnumeration) o);
105: }
106:
107: /** Return true just when this iterator has the same state as
108: * the given argument.
109: */
110: /*@ also
111: @ public normal_behavior
112: @ ensures \result <==> oth != null
113: @ && oth instanceof JMLEnumerationToIterator
114: @ && theEnumeration.equals(((JMLEnumerationToIterator) oth)
115: @ .theEnumeration);
116: @*/
117: public/*@ pure @*/boolean equals(Object oth) {
118: return oth != null
119: && oth instanceof JMLEnumerationToIterator
120: && theEnumeration
121: .equals(((JMLEnumerationToIterator) oth).theEnumeration);
122: }
123:
124: /** Return a hash code for this iterator.
125: */
126: public/*@ pure @*/int hashCode() {
127: return theEnumeration.hashCode();
128: }
129: }
|