2
* This program is free software; you can redistribute it and/or modify
3
* it under the terms of the GNU General Public License as published by
4
* the Free Software Foundation; either version 2 of the License, or
5
* (at your option) any later version.
7
* This program is distributed in the hope that it will be useful,
8
* but WITHOUT ANY WARRANTY; without even the implied warranty of
9
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
10
* GNU General Public License for more details.
12
* You should have received a copy of the GNU General Public License
13
* along with this program; if not, write to the Free Software
14
* Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
19
* Copyright (C) 1999 University of Waikato, Hamilton, New Zealand
21
* Modified March-May 2004 by Mark Utting to add JML specs
22
* (this was done as the example solution of an assignment for a
23
* software engineering course, so the specifications are more precise
24
* and complete than one would normally do).
25
* Passed a static analysis using ESC/Java-2.0a6 with no warnings.
30
import java.io.Serializable;
33
* Class representing a FIFO queue.
35
* @author Len Trigg (trigg@cs.waikato.ac.nz)
36
* @version $Revision: 1.9 $
40
implements Serializable {
42
/** for serialization */
43
private static final long serialVersionUID = -1141282001146389780L;
46
* Represents one node in the queue.
48
protected class QueueNode
49
implements Serializable {
51
/** for serialization */
52
private static final long serialVersionUID = -5119358279412097455L;
54
/** The next node in the queue */
55
protected /*@ spec_public @*/ QueueNode m_Next;
57
/** The nodes contents
59
protected /*@ non_null spec_public @*/ Object m_Contents;
62
* Creates a queue node with the given contents
64
//@ requires contents != null;
65
//@ assignable m_Contents, m_Next;
66
//@ ensures m_Contents == contents;
67
//@ ensures m_Next == null;
68
public QueueNode(Object contents) {
69
m_Contents = contents;
74
* Sets the next node in the queue, and returns it.
76
//@ requires next != this ;
77
//@ assignable m_Next;
78
//@ ensures m_Next==next && \result==next;
79
public QueueNode next(QueueNode next) {
81
} //@ nowarn Invariant; // Because it stupidly checks the Queue invariant!
84
* Gets the next node in the queue.
86
//@ ensures \result == m_Next;
87
public /*@ pure @*/ QueueNode next() {
92
* Sets the contents of the node.
94
//@ requires contents != null;
95
//@ assignable m_Contents;
96
//@ ensures m_Contents == contents && \result == contents;
97
public Object contents(Object contents) {
98
return m_Contents = contents;
102
* Returns the contents in the node.
104
//@ ensures \result == m_Contents;
105
public /*@ pure @*/ Object contents() {
110
/** Store a reference to the head of the queue */
111
protected /*@ spec_public @*/ QueueNode m_Head = null;
113
/** Store a reference to the tail of the queue */
114
protected /*@ spec_public @*/ QueueNode m_Tail = null;
116
/** Store the c m_Tail.m_Nexturrent number of elements in the queue */
117
protected /*@ spec_public @*/ int m_Size = 0;
119
//@ public invariant m_Head == null <==> m_Tail == null;
120
//@public invariant m_Tail != null ==> m_Tail.m_Next == null;
121
//@ public invariant m_Size >= 0;
122
//@ public invariant m_Size == 0 <==> m_Head == null;
123
//@ public invariant m_Size == 1 <==> m_Head != null && m_Head == m_Tail;
124
//@ public invariant m_Size > 1 ==> m_Head != m_Tail;
125
//@ public invariant m_Size > 1 <== m_Head != m_Tail;
130
* Removes all objects from the queue m_Tail.m_Next.
132
//@ assignable m_Size, m_Head, m_Tail;
133
//@ ensures m_Size == 0;
134
//@ ensures m_Head == null;
135
//@ ensures m_Tail == null;
136
public final synchronized void removeAllElements() {
143
* Appends an object to the back of the queue.
145
* @param item the object to be appended
146
* @return the object appended
148
//@ requires item != null;
149
//@ assignable m_Head, m_Tail, m_Tail.m_Next, m_Head.m_Next, m_Size;
150
//@ ensures m_Head != null;
151
//@ ensures m_Tail != \old(m_Tail);
152
//@ ensures m_Size == \old(m_Size) + 1;
153
//@ ensures \old(m_Size) == 0 ==> m_Head == m_Tail;
154
//@ ensures \old(m_Size) != 0 ==> m_Head == \old(m_Head);
155
//@ ensures m_Tail.contents() == \old(item);
156
//@ ensures \result == item;
157
public synchronized Object push(Object item) {
158
QueueNode newNode = new QueueNode(item);
160
if (m_Head == null) {
161
m_Head = m_Tail = newNode;
163
m_Tail = m_Tail.next(newNode);
170
* Pops an object from the front of the queue.
172
* @return the object at the front of the queue
173
* @exception RuntimeException if the queue is empty
175
//@ assignable m_Head, m_Tail, m_Size;
176
//@ ensures m_Size == \old(m_Size) - 1;
177
//@ ensures m_Head == \old(m_Head.m_Next);
178
//@ ensures m_Head != null ==> m_Tail == \old(m_Tail);
179
//@ ensures \result == \old(m_Head.m_Contents);
180
//@ signals (RuntimeException) \old(m_Head) == null;
181
public synchronized Object pop()
182
throws RuntimeException // REDUNDANT, BUT ESCJAVA REQUIRES THIS
184
if (m_Head == null) {
185
throw new RuntimeException("Queue is empty");
187
Object retval = m_Head.contents();
189
m_Head = m_Head.next();
190
// Here we need to either tell ESC/Java some facts about
191
// the contents of the list after popping off the head,
192
// or turn off the 'invariant' warnings.
194
//@ assume m_Size == 0 <==> m_Head == null;
195
//@ assume m_Size == 1 <==> m_Head == m_Tail;
196
if (m_Head == null) {
203
* Gets object from the front of the queue.
205
* @return the object at the front of the queue
206
* @exception RuntimeException if the queue is empty
208
//@ ensures \result == \old(m_Head.m_Contents);
209
//@ signals (RuntimeException) \old(m_Head) == null;
210
public /*@ pure @*/ synchronized Object peek()
211
throws RuntimeException
213
if (m_Head == null) {
214
throw new RuntimeException("Queue is empty");
216
return m_Head.contents();
220
* Checks if queue is empty.
222
* @return true if queue is empty
224
//@ ensures \result <==> m_Head == null;
225
public /*@ pure @*/ boolean empty() {
226
return m_Head == null;
232
* @return size of queue
234
//@ ensures \result == m_Size;
235
public /*@ pure @*/ int size() {
240
* Produces textual description of queue.
242
* @return textual description of queue
245
//@ ensures \result != null;
246
//@ ensures (* \result == textual description of the queue *);
247
public /*@ pure @*/ String toString() {
249
String retval = "Queue Contents "+m_Size+" elements\n";
250
QueueNode current = m_Head;
251
if (current == null) {
252
return retval + "Empty\n";
254
while (current != null) {
255
retval += current.contents().toString()+"\n"; //@nowarn Modifies;
256
current = current.next();
263
* Main method for testing this class.
265
* @param argv a set of strings that are pushed on a test queue
267
//@ requires argv.length >= 0;
268
//@ requires argv != null;
269
//@ requires (\forall int i; 0 <= i && i < argv.length; argv[i] != null);
270
public static void main(String [] argv) {
273
Queue queue = new Queue();
274
for(int i = 0; i < argv.length; i++) {
277
System.out.println("After pushing command line arguments");
278
System.out.println(queue.toString());
279
while (!queue.empty()) {
280
System.out.println("Pop: " + queue.pop().toString());
282
// try one more pop, to make sure we get an exception
286
System.out.println("ERROR: pop did not throw exception!");
288
catch (RuntimeException ex)
290
System.out.println("Pop on empty queue correctly gave exception.");
292
} catch (Exception ex) {
293
System.out.println(ex.getMessage());