00001
00005 package edu.mit.csail.sdg.squander.examples.list;
00006
00007 import java.util.Arrays;
00008
00009 import edu.mit.csail.sdg.annotations.Ensures;
00010 import edu.mit.csail.sdg.annotations.Invariant;
00011 import edu.mit.csail.sdg.annotations.Modifies;
00012 import edu.mit.csail.sdg.annotations.Requires;
00013 import edu.mit.csail.sdg.annotations.Returns;
00014 import edu.mit.csail.sdg.annotations.SpecField;
00015 import edu.mit.csail.sdg.squander.Squander;
00016 import edu.mit.csail.sdg.squander.annotations.FreshObjects;
00017
00023 @SpecField("nodes : set Node | this.nodes = this.header.succ")
00024 public class LinkedList_ind {
00025
00026 @Invariant("this !in this.^next")
00027 @SpecField("succ : set Node | this.next == null ? this.succ = this : this.succ = this + this.next.succ - null")
00028 public static class Node {
00029 private int value;
00030 private Node next;
00031
00032 public Node(int value) {
00033 this.value = value;
00034 }
00035
00036 public int getValue() { return value; }
00037 public void setValue(int value) { this.value = value; }
00038 public Node getNext() { return next; }
00039 public void setNext(Node next) { this.next = next; }
00040
00041 @Returns("this.succ")
00042 public Node[] succ() {
00043 return Squander.exe(this);
00044 }
00045
00046 @Override
00047 public String toString() {
00048 return Integer.toString(value);
00049 }
00050
00051 }
00052
00053 private Node header;
00054
00055 @Requires("n.succ !in this.nodes")
00056 @Ensures("this.nodes = @old(this.nodes) + n.succ")
00057 @Modifies({"this.header", "this.nodes", "Node.succ", "Node.next [{n : Node | n in this.nodes && n.next == null}]"})
00058 public void addNode(Node n) { Squander.exe(this, new Class[] {Node.class}, new Node[] {n}); }
00059
00060 @Ensures("return[int] = this.nodes && return.length=#this.nodes")
00061 @Modifies({"return.elems", "return.length"})
00062 @FreshObjects(cls = Node[].class, num = 1)
00063 public Node[] nodes() { return Squander.exe(this); }
00064
00065 public Node header() { return header; }
00066
00067 @Override
00068 public String toString() {
00069 return Arrays.toString(nodes());
00070 }
00071
00072 public static void main(String[] args) {
00073 LinkedList_ind lst = new LinkedList_ind();
00074
00075
00076 lst.header = new Node(1);
00077 Node n2 = new Node(2);
00078 n2.setNext(new Node(3));
00079 lst.addNode(n2);
00080
00081 }
00082
00083 }