Chalice:

* coupling invariants work (with certain restrictions as described in TODO comments)

9 files changed, 305 insertions, 40 deletions

diff --git a/Chalice/refinements/Answer b/Chalice/refinements/Answer
index b513e041..6db2a988 100644
--- a/Chalice/refinements/Answer
+++ b/Chalice/refinements/Answer
@@ -29,3 +29,9 @@ 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

diff --git a/Chalice/refinements/Counter.chalice b/Chalice/refinements/Counter.chalice
new file mode 100644
index 00000000..c9576a13
--- /dev/null
+++ b/Chalice/refinements/Counter.chalice
@@ -0,0 +1,125 @@
+class Counter0 {
+  var x: int;
+  
+  method init() 
+    requires acc(x); 
+    ensures acc(x) && x == 0;
+  {
+    x := 0;  
+  }
+
+  method inc()
+    requires acc(x);
+    ensures acc(x) && x == old(x) + 1;
+  {
+    x := x + 1;
+  } 
+
+  method dec()
+    requires acc(x);
+    ensures acc(x) && x == old(x) - 1;
+  {    
+    x := x - 1;  
+  }
+
+  /** Interesting issues */  
+
+  /* We can expose representation here */
+  method magic1() returns (c: Cell) 
+    requires acc(x)
+    ensures acc(c.n) && x == old(x);
+  {
+    var c [acc(c.n)];
+  }
+
+  /* This should prevent us from exposing representation */
+  method magic2() returns (c: Cell)
+    requires acc(x);
+    ensures acc(x) && x == old(x) && acc(c.n);
+  {
+    var c [acc(c.n)];
+  }
+}
+
+class Counter1 refines Counter0 {
+  var y: int;
+  var z: int;  
+  replaces x by acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0;
+  
+  transforms init() 
+  {
+    replaces * by {this.y := 0; this.z := 0;}
+  }
+
+  transforms inc()
+  {    
+    replaces * by {this.y := this.y + 1;}
+  }
+
+  transforms dec() 
+  {
+    replaces * by {this.z := this.z + 1;}
+  }       
+
+  /** This violates abstraction of x -- we must hold all permissions to x to update it */
+  method magic3() 
+    requires acc(y);    
+  {
+    y := y + 1;
+  }
+
+  /** This does also -- but it also prohibits us from reading part of the state across refinement */
+  method magic4() returns (i)
+    requires acc(y);
+  {
+    i := y;
+  }
+}
+
+class Cell {var n: int}
+/*
+class Counter2 refines Counter1 {
+  var a: Cell;
+  var b: Cell;
+  replaces y, z by acc(a) && acc(b) && acc(a.n) && acc(b.n) && y == a.n && z == b.n;
+  
+  transforms init() 
+  {
+    replaces * by {
+      this.a := new Cell {n := 0};
+      this.b := new Cell {n := 0};
+    }
+  }
+
+  transforms inc() 
+  {
+    replaces * by {this.a.n := this.a.n + 1;}
+  }
+
+  transforms dec()
+  {
+    replaces * by {this.b.n := this.b.n + 1;}
+  }
+
+  transforms magic1() returns (c: Cell)
+  {
+    replaces * by {c := this.a;}
+  }
+
+  transforms magic2() returns (c: Cell)
+  {
+    replaces * by {c := this.a;}
+  }
+
+  transforms magic3()
+  {
+    replaces * by {this.a.n := this.a.n + 1;}
+  }
+
+  transforms magic4() returns (i)
+  {
+    replaces * by {i := this.a.n;}
+  }
+}
+*/
+  
diff --git a/Chalice/refinements/TestCoupling.chalice b/Chalice/refinements/TestCoupling.chalice
new file mode 100644
index 00000000..a178c9b4
--- /dev/null
+++ b/Chalice/refinements/TestCoupling.chalice
@@ -0,0 +1,74 @@
+class A0 {
+  var x: int;
+  var n: int;
+  var k: int;
+  
+  method inc()
+    requires acc(x) && acc(n);
+    ensures acc(x) && x == old(x) + 1;
+  {
+    x := x + 1;
+    n := n + 1;
+  }
+
+  method error() 
+    requires acc(x)
+    ensures acc(x)
+  {
+    x := x + 1;
+  } 
+}
+
+class A1 refines A0 {
+  var y: int;
+  var z: int;  
+  replaces x by acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0;
+  
+  refines inc()
+    ensures y == old(y) + 1
+  {
+    this.y := 1 + this.y;
+    this.n := this.n + 1;    
+  }
+
+  refines error()     
+    ensures acc(y)
+  {
+    this.y := 1 + this.y;
+  }
+}
+
+class B0 {
+  var x: int; 
+  var y: int;
+  
+  method error()
+    requires acc(x);
+    ensures acc(x);
+  {
+    x := x + 1;     
+  }
+  
+  method inc()
+    requires acc(x) && acc(y);
+    ensures acc(x) && acc(y);
+  { 
+    x := x + 1;
+  }
+}
+
+class B1 refines B0 {
+  var z: int;
+  replaces x,y by acc(z) && z == x + y;
+
+  refines error() 
+  {
+    this.z := this.z + 1;
+  }
+
+  refines inc() 
+  {
+    this.z := this.z + 1;
+  }
+}
+   
diff --git a/Chalice/refinements/test.sh b/Chalice/refinements/test.sh
index 73ede390..24dbd6e5 100644
--- a/Chalice/refinements/test.sh
+++ b/Chalice/refinements/test.sh
@@ -13,6 +13,7 @@ TESTS="
   RecFiniteDiff.chalice
   LoopFiniteDiff.chalice
   Pick.chalice
