18 files changed, 141 insertions, 112 deletions
diff --git a/Chalice/tests/refinements/AngelicExec.chalice b/Chalice/tests/refinements/AngelicExec.chalice
index 06ab9c83..582c3944 100644
--- a/Chalice/tests/refinements/AngelicExec.chalice
+++ b/Chalice/tests/refinements/AngelicExec.chalice
@@ -2,7 +2,7 @@ class A0 {
   method m(b: bool) {
     var x;
     if (b) {
-      var x [0 <= x && x < 3];
+      spec x [0 <= x && x < 3];
     } else {
       x := 1;
     }
diff --git a/Chalice/tests/refinements/Answer b/Chalice/tests/refinements/Answer
index 8bd8a24b..aa387295 100644
--- a/Chalice/tests/refinements/Answer
+++ b/Chalice/tests/refinements/Answer
@@ -1,45 +1,50 @@
-Processing LoopSqRoot.chalice
-
-Boogie program verifier finished with 9 verified, 0 errors
-Processing RecSqRoot.chalice
-
-Boogie program verifier finished with 11 verified, 0 errors
-Processing SpecStmt.chalice
-  12.5: Assertion might not hold. The expression at 12.12 might not evaluate to true.
-  25.5: Assertion might not hold. The expression at 25.12 might not evaluate to true.
-  33.5: Assertion might not hold. The expression at 33.12 might not evaluate to true.
-
-Boogie program verifier finished with 4 verified, 3 errors
-Processing SumCubes.chalice
-
-Boogie program verifier finished with 6 verified, 0 errors
-Processing TestTransform.chalice
-
-Boogie program verifier finished with 10 verified, 0 errors
-Processing TestRefines.chalice
-  28.5: Refinement may produce different value for pre-state local variable: c
-
-Boogie program verifier finished with 14 verified, 1 error
-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
-Processing TestCoupling.chalice
-  35.13: The postcondition at 35.13 might not hold. Insufficient fraction at 35.13 for A1.y.
-  62.38: Location might not be readable.
-  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
-Processing AngelicExec.chalice
-  14.5: Refinement may produce different value for a declared local variable: x
-
-Boogie program verifier finished with 11 verified, 1 error
+Processing LoopSqRoot.chalice 
+
+Boogie program verifier finished with 9 verified, 0 errors
+Processing RecSqRoot.chalice 
+
+Boogie program verifier finished with 11 verified, 0 errors
+Processing SpecStmt.chalice 
+  12.5: Assertion might not hold. The expression at 12.12 might not evaluate to true.
+  25.5: Assertion might not hold. The expression at 25.12 might not evaluate to true.
+  33.5: Assertion might not hold. The expression at 33.12 might not evaluate to true.
+
+Boogie program verifier finished with 4 verified, 3 errors
+Processing SumCubes.chalice 
+
+Boogie program verifier finished with 6 verified, 0 errors
+Processing TestTransform.chalice 
+
+Boogie program verifier finished with 10 verified, 0 errors
+Processing TestRefines.chalice 
+  40.5: Refinement may produce a different value for the pre-state local variable: c
+  46.21: Refinement may change a variable outside of the frame of the specification statement: k
+  52.9: Refinement may produce a different value for the pre-state local variable: k
+
+Boogie program verifier finished with 16 verified, 3 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
+Processing TestCoupling.chalice 
+  35.13: The postcondition at 35.13 might not hold. Insufficient fraction at 35.13 for A1.y.
+  62.38: Location might not be readable.
+  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
+Processing AngelicExec.chalice 
+  14.5: Refinement may produce a different value for the declared variable: x
+
+Boogie program verifier finished with 11 verified, 1 error
+Processing RefinesLoop.chalice 
+The program did not typecheck.
+2.1: a refinement cycle detected B->C->A
diff --git a/Chalice/tests/refinements/RefinesLoop.chalice b/Chalice/tests/refinements/RefinesLoop.chalice
new file mode 100644
index 00000000..305fc164
--- /dev/null
+++ b/Chalice/tests/refinements/RefinesLoop.chalice
@@ -0,0 +1,3 @@
+class A refines B {}
+class B refines C {}
+class C refines A {}
diff --git a/Chalice/tests/refinements/SpecStmt.chalice b/Chalice/tests/refinements/SpecStmt.chalice
index 15072d41..55eacdb0 100644
--- a/Chalice/tests/refinements/SpecStmt.chalice
+++ b/Chalice/tests/refinements/SpecStmt.chalice
@@ -16,9 +16,9 @@ class Test {
     requires acc(x);
   {
     x := 0;
-    const y [acc(x), rd(x) && x == old(x) + 1 && y == x];
+    const y [acc(x), acc(x) && x == old(x) + 1 && y == x];
     assert y == 1;
-    const v [rd(x), rd(x) && v == old(x) + 1];
+    const v [acc(x), acc(x) && v == old(x) + 1];
     assert v == 2;
     const z [z == 1];
     ghost var t [z == 1, true];     
diff --git a/Chalice/tests/refinements/TestRefines.chalice b/Chalice/tests/refinements/TestRefines.chalice
index 3081eb90..40f21cea 100644
--- a/Chalice/tests/refinements/TestRefines.chalice
+++ b/Chalice/tests/refinements/TestRefines.chalice
@@ -1,30 +1,56 @@
+// Simple refinements
 class A {
   var x:int;
   function f():int {1}
   method m(i:int) returns (j:int) {
     var j [j > 0];    
   }
+
+  method n() returns (c: bool)
+  {
+    c := true;
+  }
+
+  method o() returns ()
+  {
+    var k := 1;
+    var j := 0;
+    spec j [j > 0];
+  }
+
+  method p(b: bool) returns ()
+  {
+    var k := 1;
+    if (b) {
+    } else {
+    }
+  }
 }
 
-class B refines C {}
-class C refines D {}
-class D refines A {
+class B refines A {
+  // correct
   transforms m(i:int) returns (j:int, k:int) 
   {
   *
   } 
-}
 
-class X {
-  method m() returns (c: bool) 
+  // broken: c
+  refines n() returns (c: bool) 
   {
-    c := true;
+    c := false;
   }
-}
 
-class Y refines X {
-  refines m() returns (c: bool, d: bool)
-  {
-    c := false;
+  // broken: spec stmt frame, k
+  transforms o() returns () {
+    _
+    replaces j by { j := 1; k := 0 }
   }
+
+  // broken: k
+  transforms p(b: bool) returns () {
+    _
+    if {k := 2} else {*}
+  } 
 }
+
+
diff --git a/Chalice/tests/refinements/original/CounterPredicate.chalice b/Chalice/tests/refinements/experiments/CounterPredicate.chalice
index fd35c18c..fd35c18c 100644
--- a/Chalice/tests/refinements/original/CounterPredicate.chalice
+++ b/Chalice/tests/refinements/experiments/CounterPredicate.chalice
diff --git a/Chalice/tests/refinements/original/DSW0.chalice b/Chalice/tests/refinements/experiments/DSW0.chalice
index d83c5438..d83c5438 100644
--- a/Chalice/tests/refinements/original/DSW0.chalice
+++ b/Chalice/tests/refinements/experiments/DSW0.chalice
diff --git a/Chalice/tests/refinements/original/DSW1.chalice b/Chalice/tests/refinements/experiments/DSW1.chalice
index 612f21ac..612f21ac 100644
--- a/Chalice/tests/refinements/original/DSW1.chalice
+++ b/Chalice/tests/refinements/experiments/DSW1.chalice
diff --git a/Chalice/tests/refinements/original/DSW10.chalice b/Chalice/tests/refinements/experiments/DSW10.chalice
index 3bf70eeb..3bf70eeb 100644
--- a/Chalice/tests/refinements/original/DSW10.chalice
+++ b/Chalice/tests/refinements/experiments/DSW10.chalice
diff --git a/Chalice/tests/refinements/original/DSW2.chalice b/Chalice/tests/refinements/experiments/DSW2.chalice
index 7438c688..7438c688 100644
--- a/Chalice/tests/refinements/original/DSW2.chalice
+++ b/Chalice/tests/refinements/experiments/DSW2.chalice
diff --git a/Chalice/tests/refinements/original/DSW3.chalice b/Chalice/tests/refinements/experiments/DSW3.chalice
index dbf161cd..dbf161cd 100644
--- a/Chalice/tests/refinements/original/DSW3.chalice
+++ b/Chalice/tests/refinements/experiments/DSW3.chalice
diff --git a/Chalice/tests/refinements/original/DSW4.chalice b/Chalice/tests/refinements/experiments/DSW4.chalice
index f594595a..f594595a 100644
--- a/Chalice/tests/refinements/original/DSW4.chalice
+++ b/Chalice/tests/refinements/experiments/DSW4.chalice
diff --git a/Chalice/tests/refinements/original/List.chalice b/Chalice/tests/refinements/experiments/List.chalice
index efcec2c8..efcec2c8 100644
--- a/Chalice/tests/refinements/original/List.chalice
+++ b/Chalice/tests/refinements/experiments/List.chalice
diff --git a/Chalice/tests/refinements/original/ListNode.chalice b/Chalice/tests/refinements/experiments/ListNode.chalice
index ae72fe67..ae72fe67 100644
--- a/Chalice/tests/refinements/original/ListNode.chalice
+++ b/Chalice/tests/refinements/experiments/ListNode.chalice
diff --git a/Chalice/tests/refinements/original/ListPredicate.chalice b/Chalice/tests/refinements/experiments/ListPredicate.chalice
index af334093..af334093 100644
--- a/Chalice/tests/refinements/original/ListPredicate.chalice
+++ b/Chalice/tests/refinements/experiments/ListPredicate.chalice
diff --git a/Chalice/tests/refinements/original/StringBuilder.chalice b/Chalice/tests/refinements/experiments/StringBuilder.chalice
index d73f8373..d73f8373 100644
--- a/Chalice/tests/refinements/original/StringBuilder.chalice
+++ b/Chalice/tests/refinements/experiments/StringBuilder.chalice
diff --git a/Chalice/tests/refinements/test.bat b/Chalice/tests/refinements/test.bat
new file mode 100644
index 00000000..986647d6
--- /dev/null
+++ b/Chalice/tests/refinements/test.bat
@@ -0,0 +1,47 @@
+@echo off
+
+REM Regression tests for the refinement extension to Chalice
+REM Author: Kuat Yessenov
+
+setlocal EnableDelayedExpansion
+
+set chalice="%~dp0\..\..\chalice.bat"
+set output=Output
+set answer=Answer
+set parameters="-noTermination"
+set tests=LoopSqRoot,RecSqRoot,SpecStmt,SumCubes,TestTransform,TestRefines,RecFiniteDiff,LoopFiniteDiff,Pick,TestCoupling,Calculator,AngelicExec,RefinesLoop
+
+REM Remove stale output file
+if exist %output% del %output%
+
+echo -------------------------------------
+echo Refinement extension regression tests
+echo -------------------------------------
+
+REM Process each test
+for %%f in (%tests%) do (
+  echo Processing %%f.chalice >> %output%
+  echo Processing %%f
+  
+  if exist out.bpl del out.bpl
+  call %chalice% "%%f.chalice" "%parameters%" >> %output% 2>&1
+)
+
+echo -------------------------------------
+
+REM Compare with the reference
+
+fc %answer% %output% > nul
+if not errorlevel 1 goto passTest
+goto failTest
+
+:passTest
+echo Passed
+if exist %output% del %output%
+if exist out.bpl del out.bpl
+exit /b 0
+
+:failTest
+echo Failed (see Output)
+exit /b 1
+
diff --git a/Chalice/tests/refinements/test.sh b/Chalice/tests/refinements/test.sh
deleted file mode 100644
index 8ebef27a..00000000
--- a/Chalice/tests/refinements/test.sh
+++ /dev/null
@@ -1,52 +0,0 @@
-#!/usr/bin/bash
-
-# Regression tests for refinement extension
-# Author: Kuat Yessenov
-
-TESTS="
-  LoopSqRoot.chalice
-  RecSqRoot.chalice
-  SpecStmt.chalice
-  SumCubes.chalice
-  TestTransform.chalice
-  TestRefines.chalice
-  RecFiniteDiff.chalice
-  LoopFiniteDiff.chalice
-  Pick.chalice
-  TestCoupling.chalice
-  Calculator.chalice
-  AngelicExec.chalice
-"
-
-# Switch to test directory
-CURRENT=`pwd`
-cd `dirname $0`
-
-# Remove stale output file
-if [ -f Output ]
-then
-  rm -f Output
-fi
-
-# Process tests
-START=`date +%s`
-for f in ${TESTS}
-do
-  echo "Processing $f" | tee -a Output
-  scala -cp ../bin chalice.Chalice -nologo -noTermination $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}