3 files changed, 37 insertions, 6 deletions
diff --git a/Chalice/examples/refinement/SumCubes.chalice b/Chalice/examples/refinement/SumCubes.chalice
new file mode 100644
index 00000000..5ebf78cd
--- /dev/null
+++ b/Chalice/examples/refinement/SumCubes.chalice
@@ -0,0 +1,31 @@
+// Prove \sum i*i*i == (\sum i)(\sum i)
+class SumCubes {
+  method compute0(n: int)
+    requires n >= 0;
+  {
+    var i := 0;
+    var s := 0;
+    while (i < n)
+      invariant i <= n;
+    {
+      i := i + 1;
+      s := s + i*i*i;
+    }
+  }
+  method compute1(n: int)
+    requires n >= 0; 
+  {
+    var i := 0;
+    var s := 0;
+    var t := 0;
+    while (i < n)
+      invariant i <= n;
+      invariant s == t*t;
+      invariant 2*t == i*(i+1);
+    {    
+      i := i + 1;      
+      s := s + i*i*i;          
+      t := t + i;
+    }
+  }
+}
diff --git a/Chalice/src/Graph.scala b/Chalice/src/Graph.scala
index 0d4bae4a..bcf44bea 100644
--- a/Chalice/src/Graph.scala
+++ b/Chalice/src/Graph.scala
@@ -11,10 +11,7 @@ package chalice;
 import scala.collection.mutable;
 import scala.collection.immutable;
 
-
-/**
- * Undirected graph without edge payload. Stored with adjacency lists. Edges have no multiplicites
- */
+// Directed simple graph on T. Payload of nodes (of type T) should remain immutable while in graph.
 class DiGraph[T] {
   private class Node[T](t: T) {
     val data: T = t;
@@ -58,8 +55,8 @@ class DiGraph[T] {
     immutable.Set() ++ (rep(t).children map {x => x.data})
   }
   
-  // Compute condensation of the digraph
-  // The result digraph has no self loops  
+  // Compute condensation of the digraph.
+  // The resulting digraph has no self loops
   def computeSCC(): (DiGraph[List[T]],mutable.Map[T,List[T]]) = {
     // Tarjan's algorithm for finding strongly connected components
     // http://algowiki.net/wiki/index.php/Tarjan%27s_algorithm
diff --git a/Chalice/src/Prelude.scala b/Chalice/src/Prelude.scala
index f5f4861d..1d127c76 100644
--- a/Chalice/src/Prelude.scala
+++ b/Chalice/src/Prelude.scala
@@ -279,5 +279,8 @@ axiom (forall m1: MaskType, m2: MaskType :: {submask(m1, m2)}
   submask(m1, m2) <==> (forall<T> o: ref, f: Field T :: (m1[o, f][perm$R] < m2[o, f][perm$R]) || (m1[o, f][perm$R] == m2[o, f][perm$R] && m1[o, f][perm$N] <= m2[o, f][perm$N]))
 );
 
+// ---------------------------------------------------------------
+// -- End of prelude ---------------------------------------------
+// ---------------------------------------------------------------
 """
 }