+  TestCoupling.chalice
 "
 
 # Switch to test directory
diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala
index 4e30c621..92c339ea 100644
--- a/Chalice/src/Ast.scala
+++ b/Chalice/src/Ast.scala
@@ -28,10 +28,12 @@ sealed case class Class(classId: String, parameters: List[Class], module: String
   def IsState: Boolean = false

   def IsNormalClass = true

 

-  lazy val Fields: List[Field] = members flatMap {case x: Field => List(x); case _ => Nil}

+  lazy val DeclaredFields = members flatMap {case x: Field => List(x); case _ => Nil}

   lazy val MentionableFields = Fields filter {x => ! x.Hidden}

-  lazy val Invariants: List[MonitorInvariant] = members flatMap {case x: MonitorInvariant => List(x); case _ => Nil}

-  lazy val id2member:Map[String,NamedMember] = Map() ++ {

+  lazy val MonitorInvariants = members flatMap {case x: MonitorInvariant => List(x); case _ => Nil}

+  lazy val Fields:List[Field] = DeclaredFields ++ (if (IsRefinement) refines.Fields else Nil) 

+

+  private lazy val id2member:Map[String,NamedMember] = Map() ++ {

     val named = members flatMap {case x: NamedMember => List(x); case _ => Nil};

     (named map {x => x.Id}) zip named

   }

@@ -59,6 +61,8 @@ sealed case class Class(classId: String, parameters: List[Class], module: String
   var IsRefinement = false

   var refinesId: String = null

   var refines: Class = null

+  lazy val CouplingInvariants = members flatMap {case x: CouplingInvariant => List(x); case _ => Nil}

+  lazy val Replaces: List[Field] = CouplingInvariants flatMap (_.fields)

 }

 

 sealed case class Channel(channelId: String, parameters: List[Variable], where: Expression) extends TopLevelDecl(channelId)

@@ -190,6 +194,13 @@ 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]

+  /* Distribute 100 between fields */

+  def fraction(field: Field) = {

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

+  }

 }

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

   var refines = null: Callable

@@ -229,7 +240,9 @@ case class BlockPat() extends Transform {
 /** Matches any block of code (greedily) and acts as identity */

 case class SkipPat() extends Transform

 /** Replacement pattern for arbitrary block */

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

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

+  if (code.size > 0) pos = code.first.pos

+}

 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 {

diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala
index 36f0e22b..d12ca00f 100644
--- a/Chalice/src/Parser.scala
+++ b/Chalice/src/Parser.scala
@@ -83,9 +83,8 @@ class Parser extends StandardTokenParsers {
     "method" ~> ident ~ formalParameters(true) ~ ("returns" ~> formalParameters(false) ?) ~

     (methodSpec*) ~ blockStatement ^^ {

       case id ~ ins ~ outs ~ spec ~ body =>

-        outs match {

-          case None => Method(id, ins, Nil, spec, body)

-          case Some(outs) => Method(id, ins, outs, spec, body) }}

+        Method(id, ins, outs match {case None => Nil; case Some(outs) => outs}, spec, body)

+    }

   def predicateDecl: Parser[Predicate] =

     ("predicate" ~> ident) ~ ("{" ~> expression <~ "}") ^^ { case id ~ definition => Predicate(id, definition) }

   def functionDecl =

@@ -95,16 +94,18 @@ class Parser extends StandardTokenParsers {
   def conditionDecl =

     "condition" ~> ident ~ ("where" ~> expression ?) <~ Semi ^^ {

       case id ~ optE => Condition(id, optE) }

-  def transformDecl = {

-    "transforms" ~> ident into {id =>

-      assumeAllLocals = true;            

-      formalParameters(true) ~ ("returns" ~> formalParameters(false) ?) ~ (methodSpec*) ~ ("{" ~> transform <~ "}") ^^ {

-        case ins ~ outs ~ spec ~ trans =>

-          assumeAllLocals = false;

-          MethodTransform(id, ins, outs match {case None => Nil; case Some(outs) => outs}, spec, AST.normalize(trans))

-      }

-    }

-  }

+  def transformDecl =

+    ( "refines" ~> ident ~ formalParameters(true) ~ ("returns" ~> formalParameters(false) ?) ~ (methodSpec*) ~ blockStatement ^^ {

+        case id ~ ins ~outs ~ spec ~ body =>

+          MethodTransform(id, ins, outs match {case None => Nil; case Some(outs) => outs}, spec, ProgramPat(body)) }).|(

+      "transforms" ~> ident ~ formalParameters(true) ~ ("returns" ~> formalParameters(false) ?) ~ (methodSpec*) into {case id ~ ins ~ outs ~ spec =>

+        assumeAllLocals = true;

+        "{" ~> transform <~ "}" ^^ {

+          trans =>

+            assumeAllLocals = false;

+            MethodTransform(id, ins, outs match {case None => Nil; case Some(outs) => outs}, spec, AST.normalize(trans))

+        }

+      })

   def couplingDecl = ("replaces" ~> rep1sep(ident, ",") <~ "by") ~ expression <~ Semi ^^ {case ids ~ e => CouplingInvariant(ids, e)}

 

   def formalParameters(immutable: Boolean) =

diff --git a/Chalice/src/PrettyPrinter.scala b/Chalice/src/PrettyPrinter.scala
index da96c796..b2f30c5c 100644
--- a/Chalice/src/PrettyPrinter.scala
+++ b/Chalice/src/PrettyPrinter.scala
@@ -8,7 +8,8 @@ object PrintProgram {
   def P(prog: List[TopLevelDecl]) =

     for (decl <- prog) decl match {

       case cl: Class =>

-        if (cl.IsExternal) print("external ")

+        if (cl.IsExternal)

+          print("external ")

         println("class " + cl.id + " module " + cl.module + (if (cl.IsRefinement) " refines " + cl.refinesId else "") + " {")

         cl.members foreach Member

         println("}")

@@ -24,11 +25,15 @@ object PrintProgram {
     case m: Method =>

       print("  method " + m.id)

       print("("); VarList(m.ins); print(")")

-      if (m.outs != Nil) print(" returns ("); VarList(m.outs); print(")")

+      if (m.outs != Nil) {

+        print(" returns ("); VarList(m.outs); print(")")

+      }

       println

       PrintSpec(m.Spec)

       println("  {")

-      for (s <- m.body) {Spaces(4); Stmt(s, 4)}

+      for (s <- m.body) {

+        Spaces(4); Stmt(s, 4)

+      }

       println("  }")

     case Condition(id, optE) =>

       print("  condition " + id)

@@ -50,14 +55,18 @@ object PrintProgram {
     case m: MethodTransform =>

       print("  method " + m.id);

       print("("); VarList(m.ins); print(")")

-      if (m.outs != Nil) print(" returns ("); VarList(m.outs); print(")")

+      if (m.outs != Nil) {

+        print(" returns ("); VarList(m.outs); print(")")

+      }

       println;

       if (m.refines != null) PrintSpec(m.Spec);

       println("  {");

       if (m.body == null)

         println("    // body transform is not resolved")

       else

-        for (s <- m.body) {Spaces(4); Stmt(s, 4)}

+        for (s <- m.body) {

+          Spaces(4); Stmt(s, 4)

+        }

       println("  }")

     case CouplingInvariant(ids, e) =>

       print("  replaces "); Commas(ids); print(" by "); Expr(e); println(Semi);

@@ -79,9 +88,13 @@ object PrintProgram {
       PrintBlockStmt(ss, indent); println

     case RefinementBlock(ss, old) =>

       println("/* begin of refinement block")

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

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

+      for (s <- ss) {

+        Spaces(indent); Stmt(s, indent)

+      }

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

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

       print("if ("); Expr(guard); print(") ")

@@ -207,7 +220,9 @@ object PrintProgram {
   }

   def PrintBlockStmt(ss: List[Statement], indent: Int) = {

     println("{")

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

+    for (s <- ss) {

+      Spaces(indent+2); Stmt(s, indent+2)

+    }

     Spaces(indent);  print("}")

   }

   def VarList(vv: List[Variable]) = Commas(vv map {v => v.id + ": " + v.t.FullName})

diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala
index bdcc7108..d4adbec3 100644
--- a/Chalice/src/Resolver.scala
+++ b/Chalice/src/Resolver.scala
@@ -1079,7 +1079,7 @@ object Resolver {
  def ResolveTransform(mt: MethodTransform, context: ProgramContext) {

    mt.spec foreach {

      case Precondition(e) =>

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

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

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

@@ -1139,5 +1139,7 @@ object Resolver {
    }

    ResolveExpr(ci.e, context.SetClass(cl).SetMember(ci), false, true)(true)

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

+   // TODO: check coupling invariant may only give permissions to newly declared fields

+   // TODO: check concrete body cannot refer to replaced fields

  }

 }

diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index 915049b2..ef27e635 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -41,7 +41,7 @@ class Translator {
     // add class name

     declarations = Const(className(cl).id, true, TypeName) :: declarations;

     // translate monitor invariant

-    declarations = declarations ::: translateMonitorInvariant(cl.Invariants, cl.pos);

+    declarations = declarations ::: translateMonitorInvariant(cl.MonitorInvariants, cl.pos);

     // translate each member

     for(member <- cl.members) {

       declarations = declarations ::: translateMember(member);

@@ -323,6 +323,20 @@ class Translator {
   }

 

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

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

+      case _: PermissionExpr => throw new Exception("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

+

     // check definedness of refinement specifications

     Proc(mt.FullName + "$checkDefinedness",

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

@@ -332,12 +346,13 @@ class Translator {
         DefinePreInitialState :::

         bassume(CanAssumeFunctionDefs) ::

         // check precondition

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

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

         DefineInitialState :::

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

         Havoc(etran.Heap) ::

         // check postcondition

-        InhaleWithChecking(Postconditions(mt.Spec), "postcondition")

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

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

       ) ::

     // check correctness of refinement

     Proc(mt.FullName,

@@ -349,15 +364,16 @@ class Translator {
           bassume(CurrentModule ==@ Boogie.VarExpr(ModuleName(currentClass))) ::

           bassume(CanAssumeFunctionDefs) ::

           DefinePreInitialState :::

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

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

           DefineInitialState :::

           translateStatements(mt.body) :::

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

-          tag(

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

-            keepTag)

+          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"), keepTag)

         }

       )

+

   }

 

   def DebtCheck() = {

@@ -1053,9 +1069,9 @@ class Translator {
     val afterV = for (v <- before) yield new Variable(v.id, v.t)

 

     Comment("refinement block") ::

+    // save heap

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

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

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

@@ -1071,7 +1087,7 @@ class Translator {
     r.abs match {

       case List(s: SpecStmt) =>

         tag(

-          Comment("witness declared local variables") ::

+          Comment("give witnesses to 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 may fail to satisfy specification statement post-condition") ::

@@ -1093,8 +1109,18 @@ class Translator {
             bassert(new VariableExpr(v) ==@ new VariableExpr(w), r.pos, "Refinement may produce different value for a declared local variable: " + v.id)),

           keepTag)

     }} :::

+    {

+      val (v,ve) = NewBVar("this", tref, true)

+      // TODO: we only preserve concrete fields of "this" at the moment       

+      // TODO: check for mask coupling

+

+      // assert equality on shared globals (except those that are replaced)

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

+      // copy new globals from concrete to abstract heap (to preserve their values across refinement blocks and establish invariant)

+      (for (f <- currentClass.DeclaredFields) yield absTran.Heap.store(VarExpr("this"), VarExpr(f.FullName), conTran.Heap.select(VarExpr("this"), f.FullName)))

+    } :::

     Comment("end of refinement block")

-    // TODO: global coupling: assert coupling invariants for locations with positive, preserve permissions?

   }

 

 

@@ -1241,7 +1267,7 @@ class Translator {
     val shV = new Variable("sh", new Type(obj.typ))

     val sh = new VariableExpr(shV)

     BLocal(Variable2BVar(shV)) :: Boogie.Assign(TrExpr(sh), TrExpr(obj)) ::

-    tran.Inhale(obj.typ.Invariants map

+    tran.Inhale(obj.typ.MonitorInvariants map

            (inv => SubstThis(inv.e, sh)) map

            (inv => (if (readonly) SubstRd(inv) else inv)), "monitor invariant", false)

   }

@@ -1249,7 +1275,7 @@ class Translator {
     val shV = new Variable("sh", new Type(obj.typ))

     val sh = new VariableExpr(shV)

     BLocal(Variable2BVar(shV)) :: Boogie.Assign(TrExpr(sh), TrExpr(obj)) ::

-    tran.Exhale(obj.typ.Invariants map

+    tran.Exhale(obj.typ.MonitorInvariants map

            (inv => SubstThis(inv.e, sh)) map

            (inv => (if (readonly) SubstRd(inv) else inv, msg)), "monitor invariant", false)

   }

@@ -1257,7 +1283,7 @@ class Translator {
     val shV = new Variable("sh", new Type(obj.typ))

     val sh = new VariableExpr(shV)

     BLocal(Variable2BVar(shV)) :: Boogie.Assign(TrExpr(sh), TrExpr(obj)) ::

-    Inhale(obj.typ.Invariants map

+    Inhale(obj.typ.MonitorInvariants map

            (inv => SubstThis(inv.e, sh)) map

            (inv => (if (readonly) SubstRd(inv) else inv)), "monitor invariant")

   }

@@ -1265,7 +1291,7 @@ class Translator {
     val shV = new Variable("sh", new Type(obj.typ))

     val sh = new VariableExpr(shV)

     BLocal(Variable2BVar(shV)) :: Boogie.Assign(TrExpr(sh), TrExpr(obj)) ::

-    Exhale(obj.typ.Invariants map

+    Exhale(obj.typ.MonitorInvariants map

            (inv => SubstThis(inv.e, sh)) map

            (inv => (if (readonly) SubstRd(inv) else inv, msg)), "monitor invariant")

   }

@@ -2225,6 +2251,7 @@ object TranslationHelper {
     val result = expr match {

       case Access(e, Full) => Access(e, Frac(fraction))

       case And(lhs, rhs) => And(FractionOf(lhs, fraction), FractionOf(rhs, fraction))

+      case Implies(lhs, rhs) => Implies(lhs, FractionOf(rhs, fraction))

       case _ if ! expr.isInstanceOf[PermissionExpr] => expr

       case _ => throw new Exception("  " + expr.pos + ": Scaling non-full permissions is not supported yet." + expr);

     }

@@ -2236,6 +2263,7 @@ object TranslationHelper {
     expr match {

       case Access(e, Full) => true

       case And(lhs, rhs) => canTakeFractionOf(lhs) && canTakeFractionOf(rhs)

+      case Implies(lhs, rhs) => canTakeFractionOf(rhs)

       case _ if ! expr.isInstanceOf[PermissionExpr] => true

       case _ => false

     }