Chalice: more regression tests; cosmetic changes to code

7 files changed, 124 insertions, 8 deletions

diff --git a/Chalice/refinements/Answer b/Chalice/refinements/Answer
index 0183b442..b513e041 100644
--- a/Chalice/refinements/Answer
+++ b/Chalice/refinements/Answer
@@ -22,3 +22,10 @@ Boogie program verifier finished with 9 verified, 0 errors
 Processing RecFiniteDiff.chalice
 

 Boogie program verifier finished with 9 verified, 0 errors

+Processing LoopFiniteDiff.chalice
+

+Boogie program verifier finished with 12 verified, 0 errors

+Processing Pick.chalice
+  26.25: Sequence index might be larger than or equal to the length of the sequence.

+

+Boogie program verifier finished with 11 verified, 1 error

diff --git a/Chalice/refinements/LoopFiniteDiff.chalice b/Chalice/refinements/LoopFiniteDiff.chalice
new file mode 100644
index 00000000..bd744c89
--- /dev/null
+++ b/Chalice/refinements/LoopFiniteDiff.chalice
@@ -0,0 +1,61 @@
+class Cube0 {
+  method compute(n) 
+    requires n >= 0;   
+  {
+    var v [v == n*n*n];
+  }
+}
+
+class Cube1 refines Cube0 {
+  transforms compute(n) 
+  {
+    replaces v by {
+      var i := 0;
+      var v := 0;
+      while (i < n) 
+        invariant i <= n
+        invariant v == i * i * i
+      {
+        i := i + 1;
+        var v [v == i * i * i];
+      }
+    }
+  }
+}
+
+class Cube2 refines Cube1 {
+  transforms compute(n) 
+  {
+    _    
+    var w := 1;
+    while 
+      invariant w == (i+1)*(i+1)*(i+1) - i*i*i
+    {
+      _
+      replaces v by {        
+        v := v + w;
+        var w [w == (i+1)*(i+1)*(i+1) - i*i*i];
+      }      
+    }
+    _
+  }
+}
+
+class Cube3 refines Cube2 {
+  transforms compute(n)
+  {
+    _    
+    var x := 0;
+    while    
+      invariant x == i*i 
+    {
+      _
+      replaces w by {        
+        x := x + 2*i - 1;      
+        w := 3*x + 3*i + 1;
+      } 
+    }
+    _
+  }
+}
+
diff --git a/Chalice/refinements/Pick.chalice b/Chalice/refinements/Pick.chalice
new file mode 100644
index 00000000..7df2f90d
--- /dev/null
+++ b/Chalice/refinements/Pick.chalice
@@ -0,0 +1,28 @@
+class Pick0 {
+  method pick(s: seq<int>) returns (x)
+    requires |s| > 0;
+  {
+    var x [x in s]
+  }
+}
+
+class Pick1 refines Pick0 {
+  transforms pick(s: seq<int>) returns (x)
+  {
+    replaces x by {x := s[0]}
+  }
+}
+
+class Pick2 refines Pick0 {
+  transforms pick(s: seq<int>) returns (x)
+  {
+    replaces * by {x := s[|s|-1]}
+  }
+}
+
+class Pick3 refines Pick0 {
+  transforms pick(s: seq<int>) returns (x)
+  {
+    replaces x by {x := s[1]}
+  }
+}
diff --git a/Chalice/refinements/RecFiniteDiff.chalice b/Chalice/refinements/RecFiniteDiff.chalice
index 8fca8d9b..1a971aed 100644
--- a/Chalice/refinements/RecFiniteDiff.chalice
+++ b/Chalice/refinements/RecFiniteDiff.chalice
@@ -35,7 +35,8 @@ class Cube2 refines Cube1 {
     ensures x == (n+1)*(n+1);   
   { 
     if {
-      _; x := 1;
+      _
+      x := 1;
     } else {
       replaces v1, w1 by {
         call v1,w1,x1 := compute(n-1);
diff --git a/Chalice/refinements/test.sh b/Chalice/refinements/test.sh
index a9ac7b82..73ede390 100644
--- a/Chalice/refinements/test.sh
+++ b/Chalice/refinements/test.sh
@@ -1,5 +1,8 @@
 #!/usr/bin/bash
 
+# Regression tests for refinement extension
+# Author: Kuat Yessenov
+
 TESTS="
   LoopSqRoot.chalice
   RecSqRoot.chalice
@@ -8,23 +11,39 @@ TESTS="
   TestTransform.chalice
   TestRefines.chalice
   RecFiniteDiff.chalice
+  LoopFiniteDiff.chalice
+  Pick.chalice
 "
+
+# Switch to test directory
+CURRENT=`pwd`
+cd `dirname $0`
+
+# Remove stale output file
 if [ -f Output ]
 then
   rm -f Output
 fi
 
-for f in $TESTS 
+# Process tests
+START=`date +%s`
+for f in ${TESTS}
 do
   echo "Processing $f" | tee -a Output
   scala -cp ../bin chalice.Chalice -nologo $f >> Output 2>&1
 done
+END=`date +%s`
+echo "Time: $(( $END - $START )) seconds"
 
+# Compare with answer
 if diff Output Answer
 then
+  rm Output
+  rm out.bpl
   echo Success
 else
   echo Failure
 fi
 
-  
+# Switch back to current directory
+cd ${CURRENT}
diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala
index cbb2ac85..f5c2d1b4 100644
--- a/Chalice/src/Ast.scala
+++ b/Chalice/src/Ast.scala
@@ -241,9 +241,9 @@ case class SeqPat(pats: List[Transform]) extends Transform {
 }

 case class RefinementBlock(con: List[Statement], abs: List[Statement]) extends Statement {

   if (con.size > 0) pos = con.first.pos;

-  // existing local variables before the block

+  // local variables in context at the beginning of the block

   var before: List[Variable] = null;

-  // shared declared local variables

+  // shared declared local variables (mapping between abstract and concrete)

   lazy val during: (List[Variable], List[Variable]) = {

     val a = for (v <- abs.flatMap(s => s.Declares)) yield v;

     val c = for (v <- a) yield con.flatMap(s => s.Declares).find(_ == v).get

@@ -266,7 +266,7 @@ case class BlockStmt(ss: List[Statement]) extends Statement {
   override def Targets = (ss :\ Set[Variable]()) { (s, vars) => vars ++ s.Targets}

 }

 case class IfStmt(guard: Expression, thn: BlockStmt, els: Option[Statement]) extends Statement {

-  override def Targets = thn.Targets ++ (els match {case None => Set(); case Some(els) => els.Targets}) 

+  override def Targets = thn.Targets ++ (els match {case None => Set(); case Some(els) => els.Targets})

 }

 case class WhileStmt(guard: Expression,

                      oldInvs: List[Expression], newInvs: List[Expression], lkch: List[Expression], 

@@ -552,7 +552,7 @@ object AST {
         case x => List(x)

       }}

       def noTwoBlocks: List[Transform] => List[Transform] = {

-        case BlockPat() :: BlockPat() :: l => noTwoBlocks(BlockPat() :: l)

+        case BlockPat() :: (bp @ BlockPat()) :: l => noTwoBlocks(bp :: l)

         case x :: l => x :: noTwoBlocks(l)

         case Nil => Nil

       }

diff --git a/Chalice/src/PrettyPrinter.scala b/Chalice/src/PrettyPrinter.scala
index 30cfb66f..b2fd4e1b 100644
--- a/Chalice/src/PrettyPrinter.scala
+++ b/Chalice/src/PrettyPrinter.scala
@@ -95,7 +95,7 @@ object PrintProgram {
       }

       for (inv <- w.newInvs) {

         Spaces(indent+2)

-        print("invariant "); Expr(inv); print(" // refined"); println(Semi)

+        print("invariant "); Expr(inv); print(Semi); println(" // refined");

       }

       for (l <- lkch) {

         Spaces(indent+2)