001: package U2.T2.examples;
002:
003: import java.io.*;
004:
005: /**
006: * This class provides a linked list. The chain of elements are
007: * implemented through a private internal class. A class invariant is
008: * imposed, requiring the chain should not be circular. Note that this
009: * class also takes a class parameter.
010: *
011: * <p>The class contains error; namely the method remove is not
012: * correct.
013: *
014: * <p> Run RT2 on this class with the option --elemty=Dummy. This will
015: * cause the class Dummy to be used in the place of the type parameter
016: * T.
017: */
018: public class MyList<T> {
019:
020: public Link list;
021:
022: private class Link {
023:
024: T item;
025: Link next;
026:
027: // constructors:
028:
029: Link(T i) {
030: item = i;
031: next = null;
032: }
033:
034: Link(T i, Link p) {
035: item = i;
036: next = p;
037: }
038:
039: String show() {
040: String r = ";" + item;
041: if (next == null)
042: r = r + " END";
043: else
044: r = r + next.show();
045: return r;
046: }
047:
048: void print() {
049: System.out.println("> " + this .show());
050: }
051: }
052:
053: /**
054: * The class invariant requiring that the internal list maintained
055: * by this class is not circular.
056: */
057: public boolean classinv() {
058: if (list == null)
059: return true;
060: Link start = list;
061: Link p = list;
062: if (p.next == null)
063: return true;
064: // else:
065: p = p.next;
066: while (p != null && p != start)
067: p = p.next;
068: return p == null;
069: }
070:
071: /**
072: * A method for inserting an element at the head of the list.
073: */
074: public void insert(T i) {
075: Link u = new Link(i);
076: u.next = list;
077: list = u;
078: }
079:
080: /**
081: * A method for deleting all occurences of x from the list. This
082: * method has a rather subtle error: it will miss removing x if it
083: * occurs as the first element in the list. Another error: when
084: * null is passed as x.
085: */
086: public void remove(T x) {
087: if (list == null)
088: return;
089: Link p = list;
090: Link u = p.next;
091: while (u != null) {
092: if (x.equals(u.item))
093: p.next = u.next;
094: u = u.next;
095: p = p.next;
096: }
097: }
098:
099: /**
100: * The specification of remove; it requires that after the removal
101: * x does not appear in the list.
102: */
103: public void remove_spec(T x) {
104: remove(x);
105: Link p = list;
106: boolean ok = true;
107: while (p != null && ok) {
108: ok = p.item != x;
109: p = p.next;
110: }
111: assert ok : "POST";
112: }
113:
114: /**
115: * Returning the size of the list. For this method it is crucial
116: * that the list is not circular (as imposed by the class
117: * invariant), else it won't terminate.
118: */
119: public int size() {
120: Link x = list;
121: int i = 0;
122: while (x != null) {
123: x = x.next;
124: i++;
125: }
126: return i;
127: }
128:
129: }
|