00001
00005 package edu.mit.csail.sdg.squander.examples.graph2;
00006
00007 import edu.mit.csail.sdg.annotations.Ensures;
00008 import edu.mit.csail.sdg.annotations.Modifies;
00009 import edu.mit.csail.sdg.annotations.Requires;
00010 import edu.mit.csail.sdg.annotations.Returns;
00011 import edu.mit.csail.sdg.annotations.SpecField;
00012 import edu.mit.csail.sdg.squander.Squander;
00013 import edu.mit.csail.sdg.squander.annotations.Fresh;
00014 import edu.mit.csail.sdg.squander.annotations.FreshObjects;
00015
00021 @SpecField( { "nodes : set Node",
00022 "edges : set Node -> Node" })
00023 public class Graph {
00024
00025 public static class Node {
00026 public int label;
00027
00028 Node() { this(0); }
00029 Node(int label) { this.label = label; }
00030
00031 @Override
00032 public String toString() {
00033 return String.valueOf(label);
00034 }
00035 }
00036
00037 @Ensures({"no this.nodes", "no this.edges"})
00038 public Graph() {}
00039
00040 @Ensures( { "return !in @old(this.nodes)",
00041 "this.nodes = @old(this.nodes + return)",
00042 "return.label = key" })
00043 @Modifies("this.nodes")
00044 @Fresh(@FreshObjects(cls = Node.class, num = 1))
00045 public Node newNode(int key) {
00046 return Squander.exe(this, new Class<?>[] { int.class }, new Object[] { key });
00047 }
00048
00049 @Ensures( { "this.nodes = @old(this.nodes + n)" })
00050 @Modifies("this.nodes")
00051 public void addNode(Node n) {
00052 Squander.exe(this, new Class<?>[] { Node.class }, new Object[] { n });
00053 }
00054
00055 @Requires("a + b in this.nodes")
00056 @Ensures("this.edges = @old(this.edges) + a -> b")
00057 @Modifies("this.edges")
00058 public void newEdge(Node a, Node b) {
00059 Squander.exe(this, new Class<?>[] { Node.class, Node.class }, new Object[] { a, b });
00060 }
00061
00062 @Ensures("return[int] = this.nodes")
00063 @Modifies({"return.length", "return.elems"})
00064 @Fresh(@FreshObjects(cls = Node[].class, num = 1))
00065 public Node[] nodes() {
00066 return Squander.exe(this);
00067 }
00068
00069 @Returns("#this.edges") public int numEdges() { return Squander.exe(this); }
00070 @Returns("#this.nodes") public int numNodes() { return Squander.exe(this); }
00071 @Returns("#this.nodes") public int size() { return numNodes(); }
00072
00073 @Ensures( {
00074 "return[int] = this.nodes",
00075 "return.length = #this.nodes",
00076 "all i : int | i >= 0 && i < return.length - 1 => return[i] -> return[i+1] in this.edges"
00077 })
00078 @Modifies({"return.length", "return.elems"})
00079 @Fresh(@FreshObjects(cls = Node[].class, num = 1))
00080 public Node[] hamiltonian() {
00081 return Squander.exe(this);
00082 }
00083
00084 @Ensures( {
00085 "return[int] = this.nodes",
00086 "return.length = #this.nodes",
00087 "all i : int | all j : int | 0 <= i && i < j && j < return.length => return[i] -> return[j] !in this.edges"
00088 })
00089 @Modifies({"return.length", "return.elems"})
00090 @Fresh(@FreshObjects(cls = Node[].class, num = 1))
00091 public Node[] topsort() {
00092 return Squander.exe(this);
00093 }
00094
00095 @Ensures({
00096 "return[int] in this.nodes",
00097 "all i : int | all j : int | 0 <= i && i < j && j < return.length => return[i] -> return [j] in this.(edges + ~ edges)",
00098 "#return[int] >= k"
00099 })
00100 @Modifies({"return.length", "return.elems"})
00101 @Fresh(@FreshObjects(cls = Node[].class, num = 1))
00102 public Node[] maxClique(int k) {
00103 return Squander.exe(this, new Class<?>[]{int.class}, new Object[]{k});
00104 }
00105
00106 }