001: /*
002: * This program is free software; you can redistribute it and/or modify
003: * it under the terms of the GNU General Public License as published by
004: * the Free Software Foundation; either version 2 of the License, or
005: * (at your option) any later version.
006: *
007: * This program is distributed in the hope that it will be useful,
008: * but WITHOUT ANY WARRANTY; without even the implied warranty of
009: * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
010: * GNU General Public License for more details.
011: *
012: * You should have received a copy of the GNU General Public License
013: * along with this program; if not, write to the Free Software
014: * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
015: */
016:
017: /*
018: * Queue.java
019: * Copyright (C) 1999 University of Waikato, Hamilton, New Zealand
020: *
021: * Modified March-May 2004 by Mark Utting to add JML specs
022: * (this was done as the example solution of an assignment for a
023: * software engineering course, so the specifications are more precise
024: * and complete than one would normally do).
025: * Passed a static analysis using ESC/Java-2.0a6 with no warnings.
026: */
027:
028: package weka.core;
029:
030: import java.io.Serializable;
031:
032: /**
033: * Class representing a FIFO queue.
034: *
035: * @author Len Trigg (trigg@cs.waikato.ac.nz)
036: * @version $Revision: 1.9 $
037: */
038: public class Queue extends Object implements Serializable {
039:
040: /** for serialization */
041: private static final long serialVersionUID = -1141282001146389780L;
042:
043: /**
044: * Represents one node in the queue.
045: */
046: protected class QueueNode implements Serializable {
047:
048: /** for serialization */
049: private static final long serialVersionUID = -5119358279412097455L;
050:
051: /** The next node in the queue */
052: protected/*@ spec_public @*/QueueNode m_Next;
053:
054: /** The nodes contents
055: */
056: protected/*@ non_null spec_public @*/Object m_Contents;
057:
058: /**
059: * Creates a queue node with the given contents
060: */
061: //@ requires contents != null;
062: //@ assignable m_Contents, m_Next;
063: //@ ensures m_Contents == contents;
064: //@ ensures m_Next == null;
065: public QueueNode(Object contents) {
066: m_Contents = contents;
067: next(null);
068: }
069:
070: /**
071: * Sets the next node in the queue, and returns it.
072: */
073: //@ requires next != this ;
074: //@ assignable m_Next;
075: //@ ensures m_Next==next && \result==next;
076: public QueueNode next(QueueNode next) {
077: return m_Next = next;
078: } //@ nowarn Invariant; // Because it stupidly checks the Queue invariant!
079:
080: /**
081: * Gets the next node in the queue.
082: */
083: //@ ensures \result == m_Next;
084: public/*@ pure @*/QueueNode next() {
085: return m_Next;
086: }
087:
088: /**
089: * Sets the contents of the node.
090: */
091: //@ requires contents != null;
092: //@ assignable m_Contents;
093: //@ ensures m_Contents == contents && \result == contents;
094: public Object contents(Object contents) {
095: return m_Contents = contents;
096: }
097:
098: /**
099: * Returns the contents in the node.
100: */
101: //@ ensures \result == m_Contents;
102: public/*@ pure @*/Object contents() {
103: return m_Contents;
104: }
105: }
106:
107: /** Store a reference to the head of the queue */
108: protected/*@ spec_public @*/QueueNode m_Head = null;
109:
110: /** Store a reference to the tail of the queue */
111: protected/*@ spec_public @*/QueueNode m_Tail = null;
112:
113: /** Store the c m_Tail.m_Nexturrent number of elements in the queue */
114: protected/*@ spec_public @*/int m_Size = 0;
115:
116: //@ public invariant m_Head == null <==> m_Tail == null;
117: //@public invariant m_Tail != null ==> m_Tail.m_Next == null;
118: //@ public invariant m_Size >= 0;
119: //@ public invariant m_Size == 0 <==> m_Head == null;
120: //@ public invariant m_Size == 1 <==> m_Head != null && m_Head == m_Tail;
121: //@ public invariant m_Size > 1 ==> m_Head != m_Tail;
122: //@ public invariant m_Size > 1 <== m_Head != m_Tail;
123:
124: /**
125: * Removes all objects from the queue m_Tail.m_Next.
126: */
127: //@ assignable m_Size, m_Head, m_Tail;
128: //@ ensures m_Size == 0;
129: //@ ensures m_Head == null;
130: //@ ensures m_Tail == null;
131: public final synchronized void removeAllElements() {
132: m_Size = 0;
133: m_Head = null;
134: m_Tail = null;
135: }
136:
137: /**
138: * Appends an object to the back of the queue.
139: *
140: * @param item the object to be appended
141: * @return the object appended
142: */
143: //@ requires item != null;
144: //@ assignable m_Head, m_Tail, m_Tail.m_Next, m_Head.m_Next, m_Size;
145: //@ ensures m_Head != null;
146: //@ ensures m_Tail != \old(m_Tail);
147: //@ ensures m_Size == \old(m_Size) + 1;
148: //@ ensures \old(m_Size) == 0 ==> m_Head == m_Tail;
149: //@ ensures \old(m_Size) != 0 ==> m_Head == \old(m_Head);
150: //@ ensures m_Tail.contents() == \old(item);
151: //@ ensures \result == item;
152: public synchronized Object push(Object item) {
153: QueueNode newNode = new QueueNode(item);
154:
155: if (m_Head == null) {
156: m_Head = m_Tail = newNode;
157: } else {
158: m_Tail = m_Tail.next(newNode);
159: }
160: m_Size++;
161: return item;
162: }
163:
164: /**
165: * Pops an object from the front of the queue.
166: *
167: * @return the object at the front of the queue
168: * @exception RuntimeException if the queue is empty
169: */
170: //@ assignable m_Head, m_Tail, m_Size;
171: //@ ensures m_Size == \old(m_Size) - 1;
172: //@ ensures m_Head == \old(m_Head.m_Next);
173: //@ ensures m_Head != null ==> m_Tail == \old(m_Tail);
174: //@ ensures \result == \old(m_Head.m_Contents);
175: //@ signals (RuntimeException) \old(m_Head) == null;
176: public synchronized Object pop() throws RuntimeException // REDUNDANT, BUT ESCJAVA REQUIRES THIS
177: {
178: if (m_Head == null) {
179: throw new RuntimeException("Queue is empty");
180: }
181: Object retval = m_Head.contents();
182: m_Size--;
183: m_Head = m_Head.next();
184: // Here we need to either tell ESC/Java some facts about
185: // the contents of the list after popping off the head,
186: // or turn off the 'invariant' warnings.
187: //
188: //@ assume m_Size == 0 <==> m_Head == null;
189: //@ assume m_Size == 1 <==> m_Head == m_Tail;
190: if (m_Head == null) {
191: m_Tail = null;
192: }
193: return retval;
194: }
195:
196: /**
197: * Gets object from the front of the queue.
198: *
199: * @return the object at the front of the queue
200: * @exception RuntimeException if the queue is empty
201: */
202: //@ ensures \result == \old(m_Head.m_Contents);
203: //@ signals (RuntimeException) \old(m_Head) == null;
204: public/*@ pure @*/synchronized Object peek()
205: throws RuntimeException {
206: if (m_Head == null) {
207: throw new RuntimeException("Queue is empty");
208: }
209: return m_Head.contents();
210: }
211:
212: /**
213: * Checks if queue is empty.
214: *
215: * @return true if queue is empty
216: */
217: //@ ensures \result <==> m_Head == null;
218: public/*@ pure @*/boolean empty() {
219: return m_Head == null;
220: }
221:
222: /**
223: * Gets queue's size.
224: *
225: * @return size of queue
226: */
227: //@ ensures \result == m_Size;
228: public/*@ pure @*/int size() {
229: return m_Size;
230: }
231:
232: /**
233: * Produces textual description of queue.
234: *
235: * @return textual description of queue
236: */
237: //@ also
238: //@ ensures \result != null;
239: //@ ensures (* \result == textual description of the queue *);
240: public/*@ pure @*/String toString() {
241:
242: String retval = "Queue Contents " + m_Size + " elements\n";
243: QueueNode current = m_Head;
244: if (current == null) {
245: return retval + "Empty\n";
246: } else {
247: while (current != null) {
248: retval += current.contents().toString() + "\n"; //@nowarn Modifies;
249: current = current.next();
250: }
251: }
252: return retval;
253: } //@ nowarn Post;
254:
255: /**
256: * Main method for testing this class.
257: *
258: * @param argv a set of strings that are pushed on a test queue
259: */
260: //@ requires argv.length >= 0;
261: //@ requires argv != null;
262: //@ requires (\forall int i; 0 <= i && i < argv.length; argv[i] != null);
263: public static void main(String[] argv) {
264:
265: try {
266: Queue queue = new Queue();
267: for (int i = 0; i < argv.length; i++) {
268: queue.push(argv[i]);
269: }
270: System.out.println("After pushing command line arguments");
271: System.out.println(queue.toString());
272: while (!queue.empty()) {
273: System.out.println("Pop: " + queue.pop().toString());
274: }
275: // try one more pop, to make sure we get an exception
276: try {
277: queue.pop();
278: System.out
279: .println("ERROR: pop did not throw exception!");
280: } catch (RuntimeException ex) {
281: System.out
282: .println("Pop on empty queue correctly gave exception.");
283: }
284: } catch (Exception ex) {
285: System.out.println(ex.getMessage());
286: }
287: }
288: }
|