Chalice:

* added loop transform pattern
* implemented translation of refined loops to Boogie (only assert new loop invariants)
* refactored loop target computation code (async call was not handled as maybe some other statement)

14 files changed, 291 insertions, 168 deletions

diff --git a/Chalice/examples/refinement/sqroot.chalice b/Chalice/examples/refinement/sqroot.chalice
deleted file mode 100644
index f640eeec..00000000
--- a/Chalice/examples/refinement/sqroot.chalice
+++ /dev/null
@@ -1,62 +0,0 @@
-// Based on Back & Wright p.342
-// Algorithmic refinement with a recursion introduction
-
-// how Chalice proves termination?
-// interesting that if I leave out l >= 0 and r >= 0 (as I did initially) then Chalice correctly cannot prove refinement of sqrt1
-
-class Cell {
-  var x: int;
-
-  method compute0(e: int)
-    requires e >= 0 && acc(x);
-    ensures acc(x) && x*x <= e && e < (x+1)*(x+1);
-  {
-    assume false;
-  }
-
-  method compute1(e: int)
-    requires e >= 0 && acc(x);
-    ensures acc(x) && x*x <= e && e < (x+1)*(x+1);
-  {
-    call sqrt0(e, 0, e+1);
-  }
-
-  method sqrt0(n, l, r)
-    requires acc(x) && l*l <= n && n < r*r && l >= 0 && r >= 0;
-    ensures acc(x) && x*x <= n && n < (x+1)*(x+1);
-  {
-    if (l + 1 == r) {
-      x := l;
-    } else {
-      var k: int;
-      assume k > l;
-      assume k < r;
-      if (n < k*k) {
-        call sqrt0(n, l, k);
-      } else {
-        call sqrt0(n, k, r);
-      }
-    }
-  }
-
- method sqrt1(n, l, r)
-    requires acc(x) && l*l <= n && n < r*r && l >= 0 && r >= 0;
-    ensures acc(x) && x*x <= n && n < (x+1)*(x+1);
-  {
-    assert l < r;
-    if (l + 1 == r) {
-      x := l;
-    } else {      
-      var k := l + 1; // no division in chalice
-      assert k > l;
-      assert k < r;
-      if (n < k*k) {
-        call sqrt1(n, l, k);
-      } else {
-        call sqrt1(n, k, r);
-      }
-    }
-  }
-
- 
-}
diff --git a/Chalice/refinements/LoopSqRoot.chalice b/Chalice/refinements/LoopSqRoot.chalice
new file mode 100644
index 00000000..e14fe4d6
--- /dev/null
+++ b/Chalice/refinements/LoopSqRoot.chalice
@@ -0,0 +1,51 @@
+class A0 {
+  method sqroot(n) returns (x)
+    requires n >= 0;
+  { 
+    var x [x*x <= n && n < (x+1)*(x+1) && x >=0];    
+  }
+}
+
+class A1 refines A0 {
+  transforms sqroot(n) returns (x)
+  {
+    replaces x by {
+      var l := 0;
+      var r := n + 1;
+      while (l + 1 != r) 
+        invariant l >= 0 && r > l;
+        invariant l*l <= n && n < r*r;
+      {
+        var k [l < k && k < r];
+        if (k*k <= n) {
+          l := k;
+        } else {
+          r := k;
+        }
+      }
+      x := l;      
+    }
+  }
+}
+/*
+  method compute2(n: int) returns (x: int)
+    requires n >= 0;
+  { 
+    var l := 0;
+    var r := n + 1;
+    while (l + 1 != r)
+      invariant l >= 0 && r > l;
+      invariant l*l <= n && n < r*r;
+    {
+      var p [2*p <= l+r && l+r < 2*(p+1)];
+      assert l < p && p < r;
+      if (p*p <= n) {
+        l := p;
+      } else {
+        r := p;
+      }
+    }
+    // no need to reverify
+  }
+}
+*/
diff --git a/Chalice/refinements/RecSqRoot.chalice b/Chalice/refinements/RecSqRoot.chalice
new file mode 100644
index 00000000..a10c1b55
--- /dev/null
+++ b/Chalice/refinements/RecSqRoot.chalice
@@ -0,0 +1,46 @@
+class A0 {
+  method sqroot(n) returns (x)
+    requires n >= 0;
+  {
+    var x [x*x <= n && n < (x+1)*(x+1)];      
+  }  
+}
+
+class A1 refines A0 {
+  transforms sqroot(n) returns (x)
+  {        
+    replaces x by {call x := rec(n,0,n+1)}    
+  }
+  
+  method rec(n, l, r) returns (x)
+    requires l*l <= n && n < r*r;
+    requires l >= 0 && r >= 0;
+    ensures x*x <= n && n < (x+1)*(x+1);
+  {
+    if (l+1 == r) {
+      x := l;
+    } else {
+      var k [l < k && k < r];
+      if (n < k*k) {
+        call x := rec(n,l,k);
+      } else {
+        call x := rec(n,k,r);
+      }
+    }
+  }
+}
+
+class A2 refines A1 {
+  transforms rec(n, l, r) returns (x)
+  {    
+    if {
+      *
+    } else {
+      replaces k by {
+        assert l < r;
+        var k := l+1;
+      }
+      *
+    }    
+  }
+}
diff --git a/Chalice/refinements/SpecStmt.chalice b/Chalice/refinements/SpecStmt.chalice
new file mode 100644
index 00000000..15072d41
--- /dev/null
+++ b/Chalice/refinements/SpecStmt.chalice
@@ -0,0 +1,35 @@
+class Test {
+  var x: int;
+  method m(a:int) returns (b:int) 
+  {
+    var c := 0;
+    ghost const d,c [d == c];
+    var b [b == 0];  
+    var e [e == a];   
+    assert d == c;
+    assert e == a;
+    assert b == 0;
+    assert c == 0; // error 
+  }
+
+  method n() 
+    requires acc(x);
+  {
+    x := 0;
+    const y [acc(x), rd(x) && x == old(x) + 1 && y == x];
+    assert y == 1;
+    const v [rd(x), rd(x) && v == old(x) + 1];
+    assert v == 2;
+    const z [z == 1];
+    ghost var t [z == 1, true];     
+    assert false; // reachable 
+  }
+
+  method o()  
+  {
+    var z [acc(x) && z == 0]; // unimplementable
+    x := z;
+    assert x == 0;
+    assert false; // reachable
+  }
+}
diff --git a/Chalice/examples/refinement/SumCubes.chalice b/Chalice/refinements/SumCubes.chalice
index 5ebf78cd..02d66031 100644
--- a/Chalice/examples/refinement/SumCubes.chalice
+++ b/Chalice/refinements/SumCubes.chalice
@@ -1,6 +1,6 @@
 // Prove \sum i*i*i == (\sum i)(\sum i)
