00001
00005 package edu.mit.csail.sdg.squander.examples.list;
00006
00007 import java.util.ArrayList;
00008 import java.util.Arrays;
00009 import java.util.HashSet;
00010 import java.util.Iterator;
00011 import java.util.List;
00012 import java.util.Set;
00013
00014 import edu.mit.csail.sdg.annotations.Ensures;
00015 import edu.mit.csail.sdg.annotations.Invariant;
00016 import edu.mit.csail.sdg.annotations.Modifies;
00017 import edu.mit.csail.sdg.annotations.Requires;
00018 import edu.mit.csail.sdg.annotations.Returns;
00019 import edu.mit.csail.sdg.annotations.SpecField;
00020 import edu.mit.csail.sdg.squander.Squander;
00021 import edu.mit.csail.sdg.squander.annotations.FreshObjects;
00022
00028 @SpecField("nodes : set Node | this.nodes = this.header.succ - null")
00029 public class LinkedList implements Iterable<LinkedList.Node> {
00030
00031 @Invariant("this !in this.^next")
00032 @SpecField("succ : set Node | this.succ = this.*next - null")
00033 public static class Node {
00034 private int value;
00035 private Node next;
00036
00037 public Node(int value) {
00038 this.value = value;
00039 }
00040
00041 public int getValue() { return value; }
00042 public void setValue(int value) { this.value = value; }
00043 public Node getNext() { return next; }
00044 public void setNext(Node next) { this.next = next; }
00045
00046 @Returns("this.succ")
00047 public Node[] succ() {
00048 return Squander.exe(this);
00049 }
00050
00051 @Override
00052 public String toString() {
00053 return Integer.toString(value);
00054 }
00055
00056 public int size() {
00057 if (next == null)
00058 return 1;
00059 else
00060 return 1 + next.size();
00061 }
00062
00063 }
00064
00065 private Node header;
00066
00067 @Requires("n.succ !in this.nodes")
00068 @Ensures("this.nodes = @old(this.nodes) + n.succ")
00069 @Modifies({
00070 "this.header",
00071 "Node.next [{nn : this.nodes | nn.next == null}]"
00072 })
00073 public void add(Node n) { Squander.exe(this, n); }
00074
00075 public void add_man(Node node) {
00076 Node n = header;
00077 Node prev = null;
00078 while (n != null) {
00079 prev = n;
00080 n = n.next;
00081 }
00082 if (prev == null)
00083 header = node;
00084 else
00085 prev.next = node;
00086 }
00087
00088 @Requires("n in this.nodes")
00089 @Ensures("this.nodes = @old(this.nodes) - n")
00090 @Modifies({
00091 "this.header",
00092 "Node.next [{nn : this.nodes | nn.next == n}]"
00093 })
00094 public void remove(Node n) { Squander.exe(this, n); }
00095
00096
00097
00098 @Ensures({"return.length=#this.nodes",
00099 "all n1 : Node | n1 in this.nodes => n1 in return[int] && (all n2 : Node | n2 in n1.^next => return.elems.n1 < return.elems.n2)"})
00100 @Modifies({"return.elems", "return.length"})
00101 @FreshObjects(cls = Node[].class, num = 1)
00102 public Node[] nodes() { return Squander.exe(this); }
00103
00104 public Node header() { return header; }
00105
00106 @Override
00107 public Iterator<Node> iterator() {
00108 List<Node> nodes = new ArrayList<Node>();
00109 Node n = header;
00110 while (n != null) {
00111 nodes.add(n);
00112 n = n.next;
00113 }
00114 return nodes.iterator();
00115 }
00116
00117 @Override
00118 public String toString() {
00119 return Arrays.toString(nodes());
00120 }
00121
00122 public static void main(String[] args) {
00123 LinkedList lst = new LinkedList();
00124 lst.add(new Node(1));
00125 lst.header = new Node(1);
00126 Node n2 = new Node(2);
00127 n2.setNext(new Node(3));
00128 lst.add(n2);
00129 lst.remove(lst.header);
00130
00131 System.out.println(lst);
00132
00133
00134 }
00135
00136 public int size() {
00137 if (header == null)
00138 return 0;
00139 return header.size();
00140 }
00141
00142 public boolean repOk() {
00143 Set<Integer> visited = new HashSet<Integer>();
00144 Node n = header;
00145 while (n != null) {
00146 if (!visited.add(System.identityHashCode(n)))
00147 return false;
00148 n = n.next;
00149 }
00150 return true;
00151 }
00152
00153 public int findNode(Integer key) {
00154 Node n = header;
00155 int cnt = 0;
00156 while (n != null) {
00157 if (n.value == key)
00158 return cnt;
00159 cnt++;
00160 n = n.next;
00161 }
00162 return -1;
00163 }
00164
00165 }