Semi-automatic merge.

35 files changed, 1384 insertions, 307 deletions

diff --git a/Chalice/chalice.bat b/Chalice/chalice.bat
index 62fdb308..e4bbf5da 100644
--- a/Chalice/chalice.bat
+++ b/Chalice/chalice.bat
@@ -1,5 +1,54 @@
 @echo off

+SetLocal EnableDelayedExpansion

 

-call scala -cp "%~dp0\target\scala-2.8.1.final\classes" chalice.Chalice /boogieOpt:nologo %*

+set ROOT_DIR=%~dp0

+set JAVA_EXE=java 

+

+REM Attention: 'where' might not be available on all Windows versions

+call where %JAVA_EXE% > NUL

+if not %ERRORLEVEL%==0 (

+	echo Java could not be started.

+	goto :exit_with_error

+)

+

+REM Get the Scala version, or rather, a string such as "scala-2.8.1"

+for /f "delims=" %%A in ('dir /b %ROOT_DIR%\project\boot\scala-*') do @set SCALA_DIR=%%A

+

+REM Set classpath elements

+set __CP.SCALA_LIB=%ROOT_DIR%\project\boot\%SCALA_DIR%\lib\scala-library.jar

+set __CP.CHALICE=%ROOT_DIR%\target\%SCALA_DIR%.final\classes

+

+REM Assemble classpath and check if all classpath elements exist

+set CP=

+for /f "tokens=2* delims=.=" %%A in ('set __CP.') do (

+	REM echo %%A %%B

+	if not exist %%B (

+		echo %%B does not exist.

+		goto :exit_with_error

+	) else (

+		set CP=!CP!;%%B

+	)

+)

+

+REM Chalice main class

+set CHALICE_MAIN=chalice.Chalice

+

+REM Chalice command line options

+set CHALICE_OPTS=

+set CHALICE_OPTS=%CHALICE_OPTS% /boogieOpt:nologo

+set CHALICE_OPTS=%CHALICE_OPTS% %*

+

+REM Assemble main command

+set CMD=%JAVA_EXE% -cp %CP% -Xss16M %CHALICE_MAIN% %CHALICE_OPTS%

+

+REM echo.

+REM echo %CMD%

+REM echo.

+

+call %CMD%

 

 exit /B 0

+

+

+:exit_with_error

+exit /B 1

diff --git a/Chalice/readme.txt b/Chalice/readme.txt
index 37998339..f282da3c 100644
--- a/Chalice/readme.txt
+++ b/Chalice/readme.txt
@@ -4,6 +4,11 @@ Chalice - Verification of Concurrent Software
 

 Compiling Chalice: sbt compile

 Running Chalice: chalice.bat <file.chalice> [-params]

+  By default, chalice looks for Boogie in C:\Boogie\Binaries. If your

+  Boogie executable is located elsewhere, you can edit chalice.bat

+  to indicate the appropriate location such as 

+    REM Chalice command line options

