Chalice: example proving a simple identity (for refinement demonstration), revise code comments

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 ---------------------------------------------

+// ---------------------------------------------------------------

 """

 }