-class SumCubes {
-  method compute0(n: int)
+class SumCubes0 {
+  method compute(n)
     requires n >= 0;
   {
     var i := 0;
@@ -12,19 +12,18 @@ class SumCubes {
       s := s + i*i*i;
     }
   }
-  method compute1(n: int)
-    requires n >= 0; 
-  {
-    var i := 0;
-    var s := 0;
-    var t := 0;
-    while (i < n)
-      invariant i <= n;
+}
+
+class SumCubes1 refines SumCubes0 {
+  transforms compute(n)  
+  {    
+    _
+    var t := 0;    
+    while    
       invariant s == t*t;
       invariant 2*t == i*(i+1);
     {    
-      i := i + 1;      
-      s := s + i*i*i;          
+      _         
       t := t + i;
     }
   }
diff --git a/Chalice/refinements/TestRefines.chalice b/Chalice/refinements/TestRefines.chalice
new file mode 100644
index 00000000..2cfc19b2
--- /dev/null
+++ b/Chalice/refinements/TestRefines.chalice
@@ -0,0 +1,13 @@
+class A {
+  var x:int;
+  function f():int {1}
+  method m(i:int) returns (j:int) {
+    var j [j > 0];    
+  }
+}
+
+class B refines C {}
+class C refines D {}
+class D refines A {
+  transforms m(i:int) returns (j:int, k:int) {*} 
+}
diff --git a/Chalice/refinements/TestTransform.chalice b/Chalice/refinements/TestTransform.chalice
new file mode 100644
index 00000000..2c18907f
--- /dev/null
+++ b/Chalice/refinements/TestTransform.chalice
@@ -0,0 +1,38 @@
+class A {
+  method m(i: int) returns (x: int) 
+    ensures x == i;
+  {
+    var j := 0;
+    var v [v == i + j];
+    x := v;
+  }
+
+  method n() {
+    var x := 0;
+    var y := 1;
+    var z := 2;  
+  }
+}
+
+class B refines A {
+  transforms m(i: int) returns (x: int, y: int)  
+    ensures y == 0;
+  {
+    var t := 0;
+    _
+    replaces v by {
+      var v := i + j; 
+      call t, j := m(0);
+      y := j;
+    }
+    _
+  }
+
+  transforms n() {
+    replaces * by {
+      var x := 0;
+      var y := x + 1;
+      var z := 2*y;
+    }
+  }
+}
diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala
index 23d6356d..8059284c 100644
--- a/Chalice/src/Ast.scala
+++ b/Chalice/src/Ast.scala
@@ -190,7 +190,7 @@ sealed abstract class Refinement(id: String) extends Callable(id) {
 case class MethodTransform(id: String, ins: List[Variable], outs: List[Variable], spec: List[Specification], trans: Transform) extends Refinement(id) {

   var body = null:List[Statement];

   def Spec = {assert(refines != null); refines.Spec ++ spec}

-  def Body = {assert(body != null); body}

+  def Body = {assert(body != null); body}   // TODO: get rid of refinement blocks (that is make sure variables match)

   def Ins = {assert(refines != null); refines.Ins}

   def Outs = {assert(refines != null); refines.Outs ++ outs.drop(refines.Outs.size)}

 }

@@ -211,6 +211,7 @@ case class SkipPat() extends Transform
 /** Replacement pattern for arbitrary block */

 case class ProgramPat(code: List[Statement]) extends Transform

 case class IfPat(thn: Transform, els: Option[Transform]) extends Transform

+case class WhilePat(invs: List[Expression], body: Transform) extends Transform

 case class NonDetPat(is: List[String], code: List[Statement]) extends Transform {

   def matches(s: Statement) = s match {

     case _:Call => true

@@ -221,11 +222,12 @@ case class NonDetPat(is: List[String], code: List[Statement]) extends Transform
 case class InsertPat(code: List[Statement]) extends Transform

 case class SeqPat(pats: List[Transform]) extends Transform {

   assert(pats.size > 0)

+  pos = pats.first.pos;

 }

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

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

   var locals: List[Variable] = null;

-  override def Declares = BlockStmt(con).Declares

+  override def Declares = con flatMap {_.Declares}

 }

 

 /**

@@ -233,37 +235,42 @@ case class RefinementBlock(con: List[Statement], abs: List[Statement]) extends S
  */

 

 sealed abstract class Statement extends ASTNode {

-  // requires resolved statements

-  def Declares: List[Variable] = Nil

+  def Declares: List[Variable] = Nil // call after resolution

+  def Targets: Set[Variable] = Set() // assigned local variables

 }

 case class Assert(e: Expression) extends Statement

 case class Assume(e: Expression) extends Statement

 case class BlockStmt(ss: List[Statement]) extends Statement {

-  override def Declares = ss flatMap {s => s.Declares}

+  override def Targets = (ss :\ Set[Variable]()) { (s, vars) => vars ++ s.Targets}

+}

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

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

 }

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

 case class WhileStmt(guard: Expression,

-                     invs: List[Expression], lkch: List[Expression],

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

                      body: BlockStmt) extends Statement {

-  var LoopTargets: Set[Variable] = null

-  lazy val LoopTargetsList = {

-    assert (LoopTargets != null)

-    LoopTargets.toList

-  }

+  val Invs = oldInvs ++ newInvs;

+  var LoopTargets: List[Variable] = Nil;

+  override def Targets = body.Targets;

+}

+case class Assign(lhs: VariableExpr, rhs: RValue) extends Statement {

+  override def Targets = if (lhs.v != null) Set(lhs.v) else Set()

 }

-case class Assign(lhs: VariableExpr, rhs: RValue) extends Statement

 case class FieldUpdate(lhs: MemberAccess, rhs: RValue) extends Statement

 case class LocalVar(id: String, t: Type, const: Boolean, ghost: Boolean, rhs: Option[RValue]) extends Statement {

   val v = new Variable(id, t, ghost, const);

   override def Declares = List(v)

+  override def Targets = rhs match {case None => Set(); case Some(_) => Set(v)}

 }

 case class Call(declaresLocal: List[Boolean], lhs: List[VariableExpr], obj: Expression, id: String, args: List[Expression]) extends Statement {

   var locals = List[Variable]()

   var m: Callable = null

   override def Declares = locals

+  override def Targets = (lhs :\ Set[Variable]()) { (ve, vars) => if (ve.v != null) vars + ve.v else vars }

 }

 case class SpecStmt(lhs: List[VariableExpr], locals:List[Variable], pre: Expression, post: Expression) extends Statement {

   override def Declares = locals;

+  override def Targets = (lhs :\ Set[Variable]()) { (ve, vars) => if (ve.v != null) vars + ve.v else vars }

 }

 case class Install(obj: Expression, lowerBounds: List[Expression], upperBounds: List[Expression]) extends Statement

 case class Share(obj: Expression, lowerBounds: List[Expression], upperBounds: List[Expression]) extends Statement

@@ -279,6 +286,7 @@ case class CallAsync(declaresLocal: Boolean, lhs: VariableExpr, obj: Expression,
   var local: Variable = null

   var m: Method = null

   override def Declares = if (local != null) List(local) else Nil

+  override def Targets = if (lhs.v != null) Set(lhs.v) else Set()

 }

 case class JoinAsync(lhs: List[VariableExpr], token: Expression) extends Statement {

   var m: Method = null

@@ -539,12 +547,17 @@ object AST {
 

   /**

    * Matches a proper block to a transform.

-   * Requires: a sequence pattern should not contain a sequence pattern

+   * Effects: some statements might be replaced by refinements blocks; Loops might have new invariants.

+   * Requires: in transform, a sequence pattern should not contain a sequence pattern.

    */

   def refine:(List[Statement], Transform) => TransformMatch = {

     // order is important!

+    // reduction of base cases

+    case (l, SeqPat(List(t))) => refine(l, t)

+    case (List(BlockStmt(ss)), t) => refine(ss, t)

     // whole program 

     case (l, ProgramPat(code)) => new Matched(RefinementBlock(code, l))

+    case (l, SkipPat()) => Matched(l)    

     // if pattern

     case (List(IfStmt(guard, thn, None)), t @ IfPat(thnT, None)) =>

       refine(thn.ss, thnT) match {

@@ -556,24 +569,26 @@ object AST {
         case (Matched(thn0), Matched(els0)) => new Matched(IfStmt(guard, BlockStmt(thn0), Some(BlockStmt(els0))))

         case _ => Unmatched(t)

       }

+    // while pattern

+    case (List(WhileStmt(guard, oi, Nil, lks, body)), wp @ WhilePat(l, t)) =>

+      refine(body.ss, t) match {

+        case Matched(body0) => new Matched(WhileStmt(guard, oi, l, lks, BlockStmt(body0)))

+        case _ => Unmatched(wp)

+      }

     // non det pat

     case (l @ List(_: Call), NonDetPat(_, code)) => new Matched(RefinementBlock(code, l))

     case (l @ List(_: SpecStmt), NonDetPat(_, code)) => new Matched(RefinementBlock(code, l))

     // insert pat

     case (Nil, InsertPat(code)) => new Matched(RefinementBlock(code, Nil))

-    // reduction of base cases

-    case (l, SeqPat(List(t))) => refine(l, t)

-    case (List(BlockStmt(ss)), t) => refine(ss, t)        

     // block pattern (greedy matching)

     case (l, bp @ BlockPat()) if (l forall {s => bp matches s}) => Matched(l)

-    case (s :: ss, SeqPat((bp @ BlockPat()) :: ts)) if (bp matches s) =>

-      refine(ss, SeqPat(ts)) match {

+    case (s :: ss, t @ SeqPat((bp @ BlockPat()) :: _)) if (bp matches s) =>

+      refine(ss, t) match {

         case Matched(l) => Matched(s :: l)

         case x => x

       }

     case (l, SeqPat((bp @ BlockPat()) :: ts)) if (l.size == 0 || !(bp matches l.head)) =>

       refine(l, SeqPat(ts))

-    case (l, SkipPat()) => Matched(l)

     // sequence pattern

     case (s :: ss, SeqPat((np: NonDetPat) :: ts)) =>

       (refine(List(s), np), refine(ss, SeqPat(ts))) match {

@@ -590,6 +605,11 @@ object AST {
         case Matched(a) => Matched(RefinementBlock(code, Nil) :: a)

         case x => x

       }

+    case (s :: ss, SeqPat((wp: WhilePat) :: ts)) =>

+      (refine(List(s), wp), refine(ss, SeqPat(ts))) match {

+        case (Matched(a), Matched(b)) => Matched(a ::: b)

+        case _ => Unmatched(wp)

+      }

     case (_, t) => Unmatched(t)

   }

 

diff --git a/Chalice/src/ChaliceToCSharp.scala b/Chalice/src/ChaliceToCSharp.scala
index 67f6585b..98258e97 100644
--- a/Chalice/src/ChaliceToCSharp.scala
+++ b/Chalice/src/ChaliceToCSharp.scala
@@ -114,7 +114,7 @@ class ChaliceToCSharp {
         indent + convertExpression(target) + "." + f + " = " + convertExpression(rhs) + ";" + nl

       case Assign(VariableExpr(x), rhs) =>

         indent + x + " = " + convertExpression(rhs) + ";" + nl

-      case WhileStmt(guard, _, _, body) =>

+      case WhileStmt(guard, _, _, _, body) =>

         indent + "while (" + convertExpression(guard) + ")" + nl + convertStatement(body) + nl

       case c@Call(_, lhs, target, id, args) =>

         declareLocals(c.locals) +

diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala
index cf673280..bffcfb00 100644
--- a/Chalice/src/Parser.scala
+++ b/Chalice/src/Parser.scala
@@ -157,7 +157,7 @@ class Parser extends StandardTokenParsers {
     | "if" ~> ifStmtThen

     | "while" ~> "(" ~> expression ~ ")" ~ loopSpec ~ blockStatement ^^ {

         case guard ~ _ ~ lSpec ~ body =>

-          lSpec match { case (invs,lkch) => WhileStmt(guard, invs, lkch, BlockStmt(body)) }}

+          lSpec match { case (invs,lkch) => WhileStmt(guard, invs, Nil, lkch, BlockStmt(body)) }}

     | "reorder" ~> expression ~ (installBounds ?) <~ Semi ^^ {

         case obj ~ None => Install(obj, List(), List())

         case obj ~ Some(bounds) => Install(obj, bounds._1, bounds._2) }

@@ -558,13 +558,12 @@ class Parser extends StandardTokenParsers {
    * Transforms

    */

 

-  def transform: Parser[Transform] = positioned(

-      "if" ~> ifTransform

-    | transformAtom ~ rep(transform) ^^ {case atom ~ t => SeqPat(atom :: t)}

-    )

+  def transform: Parser[Transform] = rep1(transformAtom) ^^ SeqPat

   def transformAtom: Parser[Transform] = positioned(

       "_" ~ Semi ^^^ BlockPat()

     | "*" ~ Semi ^^^ SkipPat()

+    | "if" ~> ifTransform

+    | "while" ~> rep("invariant" ~> expression <~ Semi) ~ ("{" ~> transform <~ "}") ^^ {case ee ~ body => WhilePat(ee, body)}

     | "replaces" ~> "*" ~> "by" ~> blockStatement ^^ ProgramPat              

     | "replaces" ~> rep1sep(Ident,",") ~ ("by" ~> blockStatement) ^^ {

         case ids ~ code => NonDetPat(ids map {x => x.v}, code)

diff --git a/Chalice/src/PrettyPrinter.scala b/Chalice/src/PrettyPrinter.scala
index 2802e7b8..6a408b45 100644
--- a/Chalice/src/PrettyPrinter.scala
+++ b/Chalice/src/PrettyPrinter.scala
@@ -76,7 +76,7 @@ object PrintProgram {
       PrintBlockStmt(ss, indent); println

     case RefinementBlock(ss, old) =>

       println("/* begin of refinement block")

-      for (s <- old) {Spaces(indent); Stmt(s, indent)}

+      for (s <- old) {Spaces(indent + 2); Stmt(s, indent + 2)}

       Spaces(indent); println("end of abstract code */")

       for (s <- ss) {Spaces(indent); Stmt(s, indent)}

       Spaces(indent); println("// end of refinement block")

@@ -87,9 +87,9 @@ object PrintProgram {
         case None => println

         case Some(s) => print(" else "); Stmt(s, indent)

       }

-    case WhileStmt(guard, invs, lkch, body) =>

+    case w @ WhileStmt(guard, _, _, lkch, body) =>

       print("while ("); Expr(guard); println(")")

-      for (inv <- invs) {

+      for (inv <- w.Invs) {

         Spaces(indent+2)

         print("invariant "); Expr(inv); println(Semi)

       }

diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala
index 603cba69..e50cc7ab 100644
--- a/Chalice/src/Resolver.scala
+++ b/Chalice/src/Resolver.scala
@@ -287,8 +287,7 @@ object Resolver {
    case Assume(e) =>

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

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

-   case RefinementBlock(ss, _) =>

-     ResolveStmt(BlockStmt(ss), context)  // TODO is this correct for multi-step refinement?

+   case RefinementBlock(ss, _) => throw new Exception("unexpected statement")

    case BlockStmt(ss) =>

      var ctx = context

      for (s <- ss) s match {

@@ -333,7 +332,8 @@ object Resolver {
      CheckNoGhost(guard, context)

      ResolveStmt(thn, context)

      els match { case None => case Some(s) => ResolveStmt(s, context) }

-   case w@ WhileStmt(guard, invs, lkch, body) =>

+   case w@ WhileStmt(guard, invs, ref, lkch, body) =>

+     if (ref.size > 0) throw new Exception("unexpected statement")

      ResolveExpr(guard, context, false, false)(false)

      if (!guard.typ.IsBool) context.Error(guard.pos, "while statement requires a boolean guard (found " + guard.typ.FullName + ")")

      CheckNoGhost(guard, context)

@@ -346,7 +346,7 @@ object Resolver {
        if (!l.typ.IsRef) context.Error(l.pos, "lockchange expression must be reference (found " + l.typ.FullName + ")")

      }

      ResolveStmt(body, context)

-     w.LoopTargets = ComputeLoopTargets(body) filter context.IsVariablePresent

+     w.LoopTargets = body.Targets.filter(context.IsVariablePresent).toList

    case Assign(lhs, rhs) =>

      ResolveExpr(lhs, context, false, false)(false)

      ResolveAssign(lhs, rhs, context)

@@ -614,26 +614,6 @@ object Resolver {
        context.Error(b.pos, descript + " bound must be of a reference type or Mu type (found " + b.typ.FullName + ")")

    }

 

- def ComputeLoopTargets(s: Statement): Set[Variable] = s match {  // local variables

-   case BlockStmt(ss) =>

-     (ss :\ Set[Variable]()) { (s,vars) => vars ++ ComputeLoopTargets(s) }

-   case IfStmt(guard, thn, els) =>

-     val vars = ComputeLoopTargets(thn)

-     els match { case None => vars; case Some(els) => vars ++ ComputeLoopTargets(els) }

-   case w: WhileStmt =>

-     // assume w.LoopTargets is non-null and that it was computed with a larger context

-     w.LoopTargets

-   case Assign(lhs, rhs) =>

-     if (lhs.v != null) Set(lhs.v) else Set()  // don't assume resolution was successful

-   case s: SpecStmt =>

-     (s.lhs :\ Set[Variable]()) { (ve,vars) => if (ve.v != null) vars + ve.v else vars }

-   case lv: LocalVar =>

-     lv.rhs match { case None => Set() case Some(_) => Set(lv.v) }

-   case Call(_, lhs, obj, id, args) =>

-     (lhs :\ Set[Variable]()) { (ve,vars) => if (ve.v != null) vars + ve.v else vars }

-   case _ => Set()

- }

-

  def ResolveAssign(lhs: VariableExpr, rhs: RValue, context: ProgramContext) = {

    rhs match {

      case ExplicitSeq(Nil) => rhs.typ = lhs.typ; // if [] appears on the rhs of an assignment, we "infer" its type by looking at the type of the lhs

@@ -1096,7 +1076,8 @@ object Resolver {
 

  def ResolveTransform(mt: MethodTransform, context: ProgramContext) {

    mt.spec foreach {

-     case Precondition(e) => throw new Exception("not implemented")

+     case Precondition(e) =>

+       context.Error(e.pos, "Method refinement cannot have a pre-condition")

      case Postcondition(e) =>

        ResolveExpr(e, context.SetClass(mt.Parent).SetMember(mt), true, true)(false)

      case _ : LockChange => throw new Exception("not implemented")

@@ -1106,25 +1087,27 @@ object Resolver {
 

    mt.body = AST.refine(mt.refines.Body, mt.trans) match {

      case AST.Matched(ss) => ss

-     case AST.Unmatched(t) => context.Error(mt.pos, "Cannot match transform around " + t); Nil

+     case AST.Unmatched(t) => context.Error(mt.pos, "Cannot match transform around " + t.pos); Nil

    }

                                 

-   // resolution must check for:

-   // * resolve statements in refinement blocks

-   // * loops might have more loop targets

-   // * compute abstract local variables for every refinement block

    def resolveBody(ss: List[Statement], con: ProgramContext, abs: List[Variable]) {

      var ctx = con;

      var locals = abs;

      for (s <- ss) {

        s match {

-         case r @ RefinementBlock(l, original) =>

+         case r @ RefinementBlock(c, a) =>

+           // abstract globals available at this point in the program

            r.locals = locals

-           ResolveStmt(BlockStmt(l), ctx)

-           val vs = BlockStmt(l).Declares;

-           for (v <- BlockStmt(original).Declares)

-             if (! vs.contains(v))

-               ctx.Error(s.pos, "Refinement block must declare a local variable from abstract program: " + v.id)

+           ResolveStmt(BlockStmt(c), ctx)

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

+         case w @ WhileStmt(guard, oi, ni, lks, body) =>

+           for (inv <- ni) {

+             ResolveExpr(inv, ctx, true, true)(false)

+             if (!inv.typ.IsBool) ctx.Error(inv.pos, "loop invariant must be boolean (found " + inv.typ.FullName + ")")

+           }

+           resolveBody(body.ss, ctx, locals)

          case IfStmt(_, thn, None) =>

            resolveBody(thn.ss, ctx, locals)

          case IfStmt(_, thn, Some(els)) =>

@@ -1137,7 +1120,7 @@ object Resolver {
        // declare concrete and abstract locals

        for (v <- s.Declares) ctx = ctx.AddVariable(v);

        s match {

-         case RefinementBlock(_, abs) => locals = locals ++ BlockStmt(abs).Declares

+         case RefinementBlock(_, a) => locals = locals ++ (a flatMap {s => s.Declares})

          case _ => locals = locals ++ s.Declares 

        }

      }

diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index e6c3db7b..f4fd1108 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -113,7 +113,6 @@ class Translator {
   def translateField(f: Field): List[Decl] = {

     Const(f.FullName, true, FieldType(f.typ.typ)) ::

     Axiom(NonPredicateField(f.FullName))

-    // TODO: add typeinformation as an axiom

   }

 

   def translateFunction(f: Function): List[Decl] = {

@@ -773,6 +772,8 @@ class Translator {
         new Boogie.MapUpdate(etran.Credits, TrExpr(ch), new Boogie.MapSelect(etran.Credits, TrExpr(ch)) - 1)

       case r: RefinementBlock =>

         translateRefinement(r)

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

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

     }

   }

 

@@ -949,19 +950,18 @@ class Translator {
 

   def translateWhile(w: WhileStmt): List[Stmt] = {

     val guard = w.guard;

-    val invs = w.invs;

-    val lkch = w. lkch;

+    val lkch = w.lkch;

     val body = w.body;

 

     val preLoopGlobals = etran.FreshGlobals("while")

     val loopEtran = etran.FromPreGlobals(preLoopGlobals)

     val iterStartGlobals = etran.FreshGlobals("iterStart")

     val iterStartEtran = etran.FromPreGlobals(iterStartGlobals)

-    val saveLocalsV = for (v <- w.LoopTargetsList) yield new Variable(v.id, v.t)

-    val iterStartLocalsV = for (v <- w.LoopTargetsList) yield new Variable(v.id, v.t)

-    val lkchOld = lkch map (e => SubstVars(e, w.LoopTargetsList,

+    val saveLocalsV = for (v <- w.LoopTargets) yield new Variable(v.id, v.t)

+    val iterStartLocalsV = for (v <- w.LoopTargets) yield new Variable(v.id, v.t)

+    val lkchOld = lkch map (e => SubstVars(e, w.LoopTargets,

                                              for (v <- saveLocalsV) yield new VariableExpr(v)))

-    val lkchIterStart = lkch map (e => SubstVars(e, w.LoopTargetsList,

+    val lkchIterStart = lkch map (e => SubstVars(e, w.LoopTargets,

                                                    for (v <- iterStartLocalsV) yield new VariableExpr(v)))

     val oldLocks = lkchOld map (e => loopEtran.oldEtran.Tr(e))

     val iterStartLocks = lkchIterStart map (e => iterStartEtran.oldEtran.Tr(e))

@@ -973,15 +973,15 @@ class Translator {
     (loopEtran.oldEtran.Mask := loopEtran.Mask) ::  // oldMask is not actually used below

     (loopEtran.oldEtran.Credits := loopEtran.Credits) ::  // is oldCredits?

     // check invariant on entry to the loop

-    Exhale(invs map { inv => (inv, ErrorMessage(inv.pos, "The loop invariant might not hold on entry to the loop."))}, "loop invariant, initially") :::

-     List(bassert(DebtCheck, w.pos, "Loop invariant must consume all debt on entry to the loop.")) :::

+    Exhale(w.oldInvs map { inv => (inv, ErrorMessage(inv.pos, "The loop invariant might not hold on entry to the loop."))}, "loop invariant, initially") :::

+    tag(Exhale(w.newInvs map { inv => (inv, ErrorMessage(inv.pos, "The loop invariant might not hold on entry to the loop."))}, "loop invariant, initially"), keepTag) :::

+    List(bassert(DebtCheck, w.pos, "Loop invariant must consume all debt on entry to the loop.")) :::

     // check lockchange on entry to the loop

     Comment("check lockchange on entry to the loop") ::

     (bassert(LockFrame(lkch, etran), w.pos, "Method execution before loop might lock/unlock more than allowed by lockchange clause of loop.")) ::

     // save values of local-variable loop targets

     (for (sv <- saveLocalsV) yield BLocal(Variable2BVarWhere(sv))) :::

-    (for ((v,sv) <- w.LoopTargetsList zip saveLocalsV) yield

-      (new VariableExpr(sv) := new VariableExpr(v))) :::

+    (for ((v,sv) <- w.LoopTargets zip saveLocalsV) yield (new VariableExpr(sv) := new VariableExpr(v))) :::

     // havoc local-variable loop targets

     (w.LoopTargets :\ List[Boogie.Stmt]()) ( (v,vars) => (v match {

       case v: Variable if v.isImmutable => Boogie.Havoc(Boogie.VarExpr("assigned$" + v.id))

@@ -991,14 +991,15 @@ class Translator {
       Comment("check loop invariant definedness") ::

       //(w.LoopTargets.toList map { v: Variable => Boogie.Havoc(Boogie.VarExpr(v.id)) }) :::

       Boogie.Havoc(etran.Heap) :: Boogie.Assign(etran.Mask, ZeroMask) :: Boogie.Assign(etran.Credits, ZeroCredits) ::

-      InhaleWithChecking(invs, "loop invariant definedness") :::

+      InhaleWithChecking(w.oldInvs, "loop invariant definedness") :::

+      tag(InhaleWithChecking(w.newInvs, "loop invariant definedness"), keepTag) :::                  

       bassume(false)

     , Boogie.If(null,

     // 2. CHECK LOOP BODY

       // Renew state: set Mask to ZeroMask and Credits to ZeroCredits, and havoc Heap everywhere except

       // at {old(local),local}.{held,rdheld}

       Havoc(etran.Heap) :: (etran.Mask := ZeroMask) :: (etran.Credits := ZeroCredits) ::

-      Inhale(invs, "loop invariant, body") :::

+      Inhale(w.Invs, "loop invariant, body") :::

       // assume lockchange at the beginning of the loop iteration

       Comment("assume lockchange at the beginning of the loop iteration") ::

       (bassume(LockFrame(lkch, etran))) ::

@@ -1008,13 +1009,14 @@ class Translator {
       (iterStartEtran.oldEtran.Mask := iterStartEtran.Mask) ::  // oldMask is not actually used below

       (iterStartEtran.oldEtran.Credits := iterStartEtran.Credits) ::  // is oldCredits?

       (for (isv <- iterStartLocalsV) yield BLocal(Variable2BVarWhere(isv))) :::

-      (for ((v,isv) <- w.LoopTargetsList zip iterStartLocalsV) yield

+      (for ((v,isv) <- w.LoopTargets zip iterStartLocalsV) yield

          (new VariableExpr(isv) := new VariableExpr(v))) :::

       // evaluate the guard

       isDefined(guard) ::: List(bassume(guard)) :::

       translateStatement(body) ::: 

       // check invariant

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

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

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

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

       // check lockchange after loop iteration

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

@@ -1027,7 +1029,7 @@ class Translator {
      // assume lockchange after the loop

      Comment("assume lockchange after the loop") ::

      (bassume(LockFrame(lkch, etran))) ::

-     Inhale(invs, "loop invariant, after loop") :::

+     Inhale(w.Invs, "loop invariant, after loop") :::

      bassume(!guard)))

   }

 

@@ -1040,18 +1042,17 @@ class Translator {
     // shared locals before block (excluding immutable)

     val before = for (v <- r.locals; if (! v.isImmutable)) yield v;

     // shared locals in block

-    val duringA = for (v <- BlockStmt(r.abs).Declares) yield v;

-    val duringC = for (v <- duringA) yield BlockStmt(r.con).Declares.find(_ == v).get

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

+    val duringC = for (v <- duringA) yield r.con.flatMap(s => s.Declares).find(_ == v).get

     // save locals before (to restore for abstract block)

     val beforeV = for (v <- before) yield new Variable(v.id, v.t)

     // save locals after (to compare with abstract block)

     val afterV = for (v <- before) yield new Variable(v.id, v.t)

 

     Comment("refinement block") ::

-    // TODO: duplicate heap

     (for (c <- conGlobals) yield BLocal(c)) :::

     (for ((c, a) <- conGlobals zip etran.Globals) yield (new VarExpr(c) := a)) :::

-    // TODO: global coupling: assume coupling invariant for locations with positive permission

+    // TODO: inhale heap, global coupling: assume coupling invariant for locations with positive permission

     // save shared local variables

     (for (v <- beforeV) yield BLocal(Variable2BVarWhere(v))) :::            

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

@@ -1059,7 +1060,7 @@ class Translator {
     {

       etran = conTran;

       Comment("run concrete program:") ::

-      translateStatements(r.con)

+      tag(translateStatements(r.con), keepTag)

     } :::

     // run angelically A on the old heap

     Comment("run abstract program:") ::

@@ -1070,18 +1071,18 @@ class Translator {
           Comment("witness declared local variables") ::

           (for (v <- duringA) yield BLocal(Variable2BVarWhere(v))) :::

           (for ((v, w) <- duringA zip duringC) yield (new VariableExpr(v) := new VariableExpr(w))) :::

-          bassert(s.post, r.pos, "Refinement fails to satisfy specification statement post-condition") ::

+          bassert(s.post, r.pos, "Refinement may fail to satisfy specification statement post-condition") ::

           (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)),

           keepTag)

       case _ =>

-        Comment("save locals after") ::

+        // save locals after

         (for (v <- afterV) yield BLocal(Variable2BVarWhere(v))) :::

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

-        Comment("restore locals before") ::

+        // restore locals before

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

         translateStatements(r.abs) :::

-        Comment("assert equality on shared locals") ::

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

@@ -2558,7 +2559,7 @@ object TranslationHelper {
   }

 

   val keepTag = Boogie.Tag("keep")

-  // Assume the only composite statement is If

+  // Assume the only composite statement in Boogie is If

   def tag(l: List[Stmt], t: Boogie.Tag):List[Stmt] =

     for (s <- l) yield {

       s.tags = t :: s.tags;

@@ -2568,7 +2569,7 @@ object TranslationHelper {
       }

       s

     }

-  // Assume the only composite statement is If

+  // Assume the only composite statement in Boogie is If

   def assert2assume(l: List[Stmt]):List[Stmt] =

     if (Chalice.noFreeAssume) l else

       l flatMap {

diff --git a/Chalice/test.bat b/Chalice/test.bat
index b45207b6..4bf5db07 100644
--- a/Chalice/test.bat
+++ b/Chalice/test.bat
@@ -1,7 +1,7 @@
 @echo off

 echo start > Output

 

-set CHALICE=call scala -cp bin chalice.Chalice -nologo -boogie:"C:\\Users\\t-kuayes\\Documents\\Boogie-2010-07-13\\Boogie.exe" 

+set CHALICE=call scala -cp bin chalice.Chalice -nologo 

 

 

 REM to do: AssociationList