+    set CHALICE_OPTS=/boogie:"C:\Boogie-CodePlex\Binaries\Boogie.exe"

 Running the tests for Chalice: see tests/readme.txt

 

 Chalice is built using Simple Build Tool (https://github.com/harrah/xsbt/wiki/Setup)

diff --git a/Chalice/sbt b/Chalice/sbt
index b1dee4bb..b1dee4bb 100644..100755
--- a/Chalice/sbt
+++ b/Chalice/sbt
diff --git a/Chalice/sbt.bat b/Chalice/sbt.bat
index e43e99b9..4c92a4b3 100644
--- a/Chalice/sbt.bat
+++ b/Chalice/sbt.bat
@@ -1,3 +1,5 @@
 @ECHO OFF

+SetLocal

+

 set SCRIPT_DIR=%~dp0

-java -XX:MaxPermSize=256m -Xmx512M -Xss2M -jar "%SCRIPT_DIR%sbt-launch.jar" %*

+java %JAVA_OPTS% -XX:MaxPermSize=256m -Xmx512M -Xss2M -jar "%SCRIPT_DIR%sbt-launch.jar" %*

diff --git a/Chalice/scripts/create_release/README.TXT b/Chalice/scripts/create_release/README.TXT
new file mode 100644
index 00000000..b416a241
--- /dev/null
+++ b/Chalice/scripts/create_release/README.TXT
@@ -0,0 +1,3 @@
+This script is invoked by Aste (the build tool creating Chalice nightlies). Hence, don't move it to another location!

+

+The script will be replaced with an sbt action sooner or later anyway.
\ No newline at end of file
diff --git a/Chalice/scripts/create_release/create_release.bat b/Chalice/scripts/create_release/create_release.bat
new file mode 100644
index 00000000..a0d67fd9
--- /dev/null
+++ b/Chalice/scripts/create_release/create_release.bat
@@ -0,0 +1,24 @@
+@echo off

+SetLocal

+

+set BASE_DIR=%~dp0\..\..

+

+set RELEASE_DIR_SRC=%~dp0\files

+set RELEASE_DIR_DST=%~dp0\release

+

+set CHALICE_JAR_SRC=%BASE_DIR%\target\scala-2.8.1.final\chalice_2.8.1-1.0.jar

+set CHALICE_JAR_DST=%RELEASE_DIR_DST%\chalice.jar

+

+pushd %BASE_DIR%

+call sbt.bat package

+

+popd

+

+if exist "%RELEASE_DIR_DST%" rmdir /S /Q "%RELEASE_DIR_DST%"

+mkdir "%RELEASE_DIR_DST%"

+

+copy "%CHALICE_JAR_SRC%" "%CHALICE_JAR_DST%"

+copy "%RELEASE_DIR_SRC%\*.*" "%RELEASE_DIR_DST%"

+copy "%RELEASE_DIR_SRC%\*.*" "%RELEASE_DIR_DST%"

+

+xcopy %BASE_DIR%\tests\examples %RELEASE_DIR_DST%\examples\
\ No newline at end of file
diff --git a/Chalice/scripts/create_release/files/chalice.bat b/Chalice/scripts/create_release/files/chalice.bat
new file mode 100644
index 00000000..d70d05b8
--- /dev/null
+++ b/Chalice/scripts/create_release/files/chalice.bat
@@ -0,0 +1,5 @@
+@echo off

+

+call scala -cp chalice.jar chalice.Chalice /boogieOpt:nologo %*

+

+exit /B 0

diff --git a/Chalice/src/main/scala/Ast.scala b/Chalice/src/main/scala/Ast.scala
index 78d2ac74..c2ee009f 100644
--- a/Chalice/src/main/scala/Ast.scala
+++ b/Chalice/src/main/scala/Ast.scala
@@ -238,13 +238,16 @@ case class LockChange(ee: List[Expression]) extends Specification
 

 case class CouplingInvariant(ids: List[String], e: Expression) extends Member {

   assert(ids.size > 0)

-  var fields = Nil:List[Field]

+  var fields: List[Field] = Nil

   /* Distribute 100 between fields */

-  def fraction(field: Field) = {

+  def fraction(field: Field): Permission = {

     val k = fields.indexOf(field)

     assert (0 <= k && k < fields.size)

     val part: Int = 100 / fields.size

-    if (k == fields.size - 1) IntLiteral(100 - part * k) else IntLiteral(part)          

+    if (k == fields.size - 1) 

+      Frac(IntLiteral(100 - part * k)) 

+    else 

+      Frac(IntLiteral(part)          )

   }

 }

 case class MethodTransform(id: String, ins: List[Variable], outs: List[Variable], spec: List[Specification], trans: Transform) extends Callable(id) {

diff --git a/Chalice/src/main/scala/Boogie.scala b/Chalice/src/main/scala/Boogie.scala
index 6f18694d..acc061ad 100644
--- a/Chalice/src/main/scala/Boogie.scala
+++ b/Chalice/src/main/scala/Boogie.scala
@@ -213,6 +213,9 @@ object Boogie {
        val r = assert.pos.line;

        val c = assert.pos.column;

        r + "," + c + "," + r + "," + (c+5) + ":"

+     } else if (Chalice.rise4funMode) {

+       val (r,c) = (assert.pos.line, assert.pos.column)

+       Chalice.InputFilename + "(" + r + "," + c + "): Error: "

      } else {

        "  " + assert.pos + ": "

      }

diff --git a/Chalice/src/main/scala/Chalice.scala b/Chalice/src/main/scala/Chalice.scala
index e49d12a5..cc06ad7b 100644
--- a/Chalice/src/main/scala/Chalice.scala
+++ b/Chalice/src/main/scala/Chalice.scala
@@ -17,6 +17,8 @@ object Chalice {
    * Reporting options

    */

   private[chalice] var vsMode = false;

+  private[chalice] var rise4funMode = false;

+  private[chalice] var InputFilename = "";  // the name of the last input file mentioned on the command line, or "" if none

 

   /**

    * Translation options

@@ -40,35 +42,53 @@ object Chalice {
   private[chalice] var smoke = false;

   private[chalice] var smokeAll = false;

 

-  def main(args: Array[String]): Unit = {

-    var boogiePath = "C:\\boogie\\Binaries\\Boogie.exe"

-    val inputs = new ListBuffer[String]()

-    var printProgram = false

-    var doTypecheck = true

-    var doTranslate = true

-    var boogieArgs = " ";

-    var gen = false;

-    var showFullStackTrace = false

-

+  /**

+   * Holds all command line arguments not stored in fields of Chalice.

+   * Can only be created parseCommandLine.

+   */

+  sealed abstract class CommandLineParameters {

+    val boogiePath: String 

+    val files: List[File]

+    val printProgram: Boolean 

+    val doTypecheck: Boolean 

+    val doTranslate: Boolean 

+    val boogieArgs: String 

+    val gen: Boolean

+    val showFullStackTrace: Boolean

+    def getHelp(): String

+  }

+  

+  def parseCommandLine(args: Array[String]): Option[CommandLineParameters] = {

     // help texts and closures for boolean command line options

     // closures should be idempotent

     import scala.collection.immutable.ListMap

+    

+    var aBoogiePath = "C:\\boogie\\Binaries\\Boogie.exe"

+    val inputs = new ListBuffer[String]()

+    var aPrintProgram = false

+    var aDoTypecheck = true

+    var aDoTranslate = true

+    var aBoogieArgs = " ";

+    var aGen = false;

+    var aShowFullStackTrace = false

+    

     val options = ListMap[String,(() => Unit, String)](

      "help" -> (

        {() => },

        "print this message"),

-     "print" -> (

-       {() => printProgram = true},

-       "print intermediate versions of the Chalice program"),

+     "print" -> ({() => aPrintProgram = true},"print intermediate versions of the Chalice program"),

      "noTranslate" -> (

-       {() => doTranslate = false},

+       {() => aDoTranslate = false},

        "do not translate the program to Boogie (only parse and typecheck)"),

      "noTypecheck"-> (

-       {() => doTypecheck = false},

+       {() => aDoTypecheck = false},

        "do not typecheck the program (only parse). Implies /noTranslate."),

      "vs" -> (

        {() => vsMode = true},

        "Microsoft Visual Studio mode (special error reporting for Visual Studio; requires an existing, writable directory at C:\\tmp)"),

+     "rise4fun" -> (

+       {() => rise4funMode = true},

+       "rise4fun mode (generates error messages in a format expected by the rise4fun harness"),

      "checkLeaks" -> (

        {() => checkLeaks = true},

        "(no description available)"),

@@ -82,7 +102,7 @@ object Chalice {
        {() => defaults = 3},

        null),

      "gen" -> (

-       {() => gen = true},

+       {() => aGen = true},

        "generate C# code from the Chalice program"),

      "autoFold" -> (

        {() => autoFold = true},

@@ -94,7 +114,7 @@ object Chalice {
        {() => noFreeAssume = true},

        "(no description available)"),

      "showFullStackTrace" -> (

-       {() => showFullStackTrace = true},

+       {() => aShowFullStackTrace = true},

        "show the full stack trace if an exception is encountered"),

      "smoke" -> (

        {() => smoke = true},

@@ -130,9 +150,9 @@ object Chalice {
     }

     

     for (a <- args) {

-     if (a == "/help" || a == "-help") {Console.out.println(help); return}

+     if (a == "/help" || a == "-help") {Console.out.println(help); return None}

      else if ((a.startsWith("-") || a.startsWith("/")) && (options contains a.substring(1))) options(a.substring(1))._1()

-     else if (a.startsWith("/boogie:") || a.startsWith("-boogie:")) boogiePath = a.substring(8)

+     else if (a.startsWith("/boogie:") || a.startsWith("-boogie:")) aBoogiePath = a.substring(8)

      else if (a.startsWith("/defaults:") || a.startsWith("-defaults:")) {

        try {

          defaults = Integer.parseInt(a.substring(10));

@@ -147,18 +167,18 @@ object Chalice {
        } catch { case _ => CommandLineError("/percentageSupport takes integer argument", help); }

      }

      else if (a.startsWith("-boogieOpt:") || a.startsWith("/boogieOpt:"))

-            boogieArgs += ("\"/" + a.substring(11) + "\"" + " ")

+            aBoogieArgs += ("\"/" + a.substring(11) + "\"" + " ")

      else if (a.startsWith("-bo:") || a.startsWith("/bo:"))

-            boogieArgs += ("\"/" + a.substring(4) + "\"" + " ")

+            aBoogieArgs += ("\"/" + a.substring(4) + "\"" + " ")

                 /* [MHS] Quote whole argument to not confuse Boogie with arguments that

                  * contain spaces, e.g. if Chalice is invoked as

                  *   chalice -z3exe:"C:\Program Files\z3\z3.exe" program.chalice

                  */

      else if (a.startsWith("-z3opt:") || a.startsWith("/z3opt:"))

-            boogieArgs += ("\"/z3opt:" + a.substring(7) + "\"" + " ")

+            aBoogieArgs += ("\"/z3opt:" + a.substring(7) + "\"" + " ")

      else if (a.startsWith("-") || a.startsWith("/")) {

-       CommandLineError("unkonwn command line parameter: "+a.substring(1), help)

-       return

+       CommandLineError("unknown command line parameter: "+a.substring(1), help)

+       return None

      }

      else inputs += a

     }

@@ -166,7 +186,7 @@ object Chalice {
     // for smoke testing, we want to see all failing assertions, so we use no

     // error limit (or a very high one), and turn the subsumption option off

     if (smoke) {

-      boogieArgs += ("\"-errorLimit:10000\" ")

+      aBoogieArgs += ("\"-errorLimit:10000\" ")

     }

     

     percentageSupport match {

@@ -177,15 +197,33 @@ object Chalice {
     }

 

     // check that input files exist

-    var files = for (input <- inputs.toList) yield {

+    var aFiles = for (input <- inputs.toList) yield {

      val file = new File(input);

      if(! file.exists) {

        CommandLineError("input file " + file.getName() + " could not be found", help);

-       return

+       return None;

      }

+     InputFilename = input

      file;

     }

-

+    

+    Some(new CommandLineParameters{

+        val boogiePath = aBoogiePath 

+        val files = aFiles 

+        val printProgram = aPrintProgram 

+        val doTypecheck = aDoTypecheck 

+        val doTranslate = aDoTranslate 

+        val boogieArgs = aBoogieArgs 

+        val gen = aGen 

+        val showFullStackTrace = aShowFullStackTrace

+        def getHelp(): String = help

+    })

+  }

+  

+  def parsePrograms(params: CommandLineParameters): Option[List[TopLevelDecl]] = {

+    val files = params.files;

+    val printProgram = params.printProgram;

+    

     // parse programs

     val parser = new Parser();

     val parseResults = if (files.isEmpty) {

@@ -211,107 +249,145 @@ object Chalice {
        if (printProgram) PrintProgram.P(pprog)

        pprog

     }).flatten;

-    if (parseErrors) return;

-

+    if (parseErrors) 

+        None

+      else

+        Some(program)

+  }

+  

+  def typecheckProgram(params: CommandLineParameters, program: List[TopLevelDecl]): Boolean = {

     // typecheck program

-    if (doTypecheck) {

-     Resolver.Resolve(program) match {

-       case Resolver.Errors(msgs) =>

-         if (!vsMode) Console.err.println("The program did not typecheck.");

-         msgs foreach { msg => ReportError(msg._1, msg._2) }

-       case Resolver.Success() =>

-         if (printProgram) {

-           Console.out.println("Program after type checking: ");

-           PrintProgram.P(program)

-         }

-         if (doTranslate) {

-           // checking if Boogie.exe exists

-           val boogieFile = new File(boogiePath);

-           if(! boogieFile.exists() || ! boogieFile.isFile()) {

-             CommandLineError("Boogie.exe not found at " + boogiePath, help); return

-           }

-           // translate program to Boogie

-           val translator = new Translator();

-           var bplProg: List[Boogie.Decl] = Nil

-           try {

-             bplProg = translator.translateProgram(program);

-           } catch {

-             case e:InternalErrorException => {

-               if (showFullStackTrace) {

-                 e.printStackTrace()

-                 Console.err.println()

-                 Console.err.println()

-               }

-               CommandLineError("Internal error: " + e.msg, help)

-               return

-             }

-             case e:NotSupportedException => {

-               if (showFullStackTrace) {

-                 e.printStackTrace()

-                 Console.err.println()

-                 Console.err.println()

-               }

-               CommandLineError("Not supported: " + e.msg, help)

-               return

-             }

-           }

-           // write to out.bpl

-           val bplText = TranslatorPrelude.P + (bplProg map Boogie.Print).foldLeft(""){ (a, b) => a + b };

-           val bplFilename = if (vsMode) "c:\\tmp\\out.bpl" else "out.bpl"

-           writeFile(bplFilename, bplText);

-           // run Boogie.exe on out.bpl

-           val boogie = Runtime.getRuntime.exec(boogiePath + " /errorTrace:0 " + boogieArgs + bplFilename);

-           // terminate boogie if interrupted

-           Runtime.getRuntime.addShutdownHook(new Thread(new Runnable() {

-             def run {

-               try {

-                 val kill = Runtime.getRuntime.exec("taskkill /T /F /IM Boogie.exe");

-                 kill.waitFor;

-               } catch {case _ => }

-               // just to be sure

-               boogie.destroy

-             }

-           }))

-           // the process blocks until we exhaust input and error streams

-           new Thread(new Runnable() {

-             def run {

-               val err = new BufferedReader(new InputStreamReader(boogie.getErrorStream));

-               var line = err.readLine;

-               while(line!=null) {Console.err.println(line); Console.err.flush}

-             }

-           }).start;

-           val input = new BufferedReader(new InputStreamReader(boogie.getInputStream));

-           var line = input.readLine();

-           var previous_line = null: String;

-           val boogieOutput: ListBuffer[String] = new ListBuffer()

-           while (line!=null){

-             if (!smoke) {

-               Console.out.println(line);

-               Console.out.flush;

-             }

-             boogieOutput += line

-             previous_line = line;

-             line = input.readLine();

-           }

-           boogie.waitFor;

-           input.close;

-           

-           // smoke test output

-           if (smoke) {

-             val output = SmokeTest.processBoogieOutput(boogieOutput.toList)

-             Console.out.println(output);

-             Console.out.flush;

-           }

+    Resolver.Resolve(program) match {

+     case Resolver.Errors(msgs) =>

+       if (!vsMode) Console.err.println("The program did not typecheck.");

+       msgs foreach { msg => ReportError(msg._1, msg._2) };

+       false;

+     case Resolver.Success() =>

+       true

+    }

+  }

+  

+  def main(args: Array[String]): Unit = {

 

-           // generate code

-           if(gen && (previous_line != null) && previous_line.endsWith(" 0 errors")) { // hack

-             val converter = new ChaliceToCSharp();

-             println("Code generated in out.cs.");

-             writeFile("out.cs", converter.convertProgram(program));

-           }

-         }

-     }

+    //Parse command line arguments

+    val params = parseCommandLine(args) match {

+      case Some(p) => p

+      case None => return //invalid arguments, help has been displayed

+    }

+

+    val program = parsePrograms(params) match {

+      case Some(p) => p

+      case None => return //illegal program, errors have already been displayed

+    }

+

+    if(!params.doTypecheck || !typecheckProgram(params, program))

+      return ;

+    

+    if (params.printProgram) {

+      Console.out.println("Program after type checking: ");

+      PrintProgram.P(program)

     }

+    

+    if(!params.doTranslate)

+      return;

+    

+    // checking if Boogie.exe exists (on non-Linux machine)

+    val boogieFile = new File(params.boogiePath);

+    if(! boogieFile.exists() || ! boogieFile.isFile()

+            && (System.getProperty("os.name") != "Linux")) {

+      CommandLineError("Boogie.exe not found at " + params.boogiePath, params.getHelp()); 

+      return;

+    }

+    

+    val showFullStackTrace = params.showFullStackTrace

+    val boogiePath = params.boogiePath

+    val boogieArgs = params.boogieArgs

+    

+    // translate program to Boogie

+    val translator = new Translator();

+    var bplProg: List[Boogie.Decl] = Nil

+    try {

+      bplProg = translator.translateProgram(program);

+    } catch {

+      case e:InternalErrorException => {

+        if (showFullStackTrace) {

+          e.printStackTrace()

+          Console.err.println()

+          Console.err.println()

+        }

+        CommandLineError("Internal error: " + e.msg, params.getHelp())

+        return

+      }

+      case e:NotSupportedException => {

+        if (showFullStackTrace) {

+          e.printStackTrace()

+          Console.err.println()

+          Console.err.println()

+        }

+        CommandLineError("Not supported: " + e.msg, params.getHelp())

+        return

+      }

+    }

+    

+    

+    // write to out.bpl

+    val bplText = TranslatorPrelude.P + (bplProg map Boogie.Print).foldLeft(""){ (a, b) => a + b };

+    val bplFilename = if (vsMode) "c:\\tmp\\out.bpl" else "out.bpl"

+    writeFile(bplFilename, bplText);

+    // run Boogie.exe on out.bpl

+    val boogie = Runtime.getRuntime.exec(boogiePath + " /errorTrace:0 " + boogieArgs + bplFilename);

+    // terminate boogie if interrupted

+    Runtime.getRuntime.addShutdownHook(new Thread(new Runnable() {

+      def run {

+        try {

+          val kill = Runtime.getRuntime.exec("taskkill /T /F /IM Boogie.exe");

+          kill.waitFor;

+        } catch {case _ => }

+        // just to be sure

+        boogie.destroy

+      }

+    }))

+    // the process blocks until we exhaust input and error streams

+    new Thread(new Runnable() {

+      def run {

+        val err = new BufferedReader(new InputStreamReader(boogie.getErrorStream));

+        var line = err.readLine;

+        while(line!=null) {Console.err.println(line); Console.err.flush}

+      }

+    }).start;

+    val input = new BufferedReader(new InputStreamReader(boogie.getInputStream));

+    var line = input.readLine();

+    var previous_line = null: String;

+    val boogieOutput: ListBuffer[String] = new ListBuffer()

+    while (line!=null){

+      if (!smoke) {

+        Console.out.println(line);

+        Console.out.flush;

+      }

+      boogieOutput += line

+      previous_line = line;

+      line = input.readLine();

+    }

+    boogie.waitFor;

+    input.close;

+    

+    // smoke test output

+    if (smoke) {

+      val output = SmokeTest.processBoogieOutput(boogieOutput.toList)

+      Console.out.println(output);

+      Console.out.flush;

+    }

+   

+    // generate code

+    if(params.gen && (previous_line != null) && previous_line.endsWith(" 0 errors")) { // hack

+      generateCSharpCode(params, program)

+    }

+  }

+  

+  def generateCSharpCode(params: CommandLineParameters, program: List[TopLevelDecl]): Unit = {    

+      val converter = new ChaliceToCSharp();

+      println("Code generated in out.cs.");

+      writeFile("out.cs", converter.convertProgram(program));

   }

 

   def writeFile(filename: String, text: String) {

diff --git a/Chalice/src/main/scala/Resolver.scala b/Chalice/src/main/scala/Resolver.scala
index 17bb668e..4f812038 100644
--- a/Chalice/src/main/scala/Resolver.scala
+++ b/Chalice/src/main/scala/Resolver.scala
@@ -226,10 +226,21 @@ object Resolver {
              ResolveExpr(e, ctx, false, true)(true);

              if(!e.typ.IsBool) context.Error(e.pos, "predicate requires a boolean expression (found " + e.typ.FullName + ")")

            case f@Function(id, ins, out, spec, definition) =>

-              // TODO: disallow credit(...) expressions in function specifications

+             def hasCredit(e: Expression) = {

+               var b = false

+               e transform {

+                 case _:Credit => b = true; None

+                 case _ => None

+               }

+               b

+             }

              spec foreach {

-               case Precondition(e) => ResolveExpr(e, context, false, true)(false)

-               case Postcondition(e) => ResolveExpr(e, context, false, true)(false)

+               case p@Precondition(e) =>

+                 ResolveExpr(e, context, false, true)(false)

+                 if (hasCredit(e)) context.Error(p.pos, "the specification of functions cannot contain credit expressions") 

+               case p@Postcondition(e) =>

+                 ResolveExpr(e, context, false, true)(false)

+                 if (hasCredit(e)) context.Error(p.pos, "the specification of functions cannot contain credit expressions") 

                case lc : LockChange => context.Error(lc.pos, "lockchange not allowed on function") 

              }

 

@@ -1314,15 +1325,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 {

@@ -1330,18 +1343,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)

@@ -1356,8 +1380,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 {

@@ -1366,7 +1391,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 c2019b12..7d53dd2b 100644
--- a/Chalice/src/main/scala/Translator.scala
+++ b/Chalice/src/main/scala/Translator.scala
@@ -408,37 +408,44 @@ class Translator {
     }

   }

 

-  // TODO: This method has not yet been updated to the new permission model

   def translateMethodTransform(mt: MethodTransform): List[Decl] = {

-    // extract coupling invariants

-    def Invariants(e: Expression): Expression = desugar(e) match {

-      case And(a,b) => And(Invariants(a), Invariants(b))

-      case Implies(a,b) => Implies(a, Invariants(b))

+    // extract coupling invariants from the class pool of invariants

+    val pool = mt.Parent.CouplingInvariants

+

+    def extractInv(e: Expression): Expression = desugar(e) match {

+      case And(a,b) => And(extractInv(a), extractInv(b))

+      case Implies(a,b) => Implies(a, extractInv(b))

       case Access(ma, Full) if ! ma.isPredicate =>

-        val cis = for (ci <- mt.Parent.CouplingInvariants; if (ci.fields.contains(ma.f))) yield FractionOf(ci.e, ci.fraction(ma.f));

-        cis.foldLeft(BoolLiteral(true):Expression)(And(_,_))

+        {for (ci <- pool; 

+          if (ci.fields.contains(ma.f))) 

+          yield scaleExpressionByPermission(ci.e, ci.fraction(ma.f), ma.pos)}.foldLeft(BoolLiteral(true):Expression)(And(_,_))

       case _: PermissionExpr => throw new NotSupportedException("not supported")

       case _ => BoolLiteral(true)

     }

 

-    val preCI = if (mt.Parent.CouplingInvariants.size > 0) Preconditions(mt.Spec).map(Invariants) else Nil

-    val postCI = if (mt.Parent.CouplingInvariants.size > 0) Postconditions(mt.refines.Spec).map(Invariants) else Nil

+    val preCI = Preconditions(mt.Spec).map(extractInv)

+    val postCI = Postconditions(mt.refines.Spec).map(extractInv)

 

+    // pick new k for this method, that represents the fraction for read permissions

+    val (methodKV, methodK) = Boogie.NewBVar("methodK", tint, true)

+    val methodKStmts = BLocal(methodKV) :: bassume(0 < methodK && 1000*methodK < permissionOnePercent)

+ 

     // check definedness of refinement specifications

     Proc(mt.FullName + "$checkDefinedness",

       NewBVarWhere("this", new Type(currentClass)) :: (mt.Ins map {i => Variable2BVarWhere(i)}),

       mt.Outs map {i => Variable2BVarWhere(i)},

       GlobalNames,

       DefaultPrecondition(),

+        methodKStmts :::

         DefinePreInitialState :::

         bassume(CanAssumeFunctionDefs) ::

         // check precondition

-        InhaleWithChecking(Preconditions(mt.Spec) ::: preCI, "precondition", todoiparam) :::

+        InhaleWithChecking(Preconditions(mt.Spec) ::: preCI, "precondition", methodK) :::

         DefineInitialState :::

         resetState(etran) :::

         // check postcondition

-        InhaleWithChecking(Postconditions(mt.refines.Spec), "postcondition", todoiparam) :::

-        tag(InhaleWithChecking(postCI ::: Postconditions(mt.spec), "postcondition", todoiparam), keepTag)

+        InhaleWithChecking(Postconditions(mt.refines.Spec), "postcondition", methodK) :::

+        tag(InhaleWithChecking(postCI ::: Postconditions(mt.spec), "postcondition", methodK), keepTag)

       ) ::

     // check correctness of refinement

     Proc(mt.FullName,

@@ -446,17 +453,18 @@ class Translator {
       mt.Outs map {i => Variable2BVarWhere(i)},

       GlobalNames,

       DefaultPrecondition(),

+        methodKStmts ::: 

         assert2assume {

           bassume(CurrentModule ==@ Boogie.VarExpr(ModuleName(currentClass))) ::

           bassume(CanAssumeFunctionDefs) ::

           DefinePreInitialState :::

-          Inhale(Preconditions(mt.Spec) ::: preCI, "precondition", todoiparam) :::

+          Inhale(Preconditions(mt.Spec) ::: preCI, "precondition", methodK) :::

           DefineInitialState :::

-          translateStatements(mt.body, todoiparam) :::

-          Exhale(Postconditions(mt.refines.Spec) map {p => (p, ErrorMessage(p.pos, "The postcondition at " + p.pos + " might not hold."))}, "postcondition", todoiparam, todobparam) :::

+          translateStatements(mt.body, methodK) :::

+          Exhale(Postconditions(mt.refines.Spec) map {p => (p, ErrorMessage(p.pos, "The postcondition at " + p.pos + " might not hold."))}, "postcondition", methodK, true) :::

           tag(Exhale(

             (postCI map {p => (p, ErrorMessage(mt.pos, "The coupling invariant might not be preserved."))}) :::

-            (Postconditions(mt.spec) map {p => (p, ErrorMessage(p.pos, "The postcondition at " + p.pos + " might not hold."))}), "postcondition", todoiparam, todobparam), keepTag)

+            (Postconditions(mt.spec) map {p => (p, ErrorMessage(p.pos, "The postcondition at " + p.pos + " might not hold."))}), "postcondition", methodK, true), keepTag)

         }

       )

 

@@ -572,7 +580,7 @@ class Translator {
           //update the local, provided a rhs was provided

           case None => Nil

           case Some(rhs) => translateStatement(Assign(new VariableExpr(lv.v), rhs), methodK) }}

-      case s: SpecStmt => translateSpecStmt(s)

+      case s: SpecStmt => translateSpecStmt(s, methodK)

       case c: Call => translateCall(c, methodK)

       case Install(obj, lowerBounds, upperBounds) =>

         Comment("install") ::

@@ -885,7 +893,7 @@ class Translator {
         // decrease credits

         new Boogie.MapUpdate(etran.Credits, TrExpr(ch), new Boogie.MapSelect(etran.Credits, TrExpr(ch)) - 1)

       case r: RefinementBlock =>

-        translateRefinement(r)

+        translateRefinement(r, methodK)

       case _: Signal => throw new NotSupportedException("not implemented")

       case _: Wait => throw new NotSupportedException("not implemented")      

     }

@@ -1009,10 +1017,14 @@ class Translator {
     etran.Heap.store(o, "rdheld", false)

   }

 

-  // TODO: This method has not yet been updated to the new permission model

-  def translateSpecStmt(s: SpecStmt): List[Stmt] = {

+  def translateSpecStmt(s: SpecStmt, methodK: Expr): List[Stmt] = {

     val (preGlobalsV, preGlobals) = etran.FreshGlobals("pre")

 

+    // pick new k for the spec stmt

+    val (specKV, specK) = Boogie.NewBVar("specStmtK", tint, true)

+

+    BLocal(specKV) ::

+    bassume(0 < specK && 1000*specK < percentPermission(1) && 1000*specK < methodK) ::

     // declare new local variables

     s.locals.flatMap(v => translateLocalVarDecl(v, true)) :::

     Comment("spec statement") ::

@@ -1020,11 +1032,11 @@ class Translator {
     // remember values of globals

     copyState(preGlobals, etran) :::

     // exhale preconditions

-    etran.Exhale(List((s.pre, ErrorMessage(s.pos, "The specification statement precondition at " + s.pos + " might not hold."))), "spec stmt precondition", true, todoiparam, todobparam) :::

+    etran.Exhale(List((s.pre, ErrorMessage(s.pos, "The specification statement precondition at " + s.pos + " might not hold."))), "spec stmt precondition", true, specK, false) :::

     // havoc locals

     (s.lhs.map(l => Boogie.Havoc(l))) :::

     // inhale postconditions (using the state before the call as the "old" state)

-    etran.FromPreGlobals(preGlobals).Inhale(List(s.post), "spec stmt postcondition", true, todoiparam)

+    etran.FromPreGlobals(preGlobals).Inhale(List(s.post), "spec stmt postcondition", false, specK)

   }

 

   def translateCall(c: Call, methodK: Expr): List[Stmt] = {

@@ -1147,7 +1159,7 @@ class Translator {
       // check invariant

       Exhale(w.oldInvs map { inv => (inv, ErrorMessage(inv.pos, "The loop invariant at " + inv.pos + " might not be preserved by the loop."))}, "loop invariant, maintained", whileK, true) :::

       tag(Exhale(w.newInvs map { inv => (inv, ErrorMessage(inv.pos, "The loop invariant at " + inv.pos + " might not be preserved by the loop."))}, "loop invariant, maintained", whileK, true), keepTag) :::

-      isLeaking(w.pos, "The loop might leak refereces.") :::

+      isLeaking(w.pos, "The loop might leak references.") :::

       // check lockchange after loop iteration

       Comment("check lockchange after loop iteration") ::

         (bassert(LockFrame(lkch, etran), w.pos, "The loop might lock/unlock more than the lockchange clause allows.")) ::

@@ -1164,20 +1176,19 @@ class Translator {
      bassume(!guard)}))

   }

 

-  // TODO: This method has not yet been updated to the new permission model

-  def translateRefinement(r: RefinementBlock): List[Stmt] = {

+  def translateRefinement(r: RefinementBlock, methodK: Expr): List[Stmt] = {

     // abstract expression translator

     val absTran = etran;

     // concrete expression translate

     val (conGlobalsV, conGlobals) = etran.FreshGlobals("concrete")

     val conTran = new ExpressionTranslator(conGlobals, etran.oldEtran.globals, currentClass); // TODO: what about FoldedPredicateInfo?

-    // 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") ::

@@ -1190,25 +1201,25 @@ class Translator {
     // run concrete C on the fresh heap

     {

       etran = conTran;

-      Comment("run concrete program:") ::

-      tag(translateStatements(r.con, todoiparam), keepTag)

+      Comment("concrete program:") ::

+      tag(translateStatements(r.con, methodK), 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)

         var (sm, sme) = NewBVar("specSecMask", 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) :: BLocal(sm) ::

           (me := absTran.Mask) :: (sme := absTran.SecMask) ::

-          absTran.Exhale(me, sme, List((s.post,ErrorMessage(r.pos, "Refinement may fail to satisfy specification statement post-condition."))), "SpecStmt", false, todoiparam, todobparam) :::

+          absTran.Exhale(s.post, me, absTran.Heap, ErrorMessage(r.pos, "Refinement may fail to satisfy the specification statement post-condition."), false, methodK, false, false) :::

           (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

@@ -1216,13 +1227,13 @@ class Translator {
         (for ((v, w) <- afterV zip before) yield (new VariableExpr(v) := new VariableExpr(w))) :::

         // restore locals before

         (for ((v, w) <- before zip beforeV) yield (new VariableExpr(v) := new VariableExpr(w))) :::

-        translateStatements(r.abs, todoiparam) :::

+        translateStatements(r.abs, methodK) :::

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

     }} :::

     {

@@ -1245,10 +1256,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,

@@ -2656,9 +2667,6 @@ object TranslationHelper {
   }

   

   // prelude definitions

-

-  def todoiparam: Expr = IntLiteral(-1); // This value is used as parameter at places where Chalice has not been updated to the new permission model.

-  def todobparam: Boolean = true; // This value is used as parameter at places where Chalice has not been updated to the new permission model.

   

   def ModuleType = NamedType("ModuleName");

   def ModuleName(cl: Class) = "module#" + cl.module.id;

@@ -2812,11 +2820,6 @@ object TranslationHelper {
     }

     result

   }

-  

-  // TODO: this method is used by the method tranform extension, which has not yet been updated to the new permission model

-  def FractionOf(expr: Expression, fraction: Expression) : Expression = {

-    throw new NotSupportedException("Not supported")

-  }

 

   def TypeInformation(e: Boogie.Expr, cl: Class): Boogie.Expr = {

     if (cl.IsRef) {

diff --git a/Chalice/tests/examples/AVLTree.iterative.chalice b/Chalice/tests/examples/AVLTree.iterative.chalice
new file mode 100644
index 00000000..4156a73f
--- /dev/null
+++ b/Chalice/tests/examples/AVLTree.iterative.chalice
@@ -0,0 +1,227 @@
+class AVLTree{

+	var root : AVLTreeNode;

+

+	predicate valid{

+		   acc(root,100)

+		&& (root!=null ==> root.valid)

+		&& (root!=null ==> acc(root.parent,100))

+		&& (root!=null ==> root.parent==null)

+		&& (root!=null ==> acc(root.root,50))

+		&& (root!=null ==> root.root==root)

+	}

+

+	method init()

+		requires acc(root,100);

+		ensures valid;

+	{

+		root := null;

+		fold valid;

+	}

+

+	method has(k : int) returns (b : bool)

+		requires valid;

+		ensures valid;

+	{

+		unfold valid;

+		if (root==null){

+			b := false;

+			fold valid;

+		}else{

+			var n : AVLTreeNode := root;

+			b := false;

+			var end : bool := false;

+			fold n.udParentValid;

+			while (!end)

+				invariant acc(root,100);

+				invariant root != null && acc(root.parent,50);

+				invariant n!=null;

+				invariant n.valid;

+				invariant acc(n.root,40);

+				invariant n.udParentValid;

+				invariant unfolding n.valid in n.root==root;

+				invariant root!=null;

+			{

+				unfold n.valid;

+				unfold n.validRest;

+				if (n.key==k){

+					b := true;

+					fold n.validRest;

+					fold n.valid;

+					end := true;

+				}else{

+					if (n.key<k){

+						if (n.left==null){

+							end := true;

+							fold n.validRest;

+							fold n.valid;

+						}else{

+							var p : AVLTreeNode := n;

+							unfold p.leftValid;

+							n := p.left;

+							p.leftDown := true;

+							fold p.leftOpen;

+							fold p.udValid;

+							assert p.right!=p.left;

+							assert n.parent.left==n;

+							fold n.udParentValid;

+						}

+					}else{

+						if (n.right==null){

+							end := true;

+							fold n.validRest;

+							fold n.valid;

+						}else{

+							var p : AVLTreeNode := n;

+							unfold p.rightValid;

+							n := p.right;

+							p.leftDown := false;

+							fold p.rightOpen;

+							fold p.udValid;

+							fold n.udParentValid;

+						}

+					}

+				}

+			}

+			

+			end := false;

+			while (!end)

+				invariant acc(root,100);

+				invariant root != null && acc(root.parent,50);

+				invariant n!=null;

+				invariant n.valid;

+				invariant n.udParentValid;

+				invariant acc(n.root,40);

+				invariant unfolding n.valid in n.root==root;

+				invariant root!=null;

+				invariant end==>unfolding n.udParentValid in n.parent==null;

+			{

+				unfold n.udParentValid;

+				var p : AVLTreeNode := n.parent;

+				if (p==null){

+					end := true;

+					fold n.udParentValid;

+				}else{

+					unfold p.udValid;

+					if (p.left==n){

+						unfold p.leftOpen;

+						fold   p.leftValid;

+					}else{

+						unfold p.rightOpen;

+						fold   p.rightValid;

+					}

+					fold p.validRest;

+					fold p.valid;

+					n:=p;

+				}

+			}

+			assert unfolding n.udParentValid in n==root;

+			assert acc(n.root,40);

+			unfold n.udParentValid;

+			assert acc(n.root,50);

+			fold valid;

+		}

+	}

+}

+

+class AVLTreeNode{

+	var key    : int;

+	var left   : AVLTreeNode;

+	var right  : AVLTreeNode;

+	var parent : AVLTreeNode;

+

+	ghost var leftDown : bool;

+	ghost var root : AVLTreeNode;

+	

+	predicate valid{

+		   validRest

+		&& leftValid

+		&& rightValid

+	}

+

+	predicate validRest{

+		   acc(key   ,100)

+		&& acc(root,    30)

+		&& acc(left  ,75)

+		&& acc(right ,75)

+		&& acc(leftDown,100)

+		&& (right!=left || right==null)

+	}

+

+	predicate rightValid{

+		   acc(right ,25)

+		&& acc(root,10)

+		&& (right!=null ==> right.valid)

+		&& (right!=null ==> acc(right.parent,100))

+		&& (right!=null ==> right.parent==this)

+		&& (right!=null ==> acc(right.root,50))

+		&& (right!=null ==> right.root==root)

+	}

+	predicate leftValid{

+		   acc(left  ,25)

+		&& acc(root,10)

+		&& (left!=null ==> left.valid)

+		&& (left!=null ==> acc(left.parent,100))

+		&& (left!=null ==> left.parent == this)

+		&& (left!=null ==> acc(left.root,50))

+		&& (left!=null ==> left.root == root)

+	}

+	

+	predicate leftOpen{

+		   acc(left  ,25)

+		&& acc(root,10)

+		&& (left!=null ==> acc(left.parent,50))

+		&& (left!=null ==> left.parent==this)

+	}

+	

+	predicate rightOpen{

+		   acc(right  ,25)

+		&& acc(root,10)

+		&& (right!=null ==> acc(right.parent,50))

+		&& (right!=null ==> right.parent==this)

+	}

+	

+	predicate udParentValid {

+		   acc(parent,50)

+		&& acc(root,10)

+		&& (parent!=null ==> parent.udValid)

+		&& (parent!=null ==> acc(parent.leftDown,50))

+		&& (parent!=null ==> acc(parent.left,50))

+		&& (parent!=null ==> ( parent.leftDown<==>parent.left==this))

+		&& (parent!=null ==> acc(parent.right,50))

+		&& (parent!=null ==> (!parent.leftDown<==>parent.right==this))

+		&& (parent!=null ==> acc(parent.root,50))

+		&& (parent!=null ==> root==parent.root)

+		&& (parent==null ==> root==this)

+	}

+

+	predicate udValid{

+		   acc(key   ,100)

+		&& acc(leftDown,50)

+		&& acc(left  ,25)

+		&& acc(right ,25)

+		&& acc(root ,20)

+		&& ( leftDown ==> rightValid)

+		&& ( leftDown ==> leftOpen  )

+		&& (!leftDown ==> leftValid )

+		&& (!leftDown ==> rightOpen )

+		&& udParentValid

+	}

+

+	method init(k : int)

+		requires acc(key   ,100);

+		requires acc(left  ,100);

+		requires acc(right ,100);

+		requires acc(leftDown ,100);

+		requires acc(root,     100);

+		ensures valid;

+	{

+		left   := null;

+		right  := null;

+		key    := k;

+

+		fold leftValid;

+		fold rightValid;

+		fold validRest;

+		fold valid;

+	}

+}
\ No newline at end of file
diff --git a/Chalice/tests/examples/AVLTree.iterative.output.txt b/Chalice/tests/examples/AVLTree.iterative.output.txt
new file mode 100644
index 00000000..152260e3
--- /dev/null
+++ b/Chalice/tests/examples/AVLTree.iterative.output.txt
@@ -0,0 +1,4 @@
+Verification of AVLTree.iterative.chalice using parameters="" 

+

+
+Boogie program verifier finished with 0 errors and 0 smoke test warnings.

diff --git a/Chalice/tests/examples/AVLTree.nokeys.chalice b/Chalice/tests/examples/AVLTree.nokeys.chalice
new file mode 100644
index 00000000..721541f2
--- /dev/null
+++ b/Chalice/tests/examples/AVLTree.nokeys.chalice
@@ -0,0 +1,609 @@
+class AVLTree{

+	var root : AVLTreeNode;

+

+	predicate valid{

+		   acc(root,100)

+		&& (root!=null ==> root.valid)

+		&& (root!=null ==> acc(root.height       ,50))

+		&& (root!=null ==> acc(root.balanceFactor,50))

+	}

+

+	method init()

+		requires acc(root,100);

+		ensures valid;

+	{

+		root := null;

+		fold valid;

+	}

+

+	method insert(k : int)

+		requires valid;

+		ensures valid;

+	{

+		unfold valid;

+		if (root==null){

+			var n : AVLTreeNode := new AVLTreeNode;

+			call n.init(k);

+			root := n;

+		}else{

+			call r := root.insert(k);

+			root := r;

+		}

+		fold valid;

+	}

+

+	method remove(k : int)

+		requires valid;

+		ensures valid;

+	{

+		unfold valid;

+		if (root==null){

+		}else{

+			call r := root.remove(k);

+			root := r;

+		}

+		fold valid;

+	}

+

+	method has(k : int) returns (b : bool)

+		requires valid;

+		ensures valid;

+	{

+		unfold valid;

+		if (root==null){

+			b := false;

+		}else{

+			var bb : bool;

+			call bb:= root.has(k);

+			b := bb;

+		}

+		fold valid;

+	}

+}

+

+class AVLTreeNode{

+	var key    : int;

+	var height : int;

+	var left  : AVLTreeNode;

+	var right : AVLTreeNode;

+	ghost var balanceFactor : int;

+

+	predicate valid{

+		   acc(key   ,100)

+		&& acc(height,50)

+		&& acc(left  ,100)

+		&& acc(right ,100)

+		&& acc(balanceFactor,50)

+		&& (left!=null ==> left.valid)

+		&& (left!=null ==> acc(left.height       ,50))

+		&& (left!=null ==> acc(left.balanceFactor,50))

+		&& (left!=null ==> left.height > 0)

+		&& (right!=null ==> right.valid)

+		&& (right!=null ==> acc(right.height       ,50))

+		&& (right!=null ==> acc(right.balanceFactor,50))

+		&& (right!=null ==> right.height > 0)

+		&& height == ( (left==null?0:left.height)>(right==null?0:right.height) ? (left==null?0:left.height)+1 : (right==null?0:right.height)+1 )

+		&& balanceFactor == (left==null?0:left.height) - (right==null?0:right.height)

+		&& balanceFactor<= 1

+		&& balanceFactor>=-1

+		&& height > 0

+	}

+

+	method init(k : int)

+		requires acc(key   ,100);

+		requires acc(height,100);

+		requires acc(left  ,100);

+		requires acc(right ,100);

+		requires acc(balanceFactor,100)

+		ensures valid;

+		ensures acc(height,50);

+		ensures acc(balanceFactor,50);

+		ensures height == 1;

+		ensures balanceFactor == 0;

+	{

+		left   := null;

+		right  := null;

+		key    := k;

+		call close();

+	}

+

+	method insert(k : int) returns ( r : AVLTreeNode )

+		requires valid;

+		requires acc(height,50);

+		requires acc(balanceFactor,50);

+		ensures r != null;

+		ensures r.valid;

+		ensures acc(r.height,50);

+		ensures acc(r.balanceFactor,50);

+		ensures ( r.height == old(height) ) || ( r.height == old(height) + 1 );

+	{

+		unfold valid;

+		if (key==k){

+			r := this;

+			call r.close();

+		}else{ //key!=k

+			if (k<key){ // insert left

+				var nl : AVLTreeNode;

+				if (left==null){

+					nl := new AVLTreeNode;

+					call nl.init(k);

+				}else{

+					call nl := left.insert(k);

+				}

+				left := nl;

+				var bf : int;

+				call bf := getBalanceFactorI();

+

+				if (bf==2){ //rebalance

+					call r:= rebalanceLeft();

+				}else{ //no rebalance

+					r := this;

+					call r.close();

+				}

+			}else{ // k>key -- insert right

+				var nr : AVLTreeNode;

+				if (right==null){

+					nr := new AVLTreeNode;

+					call nr.init(k);

+				}else{

+					call nr := right.insert(k);

+				}

+				right := nr;

+				

+				var bf : int;

+				call bf := getBalanceFactorI();

+				if (bf==-2){ //rebalance

+					call r := rebalanceRight();

+				}else{//no rebalance

+					r := this;

+					call r.close();

+				}

+			}

+		}

+	}

+

+	method remove(k : int) returns ( r : AVLTreeNode )

+		requires valid;

+		requires acc(height,50);

+		requires acc(balanceFactor,50);

+		ensures r != null ==> r.valid;

+		ensures r != null ==> acc(r.height,50);

+		ensures r != null ==> acc(r.balanceFactor,50);

+		ensures old(height)>1 ==> r!=null;

+		ensures r != null ==> r.height==old(height) || r.height+1==old(height);

+	{

+		unfold valid;

+		if (key==k){

+			if (left==null || right==null){

+				if (left==null){ // replace with right

+					r := right;

+				}else{ // right==null

+					r := left;

+				}

+			}else{ // prune max/min of left/right

+				var bf : int;

+				var nl : AVLTreeNode := left;

+				var nr : AVLTreeNode := right;

+				

+				call bf := getBalanceFactorI();

+				if (bf > 0 ){ // left larger - prune leftmax

+					call nl,r := left.pruneMax();

+				}else{ // right larger equal - prune rightmin

+					call nr,r := right.pruneMin();

+				}

+				unfold r.valid;

+				r.left  := nl;

+				r.right := nr;

+				call r.close();

+			}

+		}else{ //key!=k

+			if (k<key){ // remove left

+				if (left!=null){

+					var nl : AVLTreeNode;

+					call nl := left.remove(k);

+					left := nl;

+

+					var bf : int;

+					call bf := getBalanceFactorI();

+

+					if (bf==-2){ // rebalance

+						call r:=rebalanceRight();

+					}else{ // no rebalance

+						call close();

+						r := this;

+					}

+				}else{

+					r := this;

+					call r.close();

+				}

+			}else{ // k>key -- remove right

+				if (right != null){

+					var nr : AVLTreeNode;

+					call nr := right.remove(k);

+					right := nr;

+					

+					var bf : int;

+					call bf := getBalanceFactorI();

+					if (bf==2){ // rebalance

+						call r := rebalanceLeft();

+					}else{ // no rebalance

+						r := this;

+						call r.close();

+					}

+				}else{

+					r := this;

+					call r.close();

+				}

+			}

+		}

+	}

+

+	method pruneMax() returns ( r : AVLTreeNode, m : AVLTreeNode )

+		requires valid;

+		requires acc(height,50);

+		requires acc(balanceFactor,50);

+		ensures r != null ==> r.valid;

+		ensures r != null ==> acc(r.height,50);

+		ensures r != null ==> acc(r.balanceFactor,50);

+		ensures r != null ==> (r.height == old(height) || r.height+1 == old(height));

+		ensures old(height) >1 ==> r != null;

+		ensures old(height)==1 ==> r == null;

+		ensures old(height)==(r==null?0:r.height) || old(height)==(r==null?0:r.height)+1;

+		ensures m != null;

+		ensures	m.valid;

+		ensures acc(m.height,50);

+		ensures acc(m.balanceFactor,50);

+		ensures m.height == 1;

+	{

+		unfold valid;

+		if (right==null){

+			r := left;

+			left := null;

+			call close();

+			m := this;

+		}else{

+			var nr : AVLTreeNode;

+			call nr,m := right.pruneMax();

+			right := nr;

+			var bf : int;

+			call bf := getBalanceFactorI();

+			if (bf == 2){

+				call r:=rebalanceLeft();

+			}else{

+				call close();

+				r := this;

+			}

+		}

+	}

+	

+	method pruneMin() returns ( r : AVLTreeNode, m : AVLTreeNode )

+		requires valid;

+		requires acc(height,50);

+		requires acc(balanceFactor,50);

+		ensures r != null ==> r.valid;

+		ensures r != null ==> acc(r.height,50);

+		ensures r != null ==> acc(r.balanceFactor,50);

+		ensures r != null ==> (r.height == old(height) || r.height == old(height)-1);

+		ensures old(height) >1 ==> r != null;

+		ensures old(height)==1 ==> r == null;

+		ensures old(height)==(r==null?0:r.height) || old(height)==(r==null?0:r.height)+1;

+		ensures m != null;

+		ensures	m.valid;

+		ensures acc(m.height,50);

+		ensures acc(m.balanceFactor,50);

+		ensures m.height == 1;

+	{

+		unfold valid;

+		if (left==null){

+			r := right;

+			right := null;

+			call close();

+			m := this;

+			assert r!=null ==> (r.height == old(height) || r.height == old(height)-1);

+		}else{

+			var nl : AVLTreeNode;

+			call nl,m := left.pruneMin();

+			left := nl;

+			var bf : int;

+			call bf := getBalanceFactorI();

+			if (bf == -2){

+				call r:=rebalanceRight();

+				assert r != null ==> (r.height == old(height) || r.height == old(height)-1);

+			}else{

+				call close();

+				r := this;

+				assert r != null ==> (r.height == old(height) || r.height == old(height)-1);

+			}

+		}

+	}

+

+	method has(k : int) returns (b : bool)

+		requires valid;

+		ensures valid;

+	{

+		unfold valid;

+		if (k==key){

+			b := true;

+		}else{ //k!=key

+			if (k < key){

+				if (left!=null){

+					call b := left.has(k);

+				}else{

+					b := false;

+				}

+			}else{ //k > key;

+				if (right!=null){

+					call b := right.has(k);

+				}else{

+					b := false;

+				}

+			}

+		}

+		fold valid;

+	}

+

+	method getBalanceFactor() returns ( bf : int ) 

+		requires valid;

+		requires rd(balanceFactor);

+

+		ensures valid;

+		ensures rd(balanceFactor);

+		ensures bf == balanceFactor;

+

+		ensures unfolding valid in bf>0 ==> left !=null;

+		ensures unfolding valid in bf<0 ==> right!=null;

+	{

+		unfold valid;

+		var lh : int := (left ==null ? 0 : left .height );

+		var rh : int := (right==null ? 0 : right.height );

+		bf := lh-rh;

+

+		fold valid;

+	}

+

+	//////////////////////////////////////////////////////////

+	method getBalanceFactorI() returns ( bf : int ) 

+		requires rd(left);

+		requires left!=null ==> left.valid;

+		requires left!=null ==> rd(left.height);

+		requires rd(right);

+		requires right!=null ==> right.valid;

+		requires right!=null ==> rd(right.height);

+		ensures rd(left);

+		ensures left!=null ==> left.valid;

+		ensures left!=null ==> rd(left.height);

+		ensures rd(right);

+		ensures right!=null ==> right.valid;

+		ensures right!=null ==> rd(right.height);

+		ensures bf == (left==null?0:left.height)-(right==null?0:right.height);

+		ensures bf>0 ==> left !=null;

+		ensures bf<0 ==> right!=null;

+	{

+		var lh : int := (left ==null ? 0 : left .height );

+		var rh : int := (right==null ? 0 : right.height );

+		bf := lh-rh;

+		assert right!=null ==> unfolding right.valid in right.height>0;

+		assert left !=null ==> unfolding left .valid in left .height>0;

+		assert lh>=0;

+		assert rh>=0;

+	}

+

+	method close()

+		requires acc(key   ,100);

+		requires acc(height,100);

+		requires acc(left  ,100);

+		requires acc(right ,100);

+		requires acc(balanceFactor,100);

+		requires left!=null ==> left.valid;

+		requires left!=null ==> acc(left.height       ,50);

+		requires left!=null ==> acc(left.balanceFactor,50);

+		requires right!=null ==> right.valid;

+		requires right!=null ==> acc(right.height       ,50);

+		requires right!=null ==> acc(right.balanceFactor,50);

+		requires ( left==null ? 0 : left.height )-( right==null ? 0 : right.height ) <= 1;

+		requires ( left==null ? 0 : left.height )-( right==null ? 0 : right.height ) >=-1;

+		ensures valid;

+		ensures acc(height       ,50);

+		ensures acc(balanceFactor,50);

+		ensures height == 

+			( ( old(left)==null ? 0 : old(left.height) )>( old(right)==null ? 0 : old(right.height) ) 

+				? 

+					( old(left)==null ? 0 : old(left.height) )+1 

+				: 

+					( old(right)==null ? 0 : old(right.height))+1

+			);

+		ensures balanceFactor == 

+			( old(left)==null ? 0 : old(left.height) )-( old(right)==null ? 0 : old(right.height) );

+	{

+		var lh : int := (left ==null ? 0 : left .height );

+		var rh : int := (right==null ? 0 : right.height );

+		

+		assert left !=null ==> unfolding left .valid in left .height>0;

+		assert right!=null ==> unfolding right.valid in right.height>0;

+		height := ( (( left==null ? 0 : left.height )>( right==null ? 0 : right.height )) ? ( left==null ? 0 : left.height )+1 : ( right==null ? 0 : right.height )+1);

+		

+		balanceFactor := ( left==null ? 0 : left.height )-( right==null ? 0 : right.height );

+		

+		fold valid;

+	}

+	

+	method rebalanceLeft() returns ( r : AVLTreeNode )

+		requires acc(key   ,100);

+		requires acc(height,100);

+		requires acc(left  ,100);

+		requires acc(right ,100);

+		requires acc(balanceFactor,100);

+		requires left!=null;

+		requires left.valid;

+		requires acc(left.height       ,50);

+		requires acc(left.balanceFactor,50);

+		requires right!=null ==> right.valid;

+		requires right!=null ==> acc(right.height       ,50)

+		requires right!=null ==> acc(right.balanceFactor,50)

+		requires left.height-(right==null?0:right.height)==2;

+		ensures r != null && r.valid;

+		ensures acc(r.height       ,50);

+		ensures acc(r.balanceFactor,50);

+		ensures r.height == old(left.height) || r.height == old(left.height)+1;

+	{

+		var lbf : int;

+		call lbf := left.getBalanceFactor();

+		if (lbf<0){

+			assert unfolding left.valid in lbf==-1;

+			call r := rebalanceRL();

+		}else{//lbf>=0

+			call r := rebalanceRR();

+		}

+	}

+

+	method rebalanceRL() returns ( r : AVLTreeNode )

+		requires acc(key   ,100);

+		requires acc(height,100);

+		requires acc(left  ,100);

+		requires acc(right ,100);

+		requires acc(balanceFactor,100);

+		requires left!=null;

+		requires left.valid;

+		requires acc(left.height       ,50);

+		requires acc(left.balanceFactor,50);

+		requires right!=null ==> right.valid;

+		requires right!=null ==> acc(right.height       ,50)

+		requires right!=null ==> acc(right.balanceFactor,50)

+		requires left.height-(right==null?0:right.height)==2;

+		requires left.balanceFactor==-1;

+		ensures r != null && r.valid;

+		ensures acc(r.height       ,50);

+		ensures acc(r.balanceFactor,50);

+		ensures r.height == old(left.height);

+	{

+		unfold left.valid;

+		r := left.right;

+		unfold r.valid;

+

+		left.right := r.left;

+		call left.close();

+		r.left     := left;

+		left       := r.right;

+		

+		call close(); 

+		r.right    := this;

+		call r.close();

+	}

+

+	method rebalanceRR() returns ( r : AVLTreeNode )

+		requires acc(key   ,100);

+		requires acc(height,100);

+		requires acc(left  ,100);

+		requires acc(right ,100);

+		requires acc(balanceFactor,100);

+		requires left!=null;

+		requires left.valid;

+		requires acc(left.height       ,50);

+		requires acc(left.balanceFactor,50);

+		requires right!=null ==> right.valid;

+		requires right!=null ==> acc(right.height       ,50)

+		requires right!=null ==> acc(right.balanceFactor,50)

+		requires left.height - (right==null?0:right.height)==2;

+		requires left.balanceFactor>=0;

+		ensures r != null && r.valid;

+		ensures acc(r.height       ,50);

+		ensures acc(r.balanceFactor,50);

+		ensures r.height == old(left.height) || r.height == old(left.height)+1;

+	{

+		unfold left.valid;

+		r       := left;

+		left    := r.right;

+		call close();

+		r.right := this;

+		call r.close();

+	}

+

+	method rebalanceRight() returns ( r : AVLTreeNode )

+		requires acc(key   ,100);

+		requires acc(height,100);

+		requires acc(left  ,100);

+		requires acc(right ,100);

+		requires acc(balanceFactor,100);

+		requires left!=null==>left.valid;

+		requires left!=null==>acc(left.height       ,50);

+		requires left!=null==>acc(left.balanceFactor,50);

+		requires right!=null;

+		requires right.valid;

+		requires acc(right.height       ,50)

+		requires acc(right.balanceFactor,50)

+		requires (left==null?0:left.height)-right.height==-2;

+		ensures r != null && r.valid;

+		ensures acc(r.height       ,50);

+		ensures acc(r.balanceFactor,50);

+		ensures r.height == old(right.height) || r.height == old(right.height)+1;

+	{

+		var rbf : int;

+		call rbf := right.getBalanceFactor();

+		if (rbf>0){

+			assert unfolding right.valid in rbf==1;

+			call r := rebalanceLR();

+		}else{//rbf<=0

+			call r := rebalanceLL();

+		}

+	}

+

+	method rebalanceLR() returns ( r : AVLTreeNode )

+		requires acc(key   ,100);

+		requires acc(height,100);

+		requires acc(left  ,100);

+		requires acc(right ,100);

+		requires acc(balanceFactor,100);

+		requires left!=null==>left.valid;

+		requires left!=null==>acc(left.height       ,50);

+		requires left!=null==>acc(left.balanceFactor,50);

+		requires right!=null;

+		requires right.valid;

+		requires acc(right.height       ,50);

+		requires acc(right.balanceFactor,50);

+		requires (left==null?0:left.height)-right.height==-2;

+		requires right.balanceFactor==1;

+		ensures r != null && r.valid;

+		ensures acc(r.height       ,50);

+		ensures acc(r.balanceFactor,50);

+		ensures r.height == old(right.height);

+	{

+		unfold right.valid;

+		r := right.left;

+		unfold r.valid;

+		right.left := r.right;

+		call right.close();

+		r.right    := right;

+		right      := r.left;

+		call close();

+		r.left     := this;

+		call r.close();

+	}

+

+	method rebalanceLL() returns ( r : AVLTreeNode )

+		requires acc(key   ,100);

+		requires acc(height,100);

+		requires acc(left  ,100);

+		requires acc(right ,100);

+		requires acc(balanceFactor,100);

+		requires left!=null==>left.valid;

+		requires left!=null==>acc(left.height       ,50);

+		requires left!=null==>acc(left.balanceFactor,50);

+		requires right!=null;

+		requires right.valid;

+		requires acc(right.height       ,50);

+		requires acc(right.balanceFactor,50);

+		requires (left==null?0:left.height)-right.height==-2;

+		requires right.balanceFactor<=0;

+		ensures r != null && r.valid;

+		ensures acc(r.height       ,50);

+		ensures acc(r.balanceFactor,50);

+		ensures r.height == old(right.height) || r.height == old(right.height)+1;

+	{

+		unfold right.valid;

+		r       := right;

+		right    := r.left;

+		call close();

+		r.left := this;

+		call r.close();

+	}

+}
\ No newline at end of file
diff --git a/Chalice/tests/examples/AVLTree.nokeys.output.txt b/Chalice/tests/examples/AVLTree.nokeys.output.txt
new file mode 100644
index 00000000..c9dc557a
--- /dev/null
+++ b/Chalice/tests/examples/AVLTree.nokeys.output.txt
@@ -0,0 +1,4 @@
+Verification of AVLTree.nokeys.chalice using parameters="" 

+

+
+Boogie program verifier finished with 0 errors and 0 smoke test warnings.

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}
diff --git a/Chalice/tests/runalltests.bat b/Chalice/tests/runalltests.bat
index ced36a8e..ab878804 100644
--- a/Chalice/tests/runalltests.bat
+++ b/Chalice/tests/runalltests.bat
@@ -17,13 +17,18 @@ for %%f in (examples permission-model general-tests regressions predicates) do (
   cd %%f

   set tt=0

   for %%f in (*.chalice) do set /A tt+=1

-  call reg_test_all.bat -no-summary

+  call reg_test_all.bat -no-summary %1 %2 %3 %4 %5

   set /A c=!c!+!errorlevel!

   set /A t=!t!+!tt!

   cd ..

   echo ------------------------------------------------------

 )

 

+REM Run refinement regression tests

+cd refinements

+call test.bat

+cd ..

+

 if !nosummary!==0 (

     echo.

     if !c!==0 (echo SUMMARY: completed !t! tests successfully.) else (echo SUMMARY: !c! of !t! tests failed.)