public class LinkedList implements List
class Node
1:
2: package mylist;
3:
4: /**
5: * An implementation of List using a doubly-linked list
6: *
7: * @invariant _wellformed()
8: */
9: public class LinkedList implements List, java.lang.Cloneable, java.io.Serializable {
10:
11: public LinkedList() {
12: head = tail = null;
13: count = 0;
14: }
15:
16: public int size() {
17: return count;
18: }
19:
20: public boolean isEmpty() {
21: return (count == 0);
22: }
23:
24: public Object element(int i) {
25: assert i >= 0 && i < size();
26: Node n = head;
27: for (int j = 0; n != null && j < i; j++) {
28: n = n.next;
29: }
30: return n.item;
31: }
32:
33: public Object head() {
34: assert !isEmpty();
35: Object result = (head != null ? head.item : null);
36: assert result == element(0);
37: return result;
38: }
39:
40: public Object last() {
41: assert !isEmpty();
42: Object result = (tail != null ? tail.item : null);
43: assert result == element(size() - 1);
44: return result;
45: }
46:
47: public String toString() {
48: StringBuffer s = new StringBuffer();
49: int i = 0;
50: for (Node n = head; n != null; n = n.next, i++) {
51: s.append("[" + i + "] = " + n.item + "\n");
52: }
53: return s.toString();
54: }
55:
56: public boolean equals(Object other) {
57: if (other != null &&
58: other instanceof LinkedList) {
59: LinkedList otherlist = (LinkedList) other;
60: if (this.size() == otherlist.size()) {
61: Node thisnode = this.head;
62: Node othernode = otherlist.head;
63: while (thisnode != null && othernode != null) {
64: if (!thisnode.item.equals(othernode.item))
65: return false;
66: thisnode = thisnode.next;
67: othernode = othernode.next;
68: }
69: return true;
70: }
71: }
72: return false;
73: }
74:
75: public Object clone()
76: throws CloneNotSupportedException {
77: LinkedList list = (LinkedList) super.clone();
78: list.head = list.tail = null;
79: list.count = 0;
80: for (Node node = head; node != null; node = node.next) {
81: if (node.item != null) {
82: list.insertLast(node.item);
83: }
84: }
85: return list;
86: }
87:
88: /**
89: * Inserts a new element into the list at the i-th position.
90: *
91: * @pre item != null && i >= 0 && i <= size()
92: * @post size() == size()@pre + 1
93: * @post @forall k : [0 .. size() - 1] @
94: * (k < i ==> element(k)@pre == element(k)) &&
95: * (k == i ==> item@pre == element(k)) &&
96: * (k > i ==> element(k - 1)@pre == element(k)
97: */
98: public void insert(Object item, int i) {
99: // assert the pre-condition
100: assert item != null && i >= 0 && i <= size();
101: // assert the invaraint
102: assert _wellformed();
103:
104: // the object in pre-state, used in the post-conditions
105: int size_pre = size();
106: LinkedList this_pre = null;
107: try {
108: this_pre = (LinkedList) clone();
109: } catch (CloneNotSupportedException e) {}
110:
111: // begin insertion
112: if (i <= 0) {
113: insertHead(item);
114: } else if (i >= count) {
115: insertLast(item);
116: } else {
117: // i > 0 && i < count;
118: Node n = head;
119: for (int j = 0; n != null && j < i - 1; j++) {
120: n = n.next;
121: }
122: Node node = new Node();
123: node.item = item;
124: node.next = n.next;
125: node.prev = n;
126: node.next.prev = node;
127: n.next = node;
128: count++;
129: }
130: // end insertion
131:
132: // assert the post-condition
133: int size_post = size();
134: assert size_post == size_pre + 1;
135:
136: // assert the post-condition
137: // the quantified experssion is translated into a for-loop
138: boolean insertOK = true;
139: for (int k = 0; insertOK && k < size(); k++) {
140: if (k < i) {
141: insertOK = (this_pre.element(k) == element(k));
142: } else if (k == i) {
143: insertOK = (item == element(k));
144: } else {
145: insertOK = (this_pre.element(k - 1) == element(k));
146: }
147: }
148: assert insertOK;
149:
150: // assert the invariant
151: assert _wellformed();
152: }
153:
154: public void insertHead(Object item) {
155: assert item != null;
156: assert _wellformed();
157: Node node = new Node();
158: node.item = item;
159: node.next = head;
160: node.prev = null;
161: if (head == null)
162: tail = node;
163: else
164: head.prev = node;
165: head = node;
166: count++;
167: assert _wellformed();
168: }
169:
170: public void insertLast(Object item) {
171: assert item != null;
172: assert _wellformed();
173: Node node = new Node();
174: node.item = item;
175: node.next = null;
176: node.prev = tail;
177: if (tail != null)
178: tail.next = node;
179: else
180: head = tail = node;
181: tail = node;
182: count++;
183: assert _wellformed();
184: }
185:
186: public Object remove(int i) {
187: assert size() > 0;
188: assert i >= 0 && i < size();
189: assert _wellformed();
190: Object result = null;
191: if (i <= 0) {
192: result = removeHead();
193: } else if (i >= count) {
194: result = removeLast();
195: } else {
196: Node n = head;
197: for (int j = 0; n != null && j < i - 1; j++)
198: n = n.next;
199: result = n.next.item;
200: n.next = n.next.next;
201: n.next.prev = n;
202: count--;
203: }
204: assert _wellformed();
205: return result;
206: }
207:
208: public Object removeHead() {
209: assert size() > 0;
210: assert _wellformed();
211: Object result = null;
212: if (head != null) {
213: result = head;
214: head = head.next;
215: if (head != null)
216: head.prev = null;
217: else
218: tail = null;
219: count--;
220: }
221: assert _wellformed();
222: return result;
223: }
224:
225: public Object removeLast() {
226: assert size() > 0;
227: assert _wellformed();
228: Object result = null;
229: if (tail != null) {
230: result = tail;
231: tail = tail.prev;
232: if (tail != null)
233: tail.next = null;
234: else
235: head = null;
236: count--;
237: }
238: assert _wellformed();
239: return result;
240: }
241:
242: protected Node head, tail;
243: protected int count;
244:
245: class Node {
246: Object item;
247: Node next;
248: Node prev;
249: }
250:
251: /**
252: * The invaraiant of the linked list implementation.
253: */
254: protected boolean _wellformed() {
255: int n = 0;
256: for (Node p = head; p != null; p = p.next) {
257: n++;
258: if (p.prev != null) {
259: if (p.prev.next != p) return false;
260: } else {
261: if (head != p) return false;
262: }
263: if (p.next != null) {
264: if (p.next.prev != p) return false;
265: } else {
266: if (tail != p) return false;
267: }
268: }
269: return n == count;
270: }
271:
272: }