Chalice: limited functions are still problematic (see Calculator.chalice)

8 files changed, 110 insertions, 82 deletions

diff --git a/Chalice/refinements/Answer b/Chalice/refinements/Answer
index 6db2a988..a6654fc2 100644
--- a/Chalice/refinements/Answer
+++ b/Chalice/refinements/Answer
@@ -35,3 +35,6 @@ Processing TestCoupling.chalice
   66.5: Location might not be writable

 

 Boogie program verifier finished with 17 verified, 3 errors

+Processing Calculator.chalice
+

+Boogie program verifier finished with 15 verified, 0 errors

diff --git a/Chalice/refinements/Calculator.chalice b/Chalice/refinements/Calculator.chalice
new file mode 100644
index 00000000..57c4c87d
--- /dev/null
+++ b/Chalice/refinements/Calculator.chalice
@@ -0,0 +1,69 @@
+/*
+  Carrol Morgan's calculator  
+  7/2/2010 Kuat Dafny version
+  8/22/2010 translated into Chalice
+*/ 
+
+class Calc0 {  
+  var vals: seq<int>;
+  
+  method reset() 
+    requires acc(vals);
+    ensures acc(vals);
+  {
+    vals := [];
+  }
+  
+  method add(x: int) 
+    requires acc(vals);
+    ensures acc(vals);
+  {
+    vals := [x] ++ vals;    
+  }
+  
+  method mean() returns (m: int)     
+    requires acc(vals) && |vals| > 0;
+    ensures acc(vals);
+  {
+    m := total(vals)/|vals|;
+  }
+
+  unlimited function total(s: seq<int>): int
+  {
+    |s| == 0 ? 0 : s[0] + total(s[1..])
+  }  
+}
+
+
+
+class Calc1 refines Calc0 {  
+  var sum: int;
+  var num: int;
+  replaces vals by acc(sum) && acc(num) && sum == total(vals) && num == |vals|;
+
+  refines reset()   
+  {
+    sum := 0;
+    num := 0;
+  }
+
+  refines add(x: int)    
+  {
+    sum := sum + x;
+    num := num + 1;
+  }
+
+  refines mean() returns (m: int)  
+  {
+    m := sum/num;
+  }
+}
+
+
+
+
+
+
+
+    
+    
diff --git a/Chalice/refinements/Counter.chalice b/Chalice/refinements/Counter.chalice
index c9576a13..e0c0c7df 100644
--- a/Chalice/refinements/Counter.chalice
+++ b/Chalice/refinements/Counter.chalice
@@ -21,24 +21,6 @@ class Counter0 {
   {    
     x := x - 1;  
   }
-
-  /** Interesting issues */  
-
-  /* We can expose representation here */
-  method magic1() returns (c: Cell) 
-    requires acc(x)
-    ensures acc(c.n) && x == old(x);
-  {
-    var c [acc(c.n)];
-  }
-
-  /* This should prevent us from exposing representation */
-  method magic2() returns (c: Cell)
-    requires acc(x);
-    ensures acc(x) && x == old(x) && acc(c.n);
-  {
-    var c [acc(c.n)];
-  }
 }
 
 class Counter1 refines Counter0 {
@@ -46,80 +28,50 @@ class Counter1 refines Counter0 {
   var z: int;  
   replaces x by acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0;
   
-  transforms init() 
+  refines init() 
   {
-    replaces * by {this.y := 0; this.z := 0;}
+    this.y := 0; 
+    this.z := 0;
   }
 
-  transforms inc()
+  refines inc()
   {    
-    replaces * by {this.y := this.y + 1;}
+    this.y := this.y + 1;
   }
 
-  transforms dec() 
+  refines dec() 
   {
-    replaces * by {this.z := this.z + 1;}
+    this.z := this.z + 1;
   }       
-
-  /** This violates abstraction of x -- we must hold all permissions to x to update it */
-  method magic3() 
-    requires acc(y);    
-  {
-    y := y + 1;
-  }
-
-  /** This does also -- but it also prohibits us from reading part of the state across refinement */
-  method magic4() returns (i)
-    requires acc(y);
-  {
-    i := y;
-  }
 }
 
 class Cell {var n: int}
-/*
+
+/** TODO: 
+Two-step data refinement doesn't work for the following reason:
+the spec of Counter1 uses the abstract field x which disappears at the concrete method body level.
+I'm not sure what a good solution to this problem...
+*/
+
 class Counter2 refines Counter1 {
   var a: Cell;
   var b: Cell;
   replaces y, z by acc(a) && acc(b) && acc(a.n) && acc(b.n) && y == a.n && z == b.n;
   
-  transforms init() 
-  {
-    replaces * by {
-      this.a := new Cell {n := 0};
-      this.b := new Cell {n := 0};
-    }
-  }
-
-  transforms inc() 
-  {
-    replaces * by {this.a.n := this.a.n + 1;}
-  }
-
-  transforms dec()
-  {
-    replaces * by {this.b.n := this.b.n + 1;}
-  }
-
-  transforms magic1() returns (c: Cell)
-  {
-    replaces * by {c := this.a;}
-  }
-
-  transforms magic2() returns (c: Cell)
-  {
-    replaces * by {c := this.a;}
+  refines init() 
+  {    
+    this.a := new Cell {n := 0};
+    this.b := new Cell {n := 0};    
   }
 
-  transforms magic3()
+  refines inc() 
   {
-    replaces * by {this.a.n := this.a.n + 1;}
+    this.a.n := this.a.n + 1;
   }
 
-  transforms magic4() returns (i)
+  refines dec()
   {
-    replaces * by {i := this.a.n;}
+    this.b.n := this.b.n + 1;
   }
 }
-*/
   
diff --git a/Chalice/refinements/test.sh b/Chalice/refinements/test.sh
index 24dbd6e5..80b42258 100644
--- a/Chalice/refinements/test.sh
+++ b/Chalice/refinements/test.sh
@@ -14,6 +14,7 @@ TESTS="
   LoopFiniteDiff.chalice
   Pick.chalice
   TestCoupling.chalice
+  Calculator.chalice
 "
 
 # Switch to test directory
@@ -31,7 +32,7 @@ START=`date +%s`
 for f in ${TESTS}
 do
   echo "Processing $f" | tee -a Output
-  scala -cp ../bin chalice.Chalice -nologo $f >> Output 2>&1
+  scala -cp ../bin chalice.Chalice -nologo -noTermination $f >> Output 2>&1
 done
 END=`date +%s`
 echo "Time: $(( $END - $START )) seconds"
diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala
index 92c339ea..7beba704 100644
--- a/Chalice/src/Ast.scala
+++ b/Chalice/src/Ast.scala
@@ -164,7 +164,7 @@ case class Function(id: String, ins: List[Variable], out: Type, spec: List[Speci
     result.f = this;

     result

   }

-  val isUnlimited = false

+  var isUnlimited = false

   var isRecursive = false

   var SCC: List[Function] = Nil

 }

diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala
index d12ca00f..f086487d 100644
--- a/Chalice/src/Parser.scala
+++ b/Chalice/src/Parser.scala
@@ -30,7 +30,7 @@ class Parser extends StandardTokenParsers {
                        "predicate", "function", "free", "send", "receive",

                        "ite", "fold", "unfold", "unfolding", "in", "forall", "exists",

                        "seq", "nil", "result", "eval", "token",

-                       "wait", "signal",

+                       "wait", "signal", "unlimited", 

                        "refines", "transforms", "replaces", "by"

                       )

   // todo: can we remove "nil"?

@@ -88,8 +88,12 @@ class Parser extends StandardTokenParsers {
   def predicateDecl: Parser[Predicate] =

     ("predicate" ~> ident) ~ ("{" ~> expression <~ "}") ^^ { case id ~ definition => Predicate(id, definition) }

   def functionDecl =

-    ("function" ~> ident) ~ formalParameters(true) ~ (":" ~> typeDecl) ~ (methodSpec*) ~ opt("{" ~> expression <~ "}") ^^ {

-      case id ~ ins ~ out ~ specs ~ body => Function(id, ins, out, specs, body)

+    ("unlimited" ?) ~ ("function" ~> ident) ~ formalParameters(true) ~ (":" ~> typeDecl) ~ (methodSpec*) ~ opt("{" ~> expression <~ "}") ^^ {

+      case u ~ id ~ ins ~ out ~ specs ~ body => {

+        val f = Function(id, ins, out, specs, body);

+        if (u.isDefined) f.isUnlimited = true;

+        f

+      }

     }

   def conditionDecl =

     "condition" ~> ident ~ ("where" ~> expression ?) <~ Semi ^^ {

diff --git a/Chalice/src/PrettyPrinter.scala b/Chalice/src/PrettyPrinter.scala
index b2f30c5c..236e74cc 100644
--- a/Chalice/src/PrettyPrinter.scala
+++ b/Chalice/src/PrettyPrinter.scala
@@ -283,7 +283,7 @@ object PrintProgram {
     case Old(e) =>

           print("old("); Expr(e); print(")")

     case IfThenElse(con, then, els) => 

-      print("ite("); Expr(con); print(", "); Expr(then); print(", "); Expr(els); print(")");

+      print("("); Expr(con); print(" ? "); Expr(then); print(" : "); Expr(els); print(")");

     case Not(e) => print("!"); Expr(e, 0x80, false)

     case FunctionApplication(obj, id, ins) =>

       Expr(obj); print("."); print(id); print("("); ExprList(ins); print(")");

diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala
index d4adbec3..2729a0d5 100644
--- a/Chalice/src/Resolver.scala
+++ b/Chalice/src/Resolver.scala
@@ -216,12 +216,11 @@ object Resolver {
                  // resolve function calls

                  calls addNode f;

                  e visit {

-                 case app : FunctionApplication =>

-                   assert(app.f != null);

-                   calls addNode app.f;

-                   calls.addEdge(f, app.f);

-                   if (app.f == f) f.isRecursive = true; // self-recursion

-                 case _ =>

+                   case app : FunctionApplication if app.f != null /* may not be resolved */ =>

+                     calls addNode app.f;

+                     calls.addEdge(f, app.f);

+                     if (app.f == f) f.isRecursive = true; // self-recursion

+                   case _ =>

                  }

                case None =>

              }