20 files changed, 132 insertions, 96 deletions
diff --git a/Chalice/sbt b/Chalice/sbt
index b1dee4bb..b1dee4bb 100644..100755
--- a/Chalice/sbt
+++ b/Chalice/sbt
diff --git a/Chalice/src/main/scala/Chalice.scala b/Chalice/src/main/scala/Chalice.scala
index e49d12a5..6aabcf99 100644
--- a/Chalice/src/main/scala/Chalice.scala
+++ b/Chalice/src/main/scala/Chalice.scala
@@ -157,7 +157,7 @@ object Chalice {
      else if (a.startsWith("-z3opt:") || a.startsWith("/z3opt:"))
             boogieArgs += ("\"/z3opt:" + a.substring(7) + "\"" + " ")
      else if (a.startsWith("-") || a.startsWith("/")) {
-       CommandLineError("unkonwn command line parameter: "+a.substring(1), help)
+       CommandLineError("unknown command line parameter: "+a.substring(1), help)
        return
      }
      else inputs += a
@@ -225,11 +225,14 @@ object Chalice {
            PrintProgram.P(program)
          }
          if (doTranslate) {
-           // checking if Boogie.exe exists
+           // checking if Boogie.exe exists (on non-Linux machine)
            val boogieFile = new File(boogiePath);
-           if(! boogieFile.exists() || ! boogieFile.isFile()) {
-             CommandLineError("Boogie.exe not found at " + boogiePath, help); return
+           if ((! boogieFile.exists() || ! boogieFile.isFile()) 
+            && (System.getProperty("os.name") != "Linux")) {
+             CommandLineError("Boogie.exe not found at " + boogiePath, help); 
+             return;
            }
+           
            // translate program to Boogie
            val translator = new Translator();
            var bplProg: List[Boogie.Decl] = Nil
diff --git a/Chalice/src/main/scala/Resolver.scala b/Chalice/src/main/scala/Resolver.scala
index 9a5d50e8..dee231c8 100644
--- a/Chalice/src/main/scala/Resolver.scala
+++ b/Chalice/src/main/scala/Resolver.scala
@@ -1322,15 +1322,17 @@ object Resolver {
      CheckRunSpecification(e, context, allowMaxLock)
  }
 
- def ResolveTransform(mt: MethodTransform, context: ProgramContext) {
+ def ResolveTransform(mt: MethodTransform, baseContext: ProgramContext) {
+   val context = baseContext.SetClass(mt.Parent).SetMember(mt);
+
    mt.spec foreach {
      case Precondition(e) =>
        context.Error(e.pos, "Method refinement cannot add a pre-condition")
      case Postcondition(e) =>
-       ResolveExpr(e, context.SetClass(mt.Parent).SetMember(mt), true, true)(false)
+       ResolveExpr(e, context, true, true)(false)
      case _ : LockChange => throw new NotSupportedException("not implemented")
    }
-   if (mt.ins != mt.refines.Ins) context.Error(mt.pos, "Refinement must have same input arguments")
+   if (mt.ins != mt.refines.Ins) context.Error(mt.pos, "Refinement must have the same input arguments")
    if (! mt.outs.startsWith(mt.refines.Outs)) context.Error(mt.pos, "Refinement must declare all abstract output variables")
 
    mt.body = AST.refine(mt.refines.Body, mt.trans) match {
@@ -1338,18 +1340,29 @@ object Resolver {
      case AST.Unmatched(t) => context.Error(mt.pos, "Cannot match transform around " + t.pos); Nil
    }
                                 
-   def resolveBody(ss: List[Statement], con: ProgramContext, abs: List[Variable]) {
-     var ctx = con;
-     var locals = abs;
-     for (s <- ss) {
+   /**
+    * We thread two contexts for the concrete and abstract versions.
+    */
+   def resolveBody(ss: List[Statement], 
+     concreteContext: ProgramContext,
+     abstractContext: List[Variable]) {
+     var ctx = concreteContext;
+     var locals = abstractContext;
+     for (s <- ss) { 
        s match {
          case r @ RefinementBlock(c, a) =>
            // abstract globals available at this point in the program
-           r.before = locals
+           r.before = locals;
+
+           // resolve concrete version
            ResolveStmt(BlockStmt(c), ctx)
+
+           // compare declared local variables
            val vs = c flatMap {s => s.Declares};
-           for (v <- a flatMap {s => s.Declares}; if (! vs.contains(v)))
-             ctx.Error(r.pos, "Refinement block must declare a local variable from abstract program: " + v.id)
+           for (s <- a;
+                v <- s.Declares; 
+                if (! vs.contains(v)))
+             ctx.Error(r.pos, "Refinement block must declare a local variable from the abstract program: " + v.id)
          case w @ WhileStmt(guard, oi, ni, lks, body) =>
            for (inv <- ni) {
              ResolveExpr(inv, ctx, true, true)(false)
@@ -1364,8 +1377,9 @@ object Resolver {
            resolveBody(List(els), ctx, locals)
          case BlockStmt(ss) =>
            resolveBody(ss, ctx, locals)
-         case _ =>
+         case _ =>   
        }
+
        // declare concrete and abstract locals
        for (v <- s.Declares) ctx = ctx.AddVariable(v);
        s match {
@@ -1374,7 +1388,8 @@ object Resolver {
        }
      }
    }
-   resolveBody(mt.body, context.SetClass(mt.Parent).SetMember(mt), Nil)
+
+   resolveBody(mt.body, context, mt.refines.Ins ++ mt.refines.Outs)
  }
 
  def ResolveCouplingInvariant(ci: CouplingInvariant, cl: Class, context: ProgramContext) {
diff --git a/Chalice/src/main/scala/Translator.scala b/Chalice/src/main/scala/Translator.scala
index 10cb25bc..e81e7c10 100644
--- a/Chalice/src/main/scala/Translator.scala
+++ b/Chalice/src/main/scala/Translator.scala
@@ -1123,13 +1123,13 @@ class Translator {
     // concrete expression translate
     val conGlobals = etran.FreshGlobals("concrete")
     val conTran = new ExpressionTranslator(conGlobals map {v => new VarExpr(v)}, etran.oldEtran.Globals, currentClass);
-    // shared locals before block (excluding immutable)
+    // shared locals existing before the block (excluding immutable)
     val before = for (v <- r.before; if (! v.isImmutable)) yield v;
-    // shared locals in block
+    // shared locals declared in the block
     val (duringA, duringC) = r.during;
-    // save locals before (to restore for abstract block)
+    // variables for locals before (to restore for the abstract version)
     val beforeV = for (v <- before) yield new Variable(v.id, v.t)
-    // save locals after (to compare with abstract block)
+    // variables for locals after (to compare with the abstract version)
     val afterV = for (v <- before) yield new Variable(v.id, v.t)
 
     Comment("refinement block") ::
@@ -1142,26 +1142,26 @@ class Translator {
     // run concrete C on the fresh heap
     {
       etran = conTran;
-      Comment("run concrete program:") ::
+      Comment("concrete program:") ::
       tag(translateStatements(r.con, todoiparam), keepTag)
     } :::
     // run angelically A on the old heap
-    Comment("run abstract program:") ::
+    Comment("abstract program:") ::
     { etran = absTran;
     r.abs match {
       case List(s: SpecStmt) =>
         var (m, me) = NewBVar("specMask", tmask, true)
 
         tag(
-          Comment("give witnesses to declared local variables") ::
+          Comment("give witnesses to the declared local variables") ::
           (for (v <- duringA) yield BLocal(Variable2BVarWhere(v))) :::
           (for ((v, w) <- duringA zip duringC) yield (new VariableExpr(v) := new VariableExpr(w))) :::
           BLocal(m) ::
           (me := absTran.Mask) ::
-          absTran.Exhale(s.post, me, absTran.Heap, ErrorMessage(r.pos, "Refinement may fail to satisfy specification statement post-condition."), false, todoiparam, todobparam, false) :::
-          absTran.Exhale(s.post, me, absTran.Heap, ErrorMessage(r.pos, "Refinement may fail to satisfy specification statement post-condition."), false, todoiparam, todobparam, true) :::
+          absTran.Exhale(s.post, me, absTran.Heap, ErrorMessage(r.pos, "Refinement may fail to satisfy the specification statement post-condition."), false, todoiparam, todobparam, false) :::
+          absTran.Exhale(s.post, me, absTran.Heap, ErrorMessage(r.pos, "Refinement may fail to satisfy the specification statement post-condition."), false, todoiparam, todobparam, true) :::
           (for ((v, w) <- beforeV zip before; if (! s.lhs.exists(ve => ve.v == w))) yield
-             bassert(new VariableExpr(v) ==@ new VariableExpr(w), r.pos, "Refinement may change a variable not in frame of the specification statement: " + v.id)),
+             bassert(new VariableExpr(v) ==@ new VariableExpr(w), r.pos, "Refinement may change a variable outside of the frame of the specification statement: " + v.id)),
           keepTag)
       case _ =>
         // save locals after
@@ -1173,9 +1173,9 @@ class Translator {
         // assert equality on shared locals
         tag(
           (for ((v, w) <- afterV zip before) yield
-            bassert(new VariableExpr(v) ==@ new VariableExpr(w), r.pos, "Refinement may produce different value for pre-state local variable: " + v.id)) :::
+            bassert(new VariableExpr(v) ==@ new VariableExpr(w), r.pos, "Refinement may produce a different value for the pre-state local variable: " + v.id)) :::
           (for ((v, w) <- duringA zip duringC) yield
-            bassert(new VariableExpr(v) ==@ new VariableExpr(w), r.pos, "Refinement may produce different value for a declared local variable: " + v.id)),
+            bassert(new VariableExpr(v) ==@ new VariableExpr(w), r.pos, "Refinement may produce a different value for the declared variable: " + v.id)),
           keepTag)
     }} :::
     {
@@ -1198,10 +1198,10 @@ class Translator {
       // assert equality on shared globals (except those that are replaced)
       tag(
         for (f <- currentClass.refines.Fields; if ! currentClass.CouplingInvariants.exists(_.fields.contains(f)))
-          yield bassert((absTran.Heap.select(ve, f.FullName) ==@ conTran.Heap.select(ve, f.FullName)).forall(v), r.pos, "Refinement may change value of field " + f.FullName),
+          yield bassert((absTran.Heap.select(ve, f.FullName) ==@ conTran.Heap.select(ve, f.FullName)).forall(v), r.pos, "Refinement may change the value of the field " + f.FullName),
         keepTag)            
     } :::
-    Comment("end of refinement block")
+    Comment("end of the refinement block")
   }
 
   def UpdateMu(o: Expr, allowOnlyFromBottom: Boolean, justAssumeValue: Boolean,
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..b1adc199
--- /dev/null
+++ b/Chalice/tests/refinements/test.bat
@@ -0,0 +1,41 @@
+@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="-smoke -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%
+
+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
+)
+
+REM Compare with the reference
+
+fc %answer% %output% > nul
+if not errorlevel 1 goto passTest
+goto failTest
+
+:passTest
+echo Success
+if exist %output% del %output%
+if exist out.bpl del out.bpl
+exit /b 0
+
+:failTest
+echo Failure
+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}