10 files changed, 5208 insertions, 0 deletions
diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala
new file mode 100644
index 00000000..44d97290
--- /dev/null
+++ b/Chalice/src/Ast.scala
@@ -0,0 +1,384 @@
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+import scala.util.parsing.input.Position
+import scala.util.parsing.input.Positional
+
+trait ASTNode extends Positional
+
+// classes and types
+
+sealed case class Class(id: String, parameters: List[Class], module: String, members: List[Member]) extends ASTNode {
+  var mm = Map[String,Member]()
+  def LookupMember(id: String): Option[Member] = {
+    if (mm.keys exists { i => i.equals(id)})
+      Some(mm(id))
+    else if (IsRef && (RootClass.mm contains id)) {
+      val m = RootClass.mm(id)
+      if (m.Hidden) None else Some(m)
+    } else
+      None
+  }
+  def IsInt: boolean = false
+  def IsBool: boolean = false
+  def IsRef: boolean = true
+  def IsNull: boolean = false
+  def IsMu: boolean = false
+  def IsSeq: boolean = false
+  def IsToken: boolean = false
+  def IsState: boolean = false
+  def IsNormalClass = true;
+  var IsExternal = false;  // says whether or not to compile the class (compilation ignores external classes)
+
+  def Fields: List[Field] = {
+    members flatMap (m => m match { case f:Field => List(f) case _ => List() })
+  }
+  def Invariants: List[MonitorInvariant] = {
+    (members :\ List[MonitorInvariant]()) { (m,list) => m match {
+      case m:MonitorInvariant => m :: list
+      case _ => list }}
+  }
+  def FullName: String = if(parameters.isEmpty) id else id + "<" + parameters.tail.foldLeft(parameters.head.FullName){(a, b) => a + ", " + b.FullName} + ">"
+}
+
+case class SeqClass(parameter: Class) extends Class("seq", List(parameter), "default", Nil) {
+  override def IsRef = false;
+  override def IsSeq = true;
+  override def IsNormalClass = false;
+}
+object IntClass extends Class("int", Nil, "default", Nil) {
+  override def IsRef = false
+  override def IsInt = true
+  override def IsNormalClass = false;
+}
+object BoolClass extends Class("bool", Nil, "default", Nil) {
+  override def IsRef = false
+  override def IsBool = true
+  override def IsNormalClass = false;
+}
+object NullClass extends Class("null", Nil, "default", Nil) {
+  override def IsNull = true
+  override def IsNormalClass = false;
+}
+object MuClass extends Class("$Mu", Nil, "default", Nil) {
+  override def IsRef = false
+  override def IsMu = true
+  override def IsNormalClass = false;
+}
+case class TokenClass(c: Type, m: String) extends Class("token", Nil, "default", List( 
+  new SpecialField("joinable", new Type(BoolClass))
+))
+{
+  var method = null: Method;
+  override def IsRef = true;
+  override def IsToken = true;
+  override def IsNormalClass = false;
+  override def FullName: String = "token<" + c.FullName + "." + m + ">"
+  mm = mm.+(("joinable", Fields(0)));
+}
+
+object RootClass extends Class("$root", Nil, "default", List(
+  new SpecialField("mu", new Type(MuClass)),
+  new SpecialField("held", new Type(BoolClass)){ override val Hidden = true },
+  new SpecialField("rdheld", new Type(BoolClass)){ override val Hidden = true }
+  ))  // joinable and held are bool in Chalice, but translated into an int in Boogie
+{
+  def MentionableFields = Fields filter {fld => fld.id != "held" && fld.id != "rdheld"}
+}
+
+sealed case class Type(id: String, params: List[Type]) extends ASTNode {  // denotes the use of a type
+  var typ: Class = null
+  def this(id: String) = { this(id, Nil); }
+  def this(cl: Class) = { this(cl.id); typ = cl }
+  def FullName: String = if(params.isEmpty) id else id + "<" + params.tail.foldLeft(params.head.FullName){(a, b) => a + ", " + b.FullName} + ">"
+}
+
+sealed case class TokenType(C: Type, m: String) extends Type("token", Nil) {  // denotes the use of a type
+  typ = TokenClass(C, m);
+  var method = null : Method;
+
+  override def FullName: String = "token<" + C.FullName + "." + m + ">"
+}
+
+// members
+
+sealed abstract class Member extends ASTNode {
+  val Hidden: boolean = false  // hidden means not mentionable in source
+}
+case class MonitorInvariant(e: Expression) extends Member
+sealed abstract class NamedMember(id: String) extends Member {
+  val Id = id
+  var Parent: Class = null
+  def FullName = Parent.id + "." + Id
+}
+case class Field(id: String, typ: Type) extends NamedMember(id) {
+  val IsGhost: boolean = false
+}
+case class SpecialField(name: String, tp: Type) extends Field(name, tp) {  // direct assignments are not allowed to a SpecialField
+  override def FullName = id
+}
+case class Method(id: String, ins: List[Variable], outs: List[Variable], spec: List[Specification], body: List[Statement]) extends NamedMember(id)
+case class Predicate(id: String, definition: Expression) extends NamedMember(id)
+case class Function(id: String, ins: List[Variable], out: Type, spec: List[Specification], definition: Expression) extends NamedMember(id) {
+  def apply(rec: Expression, args: List[Expression]): FunctionApplication = {
+    val result = FunctionApplication(rec, id, args);
+    result.f = this;
+    result
+  }
+}
+class Variable(name: String, typ: Type) extends ASTNode {
+  val id = name
+  val t = typ
+  val IsGhost: boolean = false
+  val IsImmutable: boolean = false
+  val UniqueName = {
+    val n = S_Variable.VariableCount
+    S_Variable.VariableCount = S_Variable.VariableCount + 1
+    name + "#" + n
+  }
+}
+object S_Variable { var VariableCount = 0 }
+class ImmutableVariable(id: String, t: Type) extends Variable(id, t) {
+  override val IsImmutable: boolean = true
+}
+class SpecialVariable(name: String, typ: Type) extends Variable(name, typ) {
+  override val UniqueName = name
+}
+
+sealed abstract class Specification extends ASTNode
+case class Precondition(e: Expression) extends Specification
+case class Postcondition(e: Expression) extends Specification
+case class LockChange(ee: List[Expression]) extends Specification
+
+// statements
+
+sealed abstract class Statement extends ASTNode
+case class Assert(e: Expression) extends Statement
+case class Assume(e: Expression) extends Statement
+case class BlockStmt(ss: List[Statement]) extends Statement
+case class IfStmt(guard: Expression, thn: BlockStmt, els: Option[Statement]) extends Statement
+case class WhileStmt(guard: Expression,
+                     invs: List[Expression], lkch: List[Expression],
+                     body: BlockStmt) extends Statement {
+  var LoopTargets: Set[Variable] = null
+  lazy val LoopTargetsList: List[Variable] = {  // to be called only after LoopTargets has been completely filled in
+    var vv = List[Variable]()
+    LoopTargets foreach (v => vv = v :: vv)
+    vv
+  }
+}
+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 =
+    if (const)
+      new ImmutableVariable(id, t){override val IsGhost = ghost}
+    else
+      new Variable(id, t){override val IsGhost = ghost}
+}
+case class Call(lhs: List[VariableExpr], obj: Expression, id: String, args: List[Expression]) extends Statement {
+  var m: Method = null
+}
+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
+case class Unshare(obj: Expression) extends Statement
+case class Acquire(obj: Expression) extends Statement
+case class Release(obj: Expression) extends Statement
+case class RdAcquire(obj: Expression) extends Statement
+case class RdRelease(obj: Expression) extends Statement
+case class Downgrade(obj: Expression) extends Statement
+case class Lock(obj: Expression, b: BlockStmt, rdLock: boolean) extends Statement
+case class Free(obj: Expression) extends Statement
+case class CallAsync(declaresLocal: boolean, lhs: VariableExpr, obj: Expression, id: String, args: List[Expression]) extends Statement {
+  var local: Variable = null
+  var m: Method = null
+}
+case class JoinAsync(lhs: List[VariableExpr], token: Expression) extends Statement {
+  var m: Method = null
+}
+
+case class Fold(pred: PermissionExpr) extends Statement
+case class Unfold(pred: PermissionExpr) extends Statement
+
+// expressions
+
+sealed abstract class RValue extends ASTNode {
+  var typ: Class = null
+}
+case class NewRhs(id: String, initialization: List[Init]) extends RValue
+case class Init(id: String, e: Expression) extends ASTNode {
+  var f: Field = null;
+}
+sealed abstract class Expression extends RValue
+sealed abstract class Literal extends Expression
+case class IntLiteral(n: int) extends Literal
+case class BoolLiteral(b: boolean) extends Literal
+case class NullLiteral extends Literal
+case class MaxLockLiteral extends Literal
+case class LockBottomLiteral extends Literal
+case class VariableExpr(id: String) extends Expression {
+  var v: Variable = null
+  def this(vr: Variable) = { this(vr.id); v = vr; typ = vr.t.typ }
+}
+case class Result extends Expression
+sealed abstract class ThisExpr extends Expression {
+  override def equals(other: Any): Boolean = {
+    // needed in autoMagic, which checks for syntactic equality using equals
+    other.isInstanceOf[ThisExpr]
+  }
+}
+case class ExplicitThisExpr extends ThisExpr
+case class ImplicitThisExpr extends ThisExpr
+case class MemberAccess(e: Expression, id: String) extends Expression {
+  var isPredicate: Boolean = false;
+  var f: Field = null
+  var predicate: Predicate = null
+}
+case class IfThenElse(con: Expression, then: Expression, els: Expression) extends Expression
+
+sealed abstract class PermissionExpr extends Expression {
+  def getMemberAccess : MemberAccess
+}
+
+case class Access(e: MemberAccess, perm: Option[Expression]) extends PermissionExpr {
+  def getMemberAccess = e : MemberAccess;
+}
+case class RdAccess(e: MemberAccess, perm: Option[Option[Expression]]) extends PermissionExpr {
+  def getMemberAccess = e : MemberAccess;
+}
+
+case class AccessAll(obj: Expression, perm: Option[Expression]) extends Expression
+case class RdAccessAll(obj: Expression, perm: Option[Option[Expression]]) extends Expression
+
+case class Holds(e: Expression) extends Expression
+case class RdHolds(e: Expression) extends Expression
+case class Assigned(id: String) extends Expression {
+  var v: Variable = null
+}
+case class Old(e: Expression) extends Expression
+case class Not(e: Expression) extends Expression
+case class FunctionApplication(obj: Expression, id: String, args: List[Expression]) extends Expression {
+  var f: Function = null
+}
+case class Unfolding(pred: PermissionExpr, in: Expression) extends Expression
+sealed abstract class BinaryExpr(e0: Expression, e1: Expression) extends Expression {
+  def E0 = e0
+  def E1 = e1
+  def ExpectedLhsType: Class = BoolClass  // sometimes undefined
+  def ExpectedRhsType: Class = BoolClass  // sometimes undefined
+  val ResultType: Class = BoolClass
+  val OpName: String
+}
+case class Iff(e0: Expression, e1: Expression) extends BinaryExpr(e0,e1) {
+  override val OpName = "<==>"
+}
+case class Implies(e0: Expression, e1: Expression) extends BinaryExpr(e0,e1) {
+  override val OpName = "==>"
+}
+case class And(e0: Expression, e1: Expression) extends BinaryExpr(e0,e1) {
+  override val OpName = "&&"
+}
+case class Or(e0: Expression, e1: Expression) extends BinaryExpr(e0,e1) {
+  override val OpName = "||"
+}
+sealed abstract class ArithmeticExpr(e0: Expression, e1: Expression) extends BinaryExpr(e0,e1) {
+  override def ExpectedLhsType = IntClass
+  override def ExpectedRhsType = IntClass
+  override val ResultType = IntClass
+}
+case class Plus(e0: Expression, e1: Expression) extends ArithmeticExpr(e0,e1) {
+  override val OpName = "+"
+}
+case class Minus(e0: Expression, e1: Expression) extends ArithmeticExpr(e0,e1) {
+  override val OpName = "-"
+}
+case class Times(e0: Expression, e1: Expression) extends ArithmeticExpr(e0,e1) {
+  override val OpName = "*"
+}
+case class Div(e0: Expression, e1: Expression) extends ArithmeticExpr(e0,e1) {
+  override val OpName = "/"
+}
+case class Mod(e0: Expression, e1: Expression) extends ArithmeticExpr(e0,e1) {
+  override val OpName = "%"
+}
+sealed abstract class CompareExpr(e0: Expression, e1: Expression) extends BinaryExpr(e0,e1) {
+  override def ExpectedLhsType = IntClass
+  override def ExpectedRhsType = IntClass
+}
+sealed abstract class EqualityCompareExpr(e0: Expression, e1: Expression) extends CompareExpr(e0,e1) {
+  override def ExpectedLhsType = throw new Exception("EqualityCompareExpr does not have a single ExpectedArgsType")
+  override def ExpectedRhsType = throw new Exception("EqualityCompareExpr does not have a single ExpectedArgsType")
+}
+case class Eq(e0: Expression, e1: Expression) extends EqualityCompareExpr(e0,e1) {
+  override val OpName = "=="
+}
+case class Neq(e0: Expression, e1: Expression) extends EqualityCompareExpr(e0,e1) {
+  override val OpName = "!="
+}
+case class Less(e0: Expression, e1: Expression) extends CompareExpr(e0,e1) {
+  override val OpName = "<"
+}
+case class AtMost(e0: Expression, e1: Expression) extends CompareExpr(e0,e1) {
+  override val OpName = "<="
+}
+case class AtLeast(e0: Expression, e1: Expression) extends CompareExpr(e0,e1) {
+  override val OpName = ">="
+}
+case class Greater(e0: Expression, e1: Expression) extends CompareExpr(e0,e1) {
+  override val OpName = ">"
+}
+case class LockBelow(e0: Expression, e1: Expression) extends CompareExpr(e0,e1) {
+  override def ExpectedLhsType = throw new Exception("LockBelow does not have a single ExpectedArgsType")
+  override def ExpectedRhsType = throw new Exception("LockBelow does not have a single ExpectedArgsType")
+  override val OpName = "<<"
+}
+sealed abstract class Quantification(is: List[String], seq: Expression, e: Expression) extends Expression {
+  def Quantor: String; 
+  def Is = is
+  def Seq = seq
+  def E = e
+  var variables = null: List[Variable];
+}
+case class Forall(is: List[String], seq: Expression, e: Expression) extends Quantification(is, seq, e) {
+  override def Quantor = "forall"
+}
+
+// sequences
+
+case class EmptySeq(t: Type) extends Literal
+case class ExplicitSeq(elems: List[Expression]) extends Expression
+case class Range(min: Expression, max: Expression /* non-inclusive*/) extends Expression
+case class Append(s0: Expression, s1: Expression) extends SeqAccess(s0, s1) {
+  override val OpName = "++"
+}
+ sealed abstract case class SeqAccess(e0: Expression, e1: Expression) extends BinaryExpr(e0, e1)
+case class Length(e: Expression) extends Expression
+case class At(s: Expression, n: Expression) extends SeqAccess(s, n) {
+  override val OpName = "@"
+}
+case class Drop(s: Expression, n: Expression) extends SeqAccess(s, n) {
+  override val OpName = ""
+}
+case class Take(s: Expression, n: Expression) extends SeqAccess(s, n) {
+  override val OpName = ""
+}
+
+
+// eval
+
+case class Eval(h: EvalState, e: Expression) extends Expression
+sealed abstract class EvalState {
+  def target(): Expression;
+}
+case class AcquireState(obj: Expression) extends EvalState {
+  def target() = obj
+}
+case class ReleaseState(obj: Expression) extends EvalState {
+  def target() = obj
+}
+case class CallState(token: Expression, obj: Expression, id: String, args: List[Expression]) extends EvalState {
+  var m = null: Method;
+  def target() = token;
+}
diff --git a/Chalice/src/Boogie.scala b/Chalice/src/Boogie.scala
new file mode 100644
index 00000000..492e0669
--- /dev/null
+++ b/Chalice/src/Boogie.scala
@@ -0,0 +1,270 @@
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+import scala.util.parsing.input.Position
+import scala.util.parsing.input.NoPosition
+
+object Boogie {
+  
+  sealed abstract class Decl
+  case class Const(id: String, unique: boolean, t: BType) extends Decl
+  case class Proc(id: String, ins: List[BVar], outs: List[BVar],
+                  mod: List[String], PrePost: List[String],
+                  body: List[Stmt]) extends Decl
+  case class Function(id: String, ins: List[BVar], out: BVar) extends Decl
+  case class Axiom(expr: Expr) extends Decl
+
+  sealed abstract class BType
+  case class NamedType(s: String) extends BType
+  case class ClassType(cl: Class) extends BType
+  case class IndexedType(id: String, t: BType) extends BType
+
+  sealed abstract class Stmt {
+    def Locals = List[BVar]()
+  }
+  case class Comment(comment: String) extends Stmt
+  case class Assert(e: Expr) extends Stmt {
+    def this(e: Expr, p: Position, txt: String) = { this(e); this.pos = p; this.message = txt; this } 
+    var pos = NoPosition : Position
+    var message = "" : String
+  }
+  case class Assume(e: Expr) extends Stmt
+  case class Assign(lhs: Expr, rhs: Expr) extends Stmt
+  case class AssignMap(lhs: Expr, index: Expr, rhs: Expr) extends Stmt
+  case class Havoc(x: Expr) extends Stmt
+  case class MapUpdate(map: Expr, arg0: Expr, arg1: String, rhs: Expr) extends Stmt {
+    def this(map: Expr, arg0: Expr, rhs: Expr) = this(map, arg0, null, rhs)
+  }
+  case class If(guard: Expr, thn: List[Stmt], els: List[Stmt]) extends Stmt {
+    override def Locals = (thn flatMap (_.Locals)) ::: (els flatMap (_.Locals))
+  }
+  case class LocalVar(x: BVar) extends Stmt {
+    def this(id: String, tp: BType) = this(BVar(id, tp))
+
+    override def Locals = List(x)
+  }
+
+  sealed abstract class Expr {
+    def &&(that: Expr) = BinaryExpr("&&", this, that)
+    def ||(that: Expr) = BinaryExpr("||", this, that)
+    def ==@(that: Expr) = BinaryExpr("==", this, that)
+    def !=@(that: Expr) = BinaryExpr("!=", this, that)
+    def Equals(that: Expr) = BinaryExpr("==", this, that)
+    def ==>(that: Expr) = BinaryExpr("==>", this, that)
+    def <==>(that: Expr) = BinaryExpr("<==>", this, that)
+    def unary_! = UnaryExpr("!", this)
+    def <=(that: Expr) = BinaryExpr("<=", this, that)
+    def <(that: Expr) = BinaryExpr("<", this, that)
+    def >=(that: Expr) = BinaryExpr(">=", this, that)
+    def >(that: Expr) = BinaryExpr(">", this, that)
+    def +(that: Expr) = BinaryExpr("+", this, that)
+    def -(that: Expr) = BinaryExpr("-", this, that)
+    def *(that: Expr) = BinaryExpr("*", this, that)
+    def /(that: Expr) = BinaryExpr("/", this, that)
+    def %(that: Expr) = BinaryExpr("%", this, that)
+    def := (that: Expr) = Assign(this, that)
+    def select(e: Expr, f: Expr) = new MapSelect(this, e, PrintExpr(f))
+    def store(e: Expr, f: Expr, rhs: Expr) = MapUpdate(this, e, PrintExpr(f), rhs)
+  }
+  case class IntLiteral(n: int) extends Expr
+  case class BoolLiteral(b: boolean) extends Expr
+  case class Null extends Expr
+  case class VarExpr(id: String) extends Expr {
+    def this(v: BVar) = this(v.id)
+  }
+  case class MapSelect(map: Expr, arg0: Expr, arg1: String) extends Expr {
+    def this(map: Expr, arg0: Expr) = this(map, arg0, null) // for one-dimensional maps
+    def this(map: Expr, arg0: Expr, arg1: String, arg2: String) = // for 3-dimensional maps
+      this(MapSelect(map, arg0, arg1), VarExpr(arg2), null)
+  }
+  case class MapStore(map: Expr, arg0: String, rhs: Expr) extends Expr
+  case class Old(e: Expr) extends Expr
+  case class UnaryExpr(op: String, e: Expr) extends Expr
+  case class BinaryExpr(op: String, e0: Expr, e1: Expr) extends Expr
+  case class FunctionApp(f: String, args: List[Expr]) extends Expr {
+    def this(f: String, a0: Expr) = this(f, List(a0))
+    def this(f: String, a0: Expr, a1: Expr) = this(f, List(a0, a1))
+    def this(f: String, a0: Expr, a1: Expr, a2: Expr) = this(f, List(a0, a1, a2))
+  }
+  case class Forall(ta: List[TVar], xs: List[BVar], triggers: List[Expr], body: Expr) extends Expr {
+    def this(xs: List[BVar], triggers: List[Expr], body: Expr) = this(List(), xs, triggers, body)
+    def this(x: BVar, body: Expr) = this(List(), List(x), List(), body)
+    def this(t: TVar, x: BVar, body: Expr) = this(List(t), List(x), List(), body)
+  }
+  case class Exists(xs: List[BVar], triggers: List[Expr], body: Expr) extends Expr {
+    def this(x: BVar, body: Expr) = this(List(x), List(), body)
+  }
+  case class Ite(con: Expr, then: Expr, els: Expr) extends Expr
+
+  case class BVar(id: String, t: BType) {
+    def this(id: String, t: BType, uniquifyName: boolean) =
+      this(if (uniquifyName) {
+             val n = S_BVar.VariableCount
+             S_BVar.VariableCount = S_BVar.VariableCount + 1
+             id + "#_" + n
+           } else {
+             id
+           }, t)
+    val where: Expr = null
+  }
+  object S_BVar { var VariableCount = 0 }
+  def NewBVar(id: String, t: BType, uniquifyName: boolean) = {
+    val v = new Boogie.BVar(id, t, uniquifyName)
+    val e = new Boogie.VarExpr(v)
+    (v,e)
+  }
+  case class TVar(id: String) {
+    def this(id: String, uniquifyName: boolean) =
+      this(if (uniquifyName) {
+             val n = S_TVar.VariableCount
+             S_TVar.VariableCount = S_TVar.VariableCount + 1
+             id + "#_" + n
+           } else {
+             id
+           })
+    val where: Expr = null
+  }
+  object S_TVar { var VariableCount = 0 }
+  def NewTVar(id: String) = {
+    val v = new Boogie.TVar(id, true)
+    val e = new Boogie.NamedType(v.id)
+    (v,e)
+  }
+
+ // def out(s: String) = Console.out.print(s)
+  var indentLevel = 1
+  def indent: String = {
+    def doIndent(i: int): String = {
+      if(i==0) { "" } else { "  " + doIndent(i-1) }
+    }
+    doIndent(indentLevel);
+  }
+
+  def IndentMore(what: => String) = {
+    val prev = indentLevel
+    indentLevel = indentLevel + 1
+    val result = what
+    indentLevel = prev
+    result
+  }
+  def nl = System.getProperty("line.separator");
+  
+  def Print[T](list: List[T], sep: String, p: T => String): String = list match {
+    case Nil => ""
+    case x :: Nil => p(x)
+    case x :: xs => p(x) + sep + Print(xs, sep, p)
+  }
+  def PrintType(t: BType): String = t match {
+    case nt@ NamedType(s) =>
+      s
+    case ClassType(cl) =>
+      if (cl.IsRef) "ref" else cl.id
+    case IndexedType(id,t) =>
+      id + " (" + PrintType(t) + ")"
+  }
+  def Print(d: Decl): String = d match {
+    case Const(id, u, t) =>
+      "const " + (if (u) "unique " else "" ) + id + ": " + PrintType(t) + ";" + nl
+    case p: Proc =>
+      "procedure " + p.id +
+      "(" + Print(p.ins, ", ", PrintVar) + ")" +
+      " returns (" + Print(p.outs, ", ", PrintVar) + ")" + nl + 
+      (p.mod match {
+        case Nil => ""
+        case x :: xs =>
+          indent +  "modifies " +
+          Print(p.mod, ", ", { s: String => s }) +
+          ";" + nl
+      }) + 
+      Print(p.PrePost, nl, { spec: String => indent + spec }) + nl +
+      "{" + nl + 
+      Print(p.body flatMap (_.Locals), "", { v:BVar => indent + "var " + PrintVar(v) + ";" + nl}) + 
+      Print(p.body, "", PrintStmt) + 
+      "}" + nl
+    case Function(id, ins, out) =>
+      "function " + id + "(" + Print(ins, ", ", PrintVar) + ") returns (" + PrintVar(out) + ");" + nl
+    case Axiom(e) =>
+      "axiom " + PrintExpr(e) + ";" + nl
+  }
+  def PrintVar(v: BVar): String = {
+    v.id + ": " + PrintType(v.t) +
+    (if (v.where != null) {" where " + PrintExpr(v.where) } else { "" })
+  }
+  def PrintStmt(s: Stmt): String = s match {
+    case Comment(msg) => indent +  "// " +  msg + nl
+    case assert@Assert(e) => indent +  "assert " + "{:msg \"  " + assert.pos + ": " + assert.message + "\"}" + " " + PrintExpr(e) + ";" + nl
+    case Assume(e) => indent + "assume " + PrintExpr(e) +  ";" + nl
+    case If(guard, thn, els) =>
+      indent + "if (" +
+      (if (guard == null) "*" else PrintExpr(guard)) +
+      ") {" +  nl + 
+      IndentMore { Print(thn, "", PrintStmt)  } + 
+      indent +  "} else {"  + nl + 
+      IndentMore { Print(els, "", PrintStmt)  } + 
+      indent + "}" + nl
+    case Assign(lhs, rhs) =>
+      indent + PrintExpr(lhs) + " := " + PrintExpr(rhs) + ";" + nl
+    case AssignMap(lhs, index, rhs) =>
+      indent + PrintExpr(lhs) + "[" + PrintExpr(index) + "] := " + PrintExpr(rhs) + ";" + nl
+    case Havoc(lhs) =>
+      indent + "havoc " + PrintExpr(lhs) + ";" + nl
+    case MapUpdate(map, a0, a1, rhs) =>
+      indent + PrintExpr(map) + "[" +
+      PrintExpr(a0) +
+      (if (a1 != null) { ", " + a1 } else { "" }) +
+      "] := " + 
+      PrintExpr(rhs) + ";" + nl
+    case _:LocalVar => "" /* print nothing */
+  }
+  def PrintExpr(e: Expr): String = {
+    PrintExpr(e, false)
+  }
+  def PrintExpr(e: Expr, useParens: boolean): String = e match {
+    case IntLiteral(n) => n.toString
+    case BoolLiteral(b) => b.toString
+    case Null() => "null"
+    case VarExpr(id) => id
+    case MapSelect(map, arg0, arg1) =>
+      PrintExpr(map) + "[" + PrintExpr(arg0, false) + 
+      (if (arg1 != null) { ", " + arg1 } else { "" }) +
+      "]"
+    case MapStore(map, arg0, rhs) =>
+      PrintExpr(map) + "[" + arg0 + " := " + PrintExpr(rhs, false) + "]"
+    case Old(e) => "old(" + PrintExpr(e, false) + ")"
+    case UnaryExpr(op, e) =>
+      (if (useParens)  { "(" } else "") +
+      op + PrintExpr(e, true) +
+      (if (useParens) ")" else "" )
+    case BinaryExpr(op, e0, e1) =>
+      // reduce parentheses in a special common case:
+      val binIsAndImpIff = op=="&&" || op=="==>" || op=="<==>";
+      def IsAnd(e: Expr) = e match { case BinaryExpr(op,_,_) if op=="&&" => true case _ => false }
+      (if (useParens) "(" else "") + PrintExpr(e0, !(binIsAndImpIff && IsAnd(e0))) + 
+      " " + op + " " + 
+      PrintExpr(e1, !(binIsAndImpIff && IsAnd(e1))) +
+      (if (useParens) ")" else "")
+    case FunctionApp(f, args) =>
+      f + "(" +
+      Print(args, ", ", { e: Expr => PrintExpr(e, false) }) +
+      ")"
+    case Ite(con, then, els) =>
+      "ite(" + PrintExpr(con) + ", " + PrintExpr(then) + ", " + PrintExpr(els) + ")"
+    case Forall(ts, xs, triggers, body) =>
+      "(forall" +
+      (if (ts.length == 0) " " else "<" + Print(ts, ", ", { x: TVar => x.id }) + "> ") +
+      Print(xs, ", ", { x: BVar => x.id +  ": " + PrintType(x.t) }) +
+      " :: " +
+      Print(triggers , "", { s: Expr => "{" + PrintExpr(s) + "} " }) +
+      PrintExpr(body) +
+      ")"
+    case Exists(xs, triggers, body) =>
+      "(exists " +
+      Print(xs, ", ", { x: BVar => x.id +  ": " + PrintType(x.t) }) +
+      " :: " +
+      Print(triggers , "", { s: Expr => "{" + PrintExpr(s) + "} " }) +
+      PrintExpr(body) +
+      ")"
+  }
+}
diff --git a/Chalice/src/Chalice.cs b/Chalice/src/Chalice.cs
new file mode 100644
index 00000000..f4a804e7
--- /dev/null
+++ b/Chalice/src/Chalice.cs
@@ -0,0 +1,76 @@
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System.Collections.Generic;
+using System.Linq;
+
+namespace Chalice
+{
+    public class ImmutableList<E>
+    {
+        private List<E> list;
+        
+        public ImmutableList() {
+            list = new List<E>();
+        }
+
+        public ImmutableList(IEnumerable<E> elems)
+        {
+            list = new List<E>(elems);
+        }
+
+        public ImmutableList<E> Append(ImmutableList<E> other)
+        {
+            var res = new ImmutableList<E>();
+            res.list.AddRange(list);
+            res.list.AddRange(other.list);
+            return res;
+        }
+
+        public E At(int index)
+        {
+            return list[index];
+        }
+
+        public ImmutableList<E> Take(int howMany)
+        {
+            var res = new ImmutableList<E>(this.list.Take(howMany));
+            return res;
+        }
+
+        public ImmutableList<E> Drop(int howMany)
+        {
+            var res = new ImmutableList<E>(this.list.Skip(howMany));
+            return res;
+        }
+
+        public int Length
+        {
+            get
+            {
+                return list.Count;
+            }
+        }
+
+        public static ImmutableList<int> Range(int min, int max)
+        {
+            ImmutableList<int> l = new ImmutableList<int>();
+            for (int i = min; i < max; i++)
+            {
+                l.list.Add(i);
+            }
+            return l;
+        }
+    }
+
+  public class ChalicePrint {
+    public void Int(int x) {
+      System.Console.WriteLine(x);
+    }
+    public void Bool(bool x) {
+      System.Console.WriteLine(x);
+    }
+  }
+}
diff --git a/Chalice/src/Chalice.scala b/Chalice/src/Chalice.scala
new file mode 100644
index 00000000..439805d4
--- /dev/null
+++ b/Chalice/src/Chalice.scala
@@ -0,0 +1,115 @@
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+import java.io.BufferedReader
+import java.io.InputStreamReader
+import java.io.File
+import java.io.FileWriter
+
+object Chalice {
+  def main(args: Array[String]): unit = {
+    var boogiePath = "C:\\Boogie\\2\\Binaries\\Boogie.exe"
+    // parse command-line arguments
+    var inputName: String = null
+    var printProgram = false
+    var doTypecheck = true
+    var doTranslate = true
+    var checkLeaks = false
+    // level 0 or below: no defaults
+    // level 1: unfold predicates with receiver this in pre and postconditions
+    // level 2: unfold predicates and functions with receiver this in pre and postconditions
+    // level 3 or above: level 2 + autoMagic
+    var defaults = 0
+    var autoFold = false
+    var autoMagic = false
+    var boogieArgs = " ";
+    var gen = false;
+
+    for (a <- args) {
+      if (a == "-print") printProgram = true
+      else if (a == "-noTranslate") doTranslate = false
+      else if (a == "-noTypecheck") doTypecheck = false
+      else if (a == "-checkLeaks") checkLeaks = true
+      else if (a.startsWith("-boogie:")) boogiePath = a.substring(8)
+      else if (a == "-defaults") defaults = 3
+      else if (a.startsWith("-defaults:")) { try { defaults = Integer.parseInt(a.substring(10)); if(3<=defaults) { autoMagic = true; } } catch { case _ => CommandLineError("-defaults takes integer argument"); } }
+      else if (a == "-gen") { gen = true; doTranslate = false }
+      else if (a == "-autoFold") autoFold = true
+      else if (a == "-autoMagic") autoMagic = true
+      else if (a.startsWith("-") || a.startsWith("/")) boogieArgs += (a + " ") // arguments starting with "-" or "/" are sent to Boogie.exe
+      else if (inputName != null) { CommandLineError("multiple input filenames: " + inputName + " and " + a); return }
+      else { inputName = a }
+    }
+    // check the command-line arguments
+    if (inputName == null) { CommandLineError("missing input filename"); return } else {
+      val file = new File(inputName);
+      if(! file.exists()){
+        CommandLineError("input file " + file.getName() + " could not be found"); return
+      }
+    }
+    // parse program
+    val parser = new Parser();
+    parser.parseFile(inputName) match {
+      case e: parser.NoSuccess => Console.err.println("Error: " + e)
+      case parser.Success(prog, _) =>
+        if (printProgram) PrintProgram.P(prog)
+        if (doTypecheck) {
+          // typecheck program
+          Resolver.Resolve(prog) match {
+            case Resolver.Error(pos, msg) => 
+              Console.err.println("The program did not typecheck.\n");
+              Console.err.println(msg)
+            case Resolver.Errors(msgs) => 
+              Console.err.println("The program did not typecheck."); 
+              msgs foreach { msg => Console.err.println(msg) }
+            case Resolver.Success() =>
+              if(gen) {
+                val converter = new ChaliceToCSharp(); 
+                val cs = converter.convertProgram(prog);
+                writeFile("out.cs", cs);
+              }
+              if (doTranslate) {
+                // checking if Boogie.exe exists
+                val boogieFile = new File(boogiePath);
+                if(! boogieFile.exists() || ! boogieFile.isFile()) {
+                  CommandLineError("Boogie.exe not found at " + boogiePath); return
+                }
+                // translate program to BoogiePL
+                val translator = new Translator();
+                // set the translation options
+                TranslationOptions.checkLeaks = checkLeaks;
+                TranslationOptions.defaults = defaults;
+                TranslationOptions.autoFold = autoFold;
+                TranslationOptions.autoMagic = autoMagic;
+                val bplProg = translator.translateProgram(prog);
+                // write to out.bpl
+                val bplText = TranslatorPrelude.P + (bplProg map Boogie.Print).foldLeft(""){ (a, b) => a + b };
+                writeFile("out.bpl", bplText);
+                // run Boogie.exe on out.bpl
+                val boogie = Runtime.getRuntime().exec(boogiePath + " /errorTrace:0 " + boogieArgs + "out.bpl"); 
+                val input = new BufferedReader(new InputStreamReader(boogie.getInputStream()));
+                var line = input.readLine();
+                while(line!=null){
+                  println(line);
+                  line = input.readLine();
+                }
+              }
+            }
+        }
+    }
+  }
+
+  def writeFile(filename: String, text: String) {
+    val writer = new FileWriter(new File(filename));
+    writer.write(text);
+    writer.flush();
+    writer.close();
+  }
+
+  def CommandLineError(msg: String) = {
+    Console.err.println("Error: " + msg)
+    Console.err.println("syntax: chalice [-print] [-noTypecheck] [-noTranslate] [-boogie:path] [-defaults] [-autoFold] [-checkLeaks] inputFile")
+  }
+}
diff --git a/Chalice/src/ChaliceToCSharp.scala b/Chalice/src/ChaliceToCSharp.scala
new file mode 100644
index 00000000..75135e38
--- /dev/null
+++ b/Chalice/src/ChaliceToCSharp.scala
@@ -0,0 +1,211 @@
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+class ChaliceToCSharp {
+    
+  def convertProgram(classes: List[Class]): String = {
+    "using Chalice;" + nl + nl +
+    rep(classes map convertClass)
+  }
+  
+  def convertClass(cl: Class): String = if (cl.IsExternal) "" else {
+    "public class " + cl.id + " {" + nl +
+    indentMore { indent + "public " + cl.id + "() " + "{" + nl + indent + "}" } + nl + nl +
+    (if(0 < cl.Fields.length) {
+      indentMore { indent + "public " + cl.id + "(" + repsep(cl.Fields map { f => convertType(f.typ) + " " + f.Id }, ", ") + ") " + "{" + nl +
+      indentMore { rep(cl.Fields map { f => indent + "this." + f.Id + " = " + f.Id + ";" + nl}) } + 
+      indent + "}" } + nl + nl 
+    } else  "") +
+    indentMore { repsep(cl.members map convertMember, nl) } +
+    "}" + nl + nl
+  }
+  
+  def convertMember(member: Member): String = {
+    member match {
+      case Field(id, tp) =>
+        indent + "public " + convertType(tp) + " " + id + ";" + nl
+      case meth@Method(id, ins, outs, spec, body) =>
+        var csharpmain = if(id.equals("Start") && ins.length == 0 && outs.length == 0) {
+          indent + "public static void Main() { " + nl +
+          indentMore { 
+            indent + meth.Parent.id + " newObject = new " + meth.Parent.id + "();" + nl +
+            indent + "newObject.Start();" + nl
+          } + 
+          indent + "}" + nl + nl
+        } else { "" };
+        var params = repsep(ins map { variable => convertType(variable.t) + " " + variable.id }, ", ") + (if(ins.length > 0 && outs.length > 0) ", " else "") +
+        repsep(outs map { variable => "out " + convertType(variable.t) + " " + variable.id }, ", ");
+        csharpmain + 
+        indent + "public " + "void " + id + "(" + params + ") " + "{" + nl +
+        indentMore { 
+          rep(outs map { x => indent + x.id + " = " + defaultValue(x.t) + ";" + nl } ) + 
+          rep(body map convertStatement) 
+        } +
+        indent + "}" + nl + nl +
+        indent + "public delegate " + "void " + id + "_delegate" + "(" + params + ");"  + nl + nl +
+        indent + "public class " + "Token_" + id + " { " + nl + 
+        (indentMore {
+          indent + "public " + id + "_delegate " + "del;" + nl +
+          indent + "public " + "System.IAsyncResult " + "async;" + nl +
+          (rep(outs map { o: Variable => indent + "public " + convertType(o.t) + " " + o.id + ";" + nl  }))
+        }) +
+        indent + "}"  + nl
+      case Function(id, ins, out, spec, definition) => 
+        indent + "public " + convertType(out) + " " + id + "(" + 
+         repsep(ins map { variable => convertType(variable.t) + " " + variable.id }, ", ") + 
+         ") " + "{" + nl +
+         indentMore { indent + "return " + convertExpression(definition) + ";" + nl } +
+        indent +  "}" + nl
+      case MonitorInvariant(_) => indent + "// monitor invariant" + nl
+      case Predicate(_, _) => indent + "//predicate" + nl
+    }
+  }
+  
+  def convertStatement(statement: Statement): String = {
+    statement match {
+      case Assert(e) => indent + "// assert" + nl
+      case Assume(e) => indent + "assert " + convertExpression(e) + ";" // todo: what if e contains old, result, ...
+      case BlockStmt(ss) => indent + "{" + nl + (indentMore { rep(ss map convertStatement) }) + indent + "}" + nl
+      case IfStmt(guard, thn, els) => indent + "if (" + convertExpression(guard) + ")" + nl + convertStatement(thn) + 
+        (if(els.isDefined) (indent + "else" + nl + convertStatement(els.get)) else { "" }) + nl
+      case LocalVar(id, tp, const, ghost, rhs) =>
+        indent + convertType(tp) + " " + id + " = " +
+        (if(rhs.isDefined) convertExpression(rhs.get) else defaultValue(tp)) + 
+        ";" + nl
+      case FieldUpdate(MemberAccess(target, f), rhs) =>
+        indent + convertExpression(target) + "." + f + " = " + convertExpression(rhs) + ";" + nl
+      case Assign(VariableExpr(x), rhs) =>
+        indent + x + " = " + convertExpression(rhs) + ";" + nl
+      case WhileStmt(guard, _, _, body) =>
+        indent + "while (" + convertExpression(guard) + ")" + nl + convertStatement(body) + nl
+      case Call(lhs, target, id, args) =>
+        indent + convertExpression(target) + "." + id + "(" + 
+          repsep(args map convertExpression, ", ") + 
+          (if(args.length > 0 && lhs.length > 0) ", " else "") +
+          repsep(lhs map { l => "out " + convertExpression(l) }, ", ") +
+          ")" + ";" + nl
+      case Install(_, _, _) => indent + "// install" + nl
+      case Share(_, _, _) => indent + "// share" + nl
+      case Unshare(_) => indent + "// unshare" + nl
+      case Downgrade(_) => indent + "// downgrade" + nl
+      case Acquire(obj) => indent + "System.Threading.Monitor.Enter(" + convertExpression(obj) + ")" + ";" + nl
+      case Release(obj) => indent + "System.Threading.Monitor.Exit(" + convertExpression(obj) + ")" + ";" + nl
+      case Lock(obj, body, false) => indent + "lock(" + convertExpression(obj) + ") " + nl + convertStatement(body) + nl
+      case Free(_) => indent + "// free" + nl   
+      case Fold(_) => indent + "// fold" + nl  
+      case Unfold(_) => indent + "// unfold" + nl    
+      case RdAcquire(obj) => assert(false); ""
+      case RdRelease(obj) => assert(false); ""
+      case Lock(_, _, true) => assert(false); ""
+      case ca@CallAsync(declaresLocal, lhs, obj, id, args) => 
+        val tokenName = if(declaresLocal) lhs.id else { uniqueInt += 1; "tok_" + uniqueInt };
+        val call = convertExpression(obj) + "." + id;
+        val tokenClass = ca.m.Parent.id + ".Token_" + id;
+        val delegateName = ca.m.Parent.id + "." + id + "_delegate";
+        indent + tokenClass + " " + tokenName + " = new " + tokenClass + "();" + nl + 
+        indent + tokenName + "." + "del" + " = new " + delegateName + "(" + call + ");" + nl +
+        indent + tokenName + "." + "async" + " = " + tokenName + "." + "del" + "." + "BeginInvoke(" + repsep(args map convertExpression, ", ") +
+        (if(args.length > 0 && ca.m.outs.length > 0) ", " else "") + repsep(ca.m.outs map { o => "out " + tokenName + "." + o.id }, ", ") +
+        (if(args.length > 0 || ca.m.outs.length > 0) ", " else "") + "null, null" +
+        ");" + nl
+      case ja@JoinAsync(lhs, token) =>
+        indent + convertExpression(token) + "." + "del.EndInvoke(" + 
+        repsep(lhs map { x => "out " + x.id}, ", ") +
+        (if(lhs.length > 0) ", " else "") + convertExpression(token) + "." + "async" + ");" + nl
+    }
+  }
+  
+  def convertExpression(expression: RValue): String = {
+    expression match {
+      case IntLiteral(n) => "" + n
+      case BoolLiteral(b) => "" + b
+      case NullLiteral() => "null"
+      case th: ThisExpr => "this"
+      case VariableExpr(id) => id
+      case MemberAccess(target, f) => convertExpression(target) + "." + f
+      case newrhs@NewRhs(c, initialization) => 
+        if(initialization.length == 0) { "new " + c + "()" } else {
+          val init = repsep(newrhs.typ.Fields map { f => (initialization.find { i => i.f == f}) match {
+              case None => defaultValue(f.typ)
+              case Some(init) => convertExpression(init.e);
+            }
+          }, ", ");
+          "new " + c + "(" + init + ")";
+        }
+      case At(s, i) => convertExpression(s) + ".At(" + convertExpression(i) + ")" 
+      case Append(s1, s2) => convertExpression(s1) + ".Append(" + convertExpression(s2) + ")" 
+      case Take(s, i) => convertExpression(s) + ".Take(" + convertExpression(i) + ")"
+      case Drop(s, i) => convertExpression(s) + ".Drop(" + convertExpression(i) + ")" 
+      case bin: BinaryExpr => "(" + convertExpression(bin.E0) + " " + bin.OpName + " " + convertExpression(bin.E1) + ")"// todo: <==> and ==>
+      case Unfolding(p, e) => convertExpression(e)
+      case FunctionApplication(target, id, args) => convertExpression(target) + "." + id + "(" + repsep(args map convertExpression, ", ") + ")"
+      case Not(e) => "(! " + convertExpression(e) + ")"
+      case EmptySeq(tp) => "new Chalice.ImmutableList<" + convertType(tp) + ">()"
+      case es@ExplicitSeq(elems) => 
+        val elemType = new Type(es.typ.asInstanceOf[SeqClass].parameter);
+        "new Chalice.ImmutableList<" + convertType(elemType) + ">(" +
+          "new " + convertType(elemType) + "[] {" + repsep(elems map convertExpression, ", ") + "}" + 
+        ")"
+      case Range(min, max) => "Chalice.ImmutableList.Range(" + convertExpression(min) + ", " + convertExpression(max) + ")"
+      case Length(s) => convertExpression(s) + ".Length"
+      case IfThenElse(c, thn, els) => "(" + convertExpression(c) + " ? " + convertExpression(thn) + " : " + convertExpression(els) + ")" 
+    }
+  }
+  
+  def convertType(tp: Type): String = {
+    tp.typ match {
+      case t: TokenClass => t.c.FullName + ".Token_" + t.m
+      case s: SeqClass => "Chalice.ImmutableList<" + convertType(new Type(s.parameter)) + ">"
+      case IntClass => "int"
+      case BoolClass => "bool"
+      case NullClass => "object"
+      case Class(id, _, _, _) => id
+    }
+  }
+  
+  def defaultValue(tp: Type) = {
+     tp.typ match {
+      case t: TokenClass => "null"
+      case s: SeqClass => "new Chalice.ImmutableList<" + convertType(new Type(s.parameter)) + ">()"
+      case IntClass => "0"
+      case BoolClass => "false"
+      case NullClass => "null"
+      case Class(id, _, _, _) => "null"
+    }
+  }
+  
+  // utility methods below
+  
+  var uniqueInt: int = 0;
+  val nl = System.getProperty("line.separator");
+  var indentLevel = 0
+  
+  def rep(strings: List[String]): String = {
+    strings.foldLeft("")({ (a, b) => a + b })
+  }
+  
+  def repsep(strings: List[String], separator: String): String = {
+    if(strings.length == 0) {
+      ""
+    } else {
+      strings.reduceLeft({ (a, b) => a + separator + b })
+    }
+  }
+  
+  def indent: String = {
+    def doIndent(i: int): String = {
+      if(i==0) { "" } else { "  " + doIndent(i-1) }
+    }
+    doIndent(indentLevel);
+  }
+
+  def indentMore(what: => String) = {
+    val prev = indentLevel
+    indentLevel = indentLevel + 1
+    val result = what
+    indentLevel = prev
+    result
+  }
+}
diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala
new file mode 100644
index 00000000..5063cc92
--- /dev/null
+++ b/Chalice/src/Parser.scala
@@ -0,0 +1,409 @@
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+import scala.util.parsing.combinator.syntactical.StandardTokenParsers
+import scala.util.parsing.input.PagedSeqReader
+import scala.collection.immutable.PagedSeq
+import scala.util.parsing.input.Position
+import scala.util.parsing.input.Positional
+import scala.util.parsing.input.NoPosition
+
+class Parser extends StandardTokenParsers {
+
+  def parseFile(path: String): this.ParseResult[List[Class]] = {
+    val tokens = new lexical.Scanner(new PagedSeqReader(PagedSeq fromFile path));
+    phrase(programUnit)(tokens)
+  }
+ 
+  case class PositionedString(v: String) extends Positional
+
+  lexical.reserved += ("class", "ghost", "var", "const", "method", "assert", "assume", "new", "this", "reorder",
+                       "between", "and", "above", "below", "share", "unshare", "acquire", "release", "downgrade",
+                       "lock", "fork", "join", "rd", "acc", "holds", "old", "assigned",
+                       "call", "if", "else", "while", "invariant", "lockchange",
+                       "returns", "requires", "ensures", "int", "bool", "false", "true", "null", "maxlock", "lockbottom",
+                       "module", "external",
+                       "predicate", "function", "free", "ite", "fold", "unfold", "unfolding", "in", "forall", "exists", 
+                       "seq", "nil", "result", "eval", "token")
+  // todo: can we remove "nil"?
+  lexical.delimiters += ("(", ")", "{", "}",
+                         "<==>", "==>", "&&", "||",
+                         "==", "!=", "<", "<=", ">=", ">", "<<",
+                         "+", "-", "*", "/", "%", "!", ".", "..",
+                         ";", ":", ":=", ",", "?", "|", "@", "[", "]", "++")
+
+  def programUnit = classDecl*
+
+  // class and members
+
+  def classDecl =
+        positioned(("external" ?) ~ ("class" ~> ident) ~ opt("module" ~> ident) ~ "{" ~ (memberDecl*) <~ "}" ^^ {
+          case ext ~ id ~ module ~ _ ~ members =>
+            val cl = Class(id, Nil, module.getOrElse("default"), members)
+            ext match { case None => case Some(t) => cl.IsExternal = true }
+            cl
+        })
+  def memberDecl = positioned(fieldDecl | invariantDecl | methodDecl | predicateDecl | functionDecl)
+
+  def fieldDecl =
+        ( "var" ~> idType <~ Semi ^^ { case (id,t) => Field(id,t) }
+        | "ghost" ~> "var" ~> idType <~ Semi ^^ { case (id,t) => new Field(id,t){override val IsGhost = true} }
+        )
+  def Ident = 
+    positioned(ident ^^ PositionedString)
+  def idType =
+    idTypeOpt ^^ {
+      case (id, None) => (id, Type("int", Nil))
+      case (id, Some(t)) => (id, t) }
+  def idTypeOpt =
+    ident ~ (":" ~> typeDecl ?) ^^ { case id ~ optT => (id, optT) }
+  def typeDecl: Parser[Type] =
+      positioned(("int" | "bool" | ident | "seq") ~ opt("<" ~> repsep(typeDecl, ",") <~ ">") ^^ { case t ~ parameters => Type(t, parameters.getOrElse(Nil)) }
+      | ("token" ~ "<") ~> (typeDecl <~ ".") ~ ident <~ ">" ^^ { case c ~ m => TokenType(c, m) }
+      )
+  def Semi = ";" ?
+
+  def invariantDecl = positioned("invariant" ~> expression <~ Semi ^^ MonitorInvariant)
+
+  def methodDecl =
+        "method" ~> ident ~ formalParameters(true) ~ ("returns" ~> formalParameters(false) ?) ~
+        (methodSpec*) ~ blockStatement ^^ {
+          case id ~ ins ~ outs ~ spec ~ body =>
+            currentLocalVariables = Set[String]()
+            outs match {
+              case None => Method(id, ins, Nil, spec, body)
+              case Some(outs) => Method(id, ins, outs, spec, body) }}
+  def predicateDecl: Parser[Predicate] = 
+    ("predicate" ~> ident) ~ ("{" ~> expression <~ "}") ^^ { case id ~ definition => Predicate(id, definition) }
+  def functionDecl = 
+    ("function" ~> ident) ~ formalParameters(true) ~ (":" ~> typeDecl) ~ (methodSpec*) ~ ("{" ~> expression <~ "}") ^^ { case id ~ ins ~ out ~ specs ~ body => Function(id, ins, out, specs, body) }
+  def formalParameters(immutable: boolean) =
+    "(" ~> (formalList(immutable) ?) <~ ")" ^^ {
+      case None => Nil
+      case Some(ids) => ids }
+  def formalList(immutable: boolean) = {
+    def MVar(id: String, t: Type) = {
+      currentLocalVariables = currentLocalVariables + id
+      if (immutable) new ImmutableVariable(id,t) else new Variable(id,t)
+    }
+    ( idType ^^ { case (id,t) => MVar(id,t)} ) ~
+    (("," ~> idType ^^ { case (id,t) => MVar(id,t)} ) *) ^^ {
+      case e ~ ee => e::ee }
+  }
+  def methodSpec =
+    positioned( "requires" ~> expression <~ Semi ^^ Precondition
+    | "ensures" ~> expression <~ Semi ^^ Postcondition
+    | "lockchange" ~> expressionList <~ Semi ^^ LockChange
+    )
+  def blockStatement: Parser[List[Statement]] = {
+    val prev = currentLocalVariables
+    "{" ~> (statement*) <~ "}" ^^ {
+      case x => currentLocalVariables = prev; x }
+  }
+
+  // statements
+
+  def statement =
+    positioned( "assert" ~> expression <~ Semi ^^ Assert
+    | "assume" ~> expression <~ Semi ^^ Assume
+    | blockStatement ^^ BlockStmt
+    | "var" ~> localVarStmt(false, false)
+    | "const" ~> localVarStmt(true, false)
+    | "ghost" ~> ( "const" ~> localVarStmt(true, true) | "var" ~> localVarStmt(false, true))
+    | "call" ~> callStmt
+    | "if" ~> ifStmtThen
+    | "while" ~> "(" ~> expression ~ ")" ~ loopSpec ~ blockStatement ^^ {
+        case guard ~ _ ~ lSpec ~ body =>
+          lSpec match { case (invs,lkch) => WhileStmt(guard, invs, lkch, BlockStmt(body)) }}
+    | "reorder" ~> expression ~ (installBounds ?) <~ Semi ^^ {
+        case obj ~ None => Install(obj, List(), List())
+        case obj ~ Some(bounds) => Install(obj, bounds._1, bounds._2) }
+    | "share" ~> expression ~ (installBounds ?) <~ Semi ^^ {
+        case obj ~ None => Share(obj, List(), List())
+        case obj ~ Some(bounds) => Share(obj, bounds._1, bounds._2) }
+    | "unshare" ~> expression <~ Semi ^^ Unshare
+    | "acquire" ~> expression <~ Semi ^^ Acquire
+    | "release" ~> expression <~ Semi ^^ Release
+    | "lock" ~> "(" ~> expression ~ ")" ~ blockStatement ^^ {
+        case e ~ _ ~ b => Lock(e, BlockStmt(b), false) }
+    | "rd" ~>
+        ( "lock" ~> "(" ~> expression ~ ")" ~ blockStatement ^^ {
+            case e ~ _ ~ b => Lock(e, BlockStmt(b), true) }
+        | "acquire" ~> expression <~ Semi ^^ RdAcquire
+        | "release" ~> expression <~ Semi ^^ RdRelease
+        )
+    | "downgrade" ~> expression <~ Semi ^^ Downgrade
+    | "free" ~> expression <~ Semi ^^ Free
+    | Ident ~ ":=" ~ Rhs <~ Semi ^^ {
+        case lhs ~ _ ~ rhs =>
+          if (currentLocalVariables contains lhs.v) {
+            val varExpr = VariableExpr(lhs.v); varExpr.pos = lhs.pos;
+            Assign(varExpr, rhs)
+          } else {
+            val implicitThis = ImplicitThisExpr();
+            val select = MemberAccess(implicitThis, lhs.v);
+            implicitThis.pos = lhs.pos;
+            select.pos = lhs.pos;
+            FieldUpdate(select, rhs)
+          }}
+    | selectExprFerSure ~ ":=" ~ Rhs <~ Semi ^^ {
+        case lhs ~ _ ~ rhs => FieldUpdate(lhs, rhs) }
+    | ("fold" ~> expression <~ Semi) ^? { 
+        case pred: MemberAccess => Fold(Access(pred, None))
+        case perm: PermissionExpr => Fold(perm) 
+      }
+    | ("unfold" ~> expression <~ Semi) ^? { 
+        case pred: MemberAccess => Unfold(Access(pred, None))
+        case perm: PermissionExpr => Unfold(perm) 
+      }
+    | ("fork") ~> callSignature ^? ({
+        case None ~ target ~ args =>
+          val (receiver, name) = target match { 
+            case VariableExpr(id) => (new ImplicitThisExpr, id)
+            case MemberAccess(obj, id) => (obj, id) 
+          }
+          CallAsync(false, null, receiver, name, ExtractList(args))
+        case Some(List(tok)) ~ target ~ args => 
+          val (receiver, name) = target match { 
+            case VariableExpr(id) => (new ImplicitThisExpr, id)
+            case MemberAccess(obj, id) => (obj, id) 
+          }
+          if (currentLocalVariables contains tok.id) {
+            CallAsync(false, tok, receiver, name, ExtractList(args))
+          } else {
+            currentLocalVariables = currentLocalVariables + tok.id;
+            CallAsync(true, tok, receiver, name, ExtractList(args))
+          }
+        }, t => "fork statement cannot take more than 1 left-hand side")
+    | (("join") ~> ( identList <~ ":=" ?)) ~ expression <~ Semi ^^ 
+        { case results ~ token => JoinAsync(ExtractList(results), token) }
+    )
+  def localVarStmt(const: boolean, ghost: boolean) =
+      idTypeOpt ~ (":=" ~> Rhs ?) <~ Semi ^^ {
+        case (id,optT) ~ rhs =>
+          currentLocalVariables = currentLocalVariables + id
+          LocalVar(id,
+                   optT match {
+                     case Some(t) => t
+                     case None =>
+                       // do a cheap (and hokey) type inference of the RHS
+                       rhs match {
+                         case Some(NewRhs(tid, _)) => Type(tid, Nil)
+                         case Some(BoolLiteral(b)) => Type("bool", Nil)
+                         case _ => Type("int", Nil)
+                       }
+                   },
+                   const, ghost, rhs)
+      }
+  def ifStmtThen: Parser[IfStmt] =
+    "(" ~> expression ~ ")" ~ blockStatement ~ ("else" ~> ifStmtElse ?) ^^ {
+      case guard ~ _ ~ thenClause ~ elseClause => IfStmt(guard, BlockStmt(thenClause), elseClause) }
+  def ifStmtElse =
+    ( "if" ~> ifStmtThen
+    | statement
+    )
+  def loopSpec: Parser[(List[Expression], List[Expression])] =
+    (loopSpecX *) ^^ {
+      case pp => (pp :\ (List[Expression](), List[Expression]())) ( (p,list) =>
+        (p,list) match {
+          case ((null,ee),(e0,e1)) => (e0, ee ++ e1)
+          case ((e,ee),(e0,e1)) => (e :: e0, ee ++ e1)
+        })
+    }
+  def loopSpecX =
+    ( "invariant" ~> expression <~ Semi ^^ { case e => (e,Nil) }
+    | "lockchange" ~> expressionList <~ Semi ^^ { case ee => (null,ee) }
+    )
+  def callStmt =
+    callSignature ^? ({
+      case outs ~ VariableExpr(id) ~ args => Call(ExtractList(outs), new ImplicitThisExpr, id, ExtractList(args))
+      case outs ~ MemberAccess(obj,id) ~ args => Call(ExtractList(outs), obj, id, ExtractList(args))
+    }, t => "bad call statement")
+  def callSignature =
+    (identList <~ ":=" ?) ~ callTarget ~ (expressionList?) <~ ")" <~ Semi
+  def callTarget =  // returns a VariableExpr or a FieldSelect
+      ( ident <~ "(" ^^ VariableExpr
+      | selectExprFerSure <~ "("
+      )
+  def ExtractList[T](a: Option[List[T]]): List[T] = a match {
+    case None => Nil
+    case Some(list) => list }
+  def identList =
+    ( Ident ^^ { case t => val v = VariableExpr(t.v); v.pos = t.pos; v }) ~
+    (("," ~> Ident ^^ { case t => val v = VariableExpr(t.v); v.pos = t.pos; v }) *) ^^ { case e ~ ee => e::ee }
+  def Rhs : Parser[RValue] =
+    positioned( "new" ~> ident ~ opt("{" ~> repsep(FieldInit, ",") <~ "}") ^^ { case id ~ None => NewRhs(id, Nil)
+                                                                                case id ~ Some(inits) => NewRhs(id, inits)
+                                                                              }
+    | expression
+    )
+  def FieldInit: Parser[Init] =
+    positioned( (ident <~ ":=") ~ expression ^^ { case id ~ e => Init(id, e) } )
+  def installBounds: Parser[(List[Expression], List[Expression])] =
+    ( "between" ~> expressionList ~ "and" ~ expressionList ^^ { case l ~ _ ~ u => (l,u) }
+    | "below" ~> expressionList ^^ { (Nil,_) }
+    | "above" ~> expressionList ^^ { (_,Nil) }
+    )
+  
+  // expressions
+
+  def expression = positioned(iteExpr)
+
+  def iteExpr: Parser[Expression] =
+        positioned(iffExpr ~ (("?" ~> iteExpr) ~ (":" ~> iteExpr) ?) ^^ {
+          case e ~ None => e
+          case e0 ~ Some(e1 ~ e2) => IfThenElse(e0,e1,e2) })
+  def iffExpr: Parser[Expression] =
+        positioned(implExpr ~ ("<==>" ~> iffExpr ?) ^^ {
+          case e ~ None => e
+          case e0 ~ Some(e1) => Iff(e0,e1) })
+  def implExpr: Parser[Expression] =
+        positioned(logicalExpr ~ ("==>" ~> implExpr ?) ^^ {
+          case e ~ None => e
+          case e0 ~ Some(e1) => Implies(e0,e1) })
+  def logicalExpr =
+        positioned(cmpExpr ~ (( ("&&" ~ cmpExpr +) | ("||" ~ cmpExpr +) )?) ^^ {
+          case e ~ None => e
+          case e0 ~ Some(rest) => (rest foldLeft e0) {
+            case (a, "&&" ~ b) => And(a,b)
+            case (a, "||" ~ b) => Or(a,b) }})
+  def cmpExpr = 
+        positioned(seqExpr ~ ((CompareOp ~ seqExpr)?) ^^ {
+          case e ~ None => e
+          case e0 ~ Some("==" ~ e1) => Eq(e0,e1)
+          case e0 ~ Some("!=" ~ e1) => Neq(e0,e1)
+          case e0 ~ Some("<" ~ e1) => Less(e0,e1)
+          case e0 ~ Some("<=" ~ e1) => AtMost(e0,e1)
+          case e0 ~ Some(">=" ~ e1) => AtLeast(e0,e1)
+          case e0 ~ Some(">" ~ e1) => Greater(e0,e1)
+          case e0 ~ Some("<<" ~ e1) => LockBelow(e0,e1)
+        })
+  def CompareOp = "==" | "!=" | "<" | "<=" | ">=" | ">" | "<<"
+  def seqExpr =
+    positioned(addExpr ~ (seqAccess *) ^^ { case e ~ as => as.foldLeft(e: Expression)({ (t, a) => val result = a(t); result.pos = t.pos; result }) })
+
+  def seqAccess : Parser[(Expression => SeqAccess)] =
+   ( ("[" ~> expression) <~ "]" ^^ { case e1 => { e0: Expression => At(e0, e1) }} 
+    | "[" ~> expression <~ (".." ~ "]") ^^ { case e1 => { e0: Expression => Drop(e0, e1)}} 
+    | ("[" ~ "..") ~> expression <~ "]" ^^ { case e1 => { e0: Expression => Take(e0, e1)}}
+    | "++" ~> expression ^^ { case e1 => { e0: Expression => Append(e0, e1) }}
+    | ("[" ~> expression  <~ "..") ~ (expression <~ "]") ^^ { case e1 ~ e2 => {e0: Expression => val tak = Take(e0, e2); tak.pos = e0.pos; Drop(tak, e1)} })
+
+  def addExpr =
+        positioned(multExpr ~ (AddOp ~ multExpr *) ^^ {
+          case e0 ~ rest => (rest foldLeft e0) {
+            case (a, "+" ~ b) => Plus(a,b)
+            case (a, "-" ~ b) => Minus(a,b) }})
+  def AddOp = "+" | "-"
+  def multExpr: Parser[Expression] =
+        unaryExpr ~ (MulOp ~ unaryExpr *) ^^ {
+          case e0 ~ rest => (rest foldLeft e0) {
+            case (a, "*" ~ b) => Times(a,b)
+            case (a, "/" ~ b) => Div(a,b)
+            case (a, "%" ~ b) => Mod(a,b) }}
+  def MulOp = "*" | "/" | "%"
+  def unaryExpr: Parser[Expression] =
+        ( "!" ~> unaryExpr ^^ Not
+        | "-" ~> unaryExpr ^^ { Minus(IntLiteral(0),_) }
+        | functionApplication
+        | selectExpr
+        )
+  def selectExpr: Parser[Expression] =
+      atom ~ ("." ~> identOrSpecial *) ^^ {
+        case e ~ fields => (fields foldLeft e) { case (e, f) => val result = MemberAccess(e, f); result.pos = e.pos; result }
+  }
+  def selectExprFerSure: Parser[MemberAccess] =
+    positioned(atom ~ "." ~ identOrSpecial ~ ("." ~> ident *) ^^ {
+      case e ~ _ ~ field ~ moreFields => (moreFields foldLeft MemberAccess(e,field)) { (target, f) => val result = MemberAccess(target, f); result.pos = target.pos; result }})
+  def functionApplication: Parser[Expression] =
+    atom ~ rep("." ~> identOrSpecial ~ opt("(" ~> repsep(expression, ",") <~ ")")) ^^ {
+      case target ~ members =>  
+      members.foldLeft(target)({ case (e, name ~ args) => val result = if(! args.isDefined) MemberAccess(e, name) else FunctionApplication(e, name, args.get); result.pos = e.pos; result })
+    }
+  
+  def identOrSpecial: Parser[String] =
+    (  ident ^^ { case s => s }
+    | "acquire" ^^^ "acquire"
+    | "release" ^^^ "release"
+    | "fork" ^^^ "fork"
+    | "*" ^^^ "*")
+
+  var currentLocalVariables = Set[String]()
+
+  def expressionList =
+    expression ~ ("," ~> expression *) ^^ { case e ~ ee => e::ee }
+  
+  def atom : Parser[Expression] =
+      positioned( numericLit ^^ { case n => IntLiteral(n.toInt) }
+      | "false" ^^^ BoolLiteral(false)
+      | "true" ^^^ BoolLiteral(true)
+      | "null" ^^^ NullLiteral()
+      | "maxlock" ^^^ MaxLockLiteral()
+      | "lockbottom" ^^^ LockBottomLiteral()
+      | "this" ^^^ ExplicitThisExpr()
+      | ("[" ~> expression) ~ (":" ~> expression <~ "]") ^^ { case from ~ to => Range(from, to) }
+      | "(" ~> expression <~ ")"
+      | ("eval" ~ "(") ~> (evalstate <~ ",") ~ (expression <~ ")") ^^ { case h ~ e => Eval(h, e) }
+      | ("ite(" ~> expression <~ ",") ~ (expression <~ ",") ~ (expression <~ ")") ^^ { case con ~ then ~ els => IfThenElse (con, then, els) }
+      | "rd" ~>
+        ( "holds" ~> "(" ~> expression <~ ")" ^^ RdHolds
+        | "(" ~>
+          ( (Ident ^^ (e => { val result = MemberAccess(ImplicitThisExpr(),e.v); result.pos = e.pos; result})) ~ rdPermArg <~ ")"
+          | selectExprFerSure                                   ~ rdPermArg <~ ")"
+          ) ^^ { case MemberAccess(obj, "*") ~ p => RdAccessAll(obj, p) case e ~ p => RdAccess(e,p) }
+        )
+      | "acc" ~> "(" ~>
+        ( (Ident ^^ (e => { val result = MemberAccess(ImplicitThisExpr(),e.v); result.pos = e.pos; result} )) ~ ("," ~> expression ?) <~ ")"
+        | selectExprFerSure                                   ~ ("," ~> expression ?) <~ ")"
+        ) ^^ { case MemberAccess(obj, "*") ~ perm => AccessAll(obj, perm) case e ~ perm => Access(e, perm) }
+      | "holds" ~> "(" ~> expression <~ ")" ^^ Holds
+      | "assigned" ~> "(" ~> ident <~ ")" ^^ Assigned
+      | "old" ~> "(" ~> expression <~ ")" ^^ Old
+      | positioned(Ident) ~ opt("(" ~> repsep(expression, ",") <~ ")") ^^ 
+         { case id ~ args => val result = 
+                       if(args.isDefined){
+                         val implicitThis = ImplicitThisExpr(); implicitThis.pos = id.pos;
+                         FunctionApplication(implicitThis, id.v, args.get)
+                       } else {
+                         if (currentLocalVariables contains id.v) 
+                           VariableExpr(id.v) 
+                         else {
+                           val implicitThis = ImplicitThisExpr(); implicitThis.pos = id.pos; MemberAccess(implicitThis, id.v)
+                         }
+                       }; result.pos = id.pos; result }
+      | ("unfolding" ~> expression <~ "in") ~ expression ^? { 
+          case (pred: MemberAccess) ~ e => val acc = Access(pred, None); acc.pos = pred.pos; Unfolding(acc, e)
+          case (perm: PermissionExpr) ~ e => Unfolding(perm, e) 
+        }
+      | ("nil" ~> "<") ~> (typeDecl <~ ">") ^^ EmptySeq
+      | ("[" ~> repsep(expression, ",") <~ "]") ^^ { case es => ExplicitSeq(es) }
+      | "|" ~> expression <~ "|" ^^ Length
+      | forall
+      | "result" ^^^ Result()
+      )
+  def forall: Parser[Forall] = 
+    (("forall" ~ "{") ~> repsep(ident, ",") <~ "in") into { is => (expression <~ ";") ~ (exprWithLocals(is) <~ "}") ^^ 
+      { case seq ~ e => val result = Forall(is, seq, e); currentLocalVariables = currentLocalVariables -- is; result } }
+  def exprWithLocals(i: List[String]) : Parser[Expression] = {
+    val savedCurrentLocals = currentLocalVariables;
+    currentLocalVariables = currentLocalVariables ++ i;
+    val result = ((expression) ^^ { case e => e});
+    result
+  }
+
+  def evalstate: Parser[EvalState] = {
+    functionApplication ~ opt(callTarget ~ (repsep(expression, ",") <~ ")")) ^? 
+                           { case MemberAccess(e, "acquire") ~ None => AcquireState(e)
+                             case MemberAccess(e, "release") ~ None => ReleaseState(e)
+                             case MemberAccess(e, "fork") ~ Some((MemberAccess(obj, id) ~ args)) => CallState(e, obj, id, args)
+                           }
+  }
+
+  def rdPermArg : Parser[Option[Option[Expression]]] =
+      (("," ~> ( "*" ^^^ None
+               | expression ^^ { case e => Some(e) }
+               )) ?
+      )
+}
diff --git a/Chalice/src/Prelude.scala b/Chalice/src/Prelude.scala
new file mode 100644
index 00000000..876a5abe
--- /dev/null
+++ b/Chalice/src/Prelude.scala
@@ -0,0 +1,251 @@
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+object TranslatorPrelude { 
+
+  val P =
+"""// Copyright (c) 2008, Microsoft
+type Field a;
+type HeapType = <a>[ref,Field a]a;
+type MaskType = <a>[ref,Field a][PermissionComponent]int;
+type ref;
+const null: ref;
+
+var Heap: HeapType;
+
+type PermissionComponent;
+const unique perm$R: PermissionComponent;
+const unique perm$N: PermissionComponent;
+const Permission$MinusInfinity: int;
+axiom Permission$MinusInfinity < -10000;
+const Permission$PlusInfinity: int;
+axiom 10000 < Permission$PlusInfinity;
+var Mask: MaskType where IsGoodMask(Mask);
+const Permission$Zero: [PermissionComponent]int;
+axiom Permission$Zero[perm$R] == 0 && Permission$Zero[perm$N] == 0;
+const Permission$Full: [PermissionComponent]int;
+axiom Permission$Full[perm$R] == 100 && Permission$Full[perm$N] == 0;
+const ZeroMask: MaskType;
+axiom (forall<T> o: ref, f: Field T, pc: PermissionComponent :: ZeroMask[o,f][pc] == 0);
+axiom IsGoodMask(ZeroMask);
+function {:expand false} CanRead<T>(m: MaskType, obj: ref, f: Field T) returns (bool)
+{
+  0 < m[obj,f][perm$R] || 0 < m[obj,f][perm$N]
+}
+function {:expand false} CanWrite<T>(m: MaskType, obj: ref, f: Field T) returns (bool)
+{
+  m[obj,f][perm$R] == 100 && m[obj,f][perm$N] == 0
+}
+function {:expand true} IsGoodMask(m: MaskType) returns (bool)
+{
+  (forall<T> o: ref, f: Field T ::
+      0 <= m[o,f][perm$R] && 
+      (NonPredicateField(f) ==> 
+        (m[o,f][perm$R]<=100 &&
+        (0 < m[o,f][perm$N] ==> m[o,f][perm$R] < 100))) &&
+      (m[o,f][perm$N] < 0 ==> 0 < m[o,f][perm$R]))
+}
+
+function IsGoodState<T>(T) returns (bool);
+function combine<T,U>(T, U) returns (T);
+const nostate: HeapType;
+
+axiom (forall<T,U> a: T, b: U :: {IsGoodState(combine(a, b))} IsGoodState(combine(a, b)) <==> IsGoodState(a) && IsGoodState(b));
+axiom IsGoodState(nostate);
+
+type ModuleName;
+const CurrentModule: ModuleName;
+type TypeName;
+function dtype(ref) returns (TypeName);
+const CanAssumeFunctionDefs: bool;
+
+type Mu;
+const unique mu: Field Mu;
+axiom NonPredicateField(mu);
+function MuBelow(Mu, Mu) returns (bool);  // strict partial order
+axiom (forall m: Mu, n: Mu ::
+  { MuBelow(m,n), MuBelow(n,m) }
+  !(MuBelow(m,n) && MuBelow(n,m)));
+axiom (forall m: Mu, n: Mu, o: Mu ::
+  { MuBelow(m,n), MuBelow(n,o) }
+  MuBelow(m,n) && MuBelow(n,o) ==> MuBelow(m,o));
+const $LockBottom: Mu;
+axiom (forall m, n: Mu :: MuBelow(m, n) ==> n != $LockBottom);
+
+const unique held: Field int;
+function Acquire$Heap(int) returns (HeapType);
+function Acquire$Mask(int) returns (MaskType);
+axiom NonPredicateField(held);
+
+function LastSeen$Heap(Mu, int) returns (HeapType);
+function LastSeen$Mask(Mu, int) returns (MaskType);
+
+const unique rdheld: Field bool;
+axiom NonPredicateField(rdheld);
+function wf(h: HeapType, m: MaskType) returns (bool);
+
+function IsGoodInhaleState(ih: HeapType, h: HeapType,
+                           m: MaskType) returns (bool)
+{
+  (forall<T> o: ref, f: Field T :: { ih[o, f] }  CanRead(m, o, f) ==> ih[o, f] == h[o, f]) &&
+  (forall o: ref :: { ih[o, held] }  (0<ih[o, held]) == (0<h[o, held])) &&
+  (forall o: ref :: { ih[o, rdheld] }  ih[o, rdheld] == h[o, rdheld]) &&
+  (forall o: ref :: { h[o, held] }  (0<h[o, held]) ==> ih[o, mu] == h[o, mu])
+}
+
+function ite<T>(bool, T, T) returns (T);
+axiom (forall<T> con: bool, a: T, b: T :: {ite(con, a, b)} con ==> ite(con, a, b) == a);
+axiom (forall<T> con: bool, a: T, b: T :: {ite(con, a, b)} ! con ==> ite(con, a, b) == b);
+
+type Seq T;
+
+function Seq#Length<T>(Seq T) returns (int);
+axiom (forall<T> s: Seq T :: { Seq#Length(s) } 0 <= Seq#Length(s));
+
+function Seq#Empty<T>() returns (Seq T);
+axiom (forall<T> :: Seq#Length(Seq#Empty(): Seq T) == 0);
+axiom (forall<T> s: Seq T :: { Seq#Length(s) } Seq#Length(s) == 0 ==> s == Seq#Empty());
+
+function Seq#Singleton<T>(T) returns (Seq T);
+axiom (forall<T> t: T :: { Seq#Length(Seq#Singleton(t)) } Seq#Length(Seq#Singleton(t)) == 1);
+
+function Seq#Build<T>(s: Seq T, index: int, val: T, newLength: int) returns (Seq T);
+axiom (forall<T> s: Seq T, i: int, v: T, len: int :: { Seq#Length(Seq#Build(s,i,v,len)) }
+  Seq#Length(Seq#Build(s,i,v,len)) == len);
+
+function Seq#Append<T>(Seq T, Seq T) returns (Seq T);
+axiom (forall<T> s0: Seq T, s1: Seq T :: { Seq#Length(Seq#Append(s0,s1)) }
+  Seq#Length(Seq#Append(s0,s1)) == Seq#Length(s0) + Seq#Length(s1));
+
+function Seq#Index<T>(Seq T, int) returns (T);
+axiom (forall<T> t: T :: { Seq#Index(Seq#Singleton(t), 0) } Seq#Index(Seq#Singleton(t), 0) == t);
+axiom (forall<T> s0: Seq T, s1: Seq T, n: int :: { Seq#Index(Seq#Append(s0,s1), n) }
+  (n < Seq#Length(s0) ==> Seq#Index(Seq#Append(s0,s1), n) == Seq#Index(s0, n)) &&
+  (Seq#Length(s0) <= n ==> Seq#Index(Seq#Append(s0,s1), n) == Seq#Index(s1, n - Seq#Length(s0))));
+axiom (forall<T> s: Seq T, i: int, v: T, len: int, n: int :: { Seq#Index(Seq#Build(s,i,v,len),n) }
+  (i == n ==> Seq#Index(Seq#Build(s,i,v,len),n) == v) &&
+  (i != n ==> Seq#Index(Seq#Build(s,i,v,len),n) == Seq#Index(s,n)));
+
+function Seq#Contains<T>(Seq T, T) returns (bool);
+axiom (forall<T> s: Seq T, x: T :: { Seq#Contains(s,x) }
+  Seq#Contains(s,x) <==>
+    (exists i: int :: { Seq#Index(s,i) } 0 <= i && i < Seq#Length(s) && Seq#Index(s,i) == x));
+axiom (forall x: ref ::
+  { Seq#Contains(Seq#Empty(), x) }
+  !Seq#Contains(Seq#Empty(), x));
+axiom (forall<T> s0: Seq T, s1: Seq T, x: T ::
+  { Seq#Contains(Seq#Append(s0, s1), x) }
+  Seq#Contains(Seq#Append(s0, s1), x) <==>
+    Seq#Contains(s0, x) || Seq#Contains(s1, x));
+axiom (forall<T> s: Seq T, i: int, v: T, len: int, x: T ::
+  { Seq#Contains(Seq#Build(s, i, v, len), x) }
+  Seq#Contains(Seq#Build(s, i, v, len), x) <==>
+    x == v || Seq#Contains(s, x));
+axiom (forall<T> s: Seq T, n: int, x: T ::
+  { Seq#Contains(Seq#Take(s, n), x) }
+  Seq#Contains(Seq#Take(s, n), x) <==>
+    (exists i: int :: { Seq#Index(s, i) }
+      0 <= i && i < n && n <= Seq#Length(s) && Seq#Index(s, i) == x));
+axiom (forall<T> s: Seq T, n: int, x: T ::
+  { Seq#Contains(Seq#Drop(s, n), x) }
+  Seq#Contains(Seq#Drop(s, n), x) <==>
+    (exists i: int :: { Seq#Index(s, i) }
+      0 <= n && n <= i && i < Seq#Length(s) && Seq#Index(s, i) == x));
+
+function Seq#Equal<T>(Seq T, Seq T) returns (bool);
+axiom (forall<T> s0: Seq T, s1: Seq T :: { Seq#Equal(s0,s1) }
+  Seq#Equal(s0,s1) <==>
+    Seq#Length(s0) == Seq#Length(s1) &&
+    (forall j: int :: { Seq#Index(s0,j) } { Seq#Index(s1,j) }
+        0 <= j && j < Seq#Length(s0) ==> Seq#Index(s0,j) == Seq#Index(s1,j)));
+axiom(forall<T> a: Seq T, b: Seq T :: { Seq#Equal(a,b) }  // extensionality axiom for sequences
+  Seq#Equal(a,b) ==> a == b);
+
+function Seq#SameUntil<T>(Seq T, Seq T, int) returns (bool);
+axiom (forall<T> s0: Seq T, s1: Seq T, n: int :: { Seq#SameUntil(s0,s1,n) }
+  Seq#SameUntil(s0,s1,n) <==>
+    (forall j: int :: { Seq#Index(s0,j) } { Seq#Index(s1,j) }
+        0 <= j && j < n ==> Seq#Index(s0,j) == Seq#Index(s1,j)));
+
+function Seq#Take<T>(Seq T, howMany: int) returns (Seq T);
+axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Take(s,n)) }
+  0 <= n ==>
+    (n <= Seq#Length(s) ==> Seq#Length(Seq#Take(s,n)) == n) &&
+    (Seq#Length(s) < n ==> Seq#Length(Seq#Take(s,n)) == Seq#Length(s)));
+axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Take(s,n), j) }
+  0 <= j && j < n && j < Seq#Length(s) ==>
+    Seq#Index(Seq#Take(s,n), j) == Seq#Index(s, j));
+
+function Seq#Drop<T>(Seq T, howMany: int) returns (Seq T);
+axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Drop(s,n)) }
+  0 <= n ==>
+    (n <= Seq#Length(s) ==> Seq#Length(Seq#Drop(s,n)) == Seq#Length(s) - n) &&
+    (Seq#Length(s) < n ==> Seq#Length(Seq#Drop(s,n)) == 0));
+axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Drop(s,n), j) }
+  0 <= n && 0 <= j && j < Seq#Length(s)-n ==>
+    Seq#Index(Seq#Drop(s,n), j) == Seq#Index(s, j+n));
+
+function Seq#Range(min: int, max: int) returns (Seq int);
+
+axiom (forall min: int, max: int :: { Seq#Length(Seq#Range(min, max)) } (min < max ==> Seq#Length(Seq#Range(min, max)) == max-min) && (max <= min ==> Seq#Length(Seq#Range(min, max)) == 0));
+axiom (forall min: int, max: int, j: int :: { Seq#Index(Seq#Range(min, max), j) } 0<=j && j<max-min ==> Seq#Index(Seq#Range(min, max), j) == min + j);
+
+axiom (forall h: HeapType, m: MaskType, o: ref, q: ref :: {wf(h, m), h[o, mu], h[q, mu]} wf(h, m) && o!=q && (0 < h[o, held]) && (0 < h[q, held]) ==> h[o, mu] != h[q, mu]);
+
+function DecPerm<T>(m: MaskType, o: ref, f: Field T, howMuch: int) returns (MaskType);
+
+axiom (forall<T,U> m: MaskType, o: ref, f: Field T, howMuch: int, q: ref, g: Field U :: {DecPerm(m, o, f, howMuch)[q, g][perm$R]}
+      DecPerm(m, o, f, howMuch)[q, g][perm$R] == ite(o==q && f ==g, m[q, g][perm$R] - howMuch, m[q, g][perm$R])
+);
+
+function DecEpsilons<T>(m: MaskType, o: ref, f: Field T, howMuch: int) returns (MaskType);
+
+axiom (forall<T,U> m: MaskType, o: ref, f: Field T, howMuch: int, q: ref, g: Field U :: {DecPerm(m, o, f, howMuch)[q, g][perm$N]}
+         DecEpsilons(m, o, f, howMuch)[q, g][perm$N] == ite(o==q && f ==g, m[q, g][perm$N] - howMuch, m[q, g][perm$N])
+);
+
+function IncPerm<T>(m: MaskType, o: ref, f: Field T, howMuch: int) returns (MaskType);
+
+axiom (forall<T,U> m: MaskType, o: ref, f: Field T, howMuch: int, q: ref, g: Field U :: {IncPerm(m, o, f, howMuch)[q, g][perm$R]}
+         IncPerm(m, o, f, howMuch)[q, g][perm$R] == ite(o==q && f ==g, m[q, g][perm$R] + howMuch, m[q, g][perm$R])
+);
+
+function IncEpsilons<T>(m: MaskType, o: ref, f: Field T, howMuch: int) returns (MaskType);
+
+axiom (forall<T,U> m: MaskType, o: ref, f: Field T, howMuch: int, q: ref, g: Field U :: {IncPerm(m, o, f, howMuch)[q, g][perm$N]}
+         IncEpsilons(m, o, f, howMuch)[q, g][perm$N] == ite(o==q && f ==g, m[q, g][perm$N] + howMuch, m[q, g][perm$N])
+);
+
+function Havocing<T,U>(h: HeapType, o: ref, f: Field T, newValue: U) returns (HeapType);
+
+axiom (forall<T,U> h: HeapType, o: ref, f: Field T, newValue: U, q: ref, g: Field U :: {Havocing(h, o, f, newValue)[q, g]}
+         Havocing(h, o, f, newValue)[q, g] == ite(o==q && f ==g, newValue, h[q, g])
+);
+
+const unique joinable: Field int;
+axiom NonPredicateField(joinable);
+const unique token#t: TypeName;
+
+function Call$Heap(int) returns (HeapType);
+function Call$Mask(int) returns (MaskType);
+function Call$Args(int) returns (ArgSeq);
+type ArgSeq = <T>[int]T;
+
+function EmptyMask(m: MaskType) returns (bool);
+axiom (forall m: MaskType :: {EmptyMask(m)} EmptyMask(m) <==> (forall<T> o: ref, f: Field T :: NonPredicateField(f) ==> m[o, f][perm$R]<=0 && m[o, f][perm$N]<=0));
+
+function NonPredicateField<T>(f: Field T) returns (bool);
+function PredicateField<T>(f: Field T) returns (bool);
+axiom (forall<T> f: Field T :: NonPredicateField(f) ==> ! PredicateField(f));
+axiom (forall<T> f: Field T :: PredicateField(f) ==> ! NonPredicateField(f));
+
+function submask(m1: MaskType, m2: MaskType) returns (bool);
+
+axiom (forall m1: MaskType, m2: MaskType :: {submask(m1, m2)}
+  submask(m1, m2) <==> (forall<T> o: ref, f: Field T :: (m1[o, f][perm$R] < m2[o, f][perm$R]) || (m1[o, f][perm$R] == m2[o, f][perm$R] && m1[o, f][perm$N] <= m2[o, f][perm$N]))
+);
+
+"""
+}
diff --git a/Chalice/src/PrettyPrinter.scala b/Chalice/src/PrettyPrinter.scala
new file mode 100644
index 00000000..b93c23bd
--- /dev/null
+++ b/Chalice/src/PrettyPrinter.scala
@@ -0,0 +1,292 @@
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+object PrintProgram {
+  def P(prog: List[Class]) =
+    for (cl <- prog) {
+      if (cl.IsExternal) print("external ")
+      println("class " + cl.id + " module " + cl.module + " {")
+      cl.members foreach Member
+      println("}")
+    }
+  def Semi = ";"
+  def Member(m: Member) = m match {
+    case MonitorInvariant(e) =>
+      print("  invariant "); Expr(e); println(Semi)
+    case f@ Field(id, t) =>
+      println("  " + (if (f.IsGhost) "ghost " else "") + "var " + id + ": " + t.id + Semi)
+    case m: Method =>
+      print("  method " + m.id)
+      print("("); VarList(m.ins); print(")")
+      if (m.outs != Nil) {
+        print(" returns ("); VarList(m.outs); print(")")
+      }
+      println
+      m.spec foreach {
+        case Precondition(e) => print("    requires "); Expr(e); println(Semi)
+        case Postcondition(e) => print("    ensures "); Expr(e); println(Semi)
+        case LockChange(ee) => print("    lockchange "); ExprList(ee); println(Semi)
+      }
+      println("  {");
+      for (s <- m.body) {
+        print("    "); Stmt(s, 4)
+      }
+      println("  }")
+    case Predicate(id, definition) =>
+      print("  predicate " + id + "  { " + Expr(definition) + "}")
+    case Function(id, ins, out, specs, e) =>
+      print("  function " + id + "(" + VarList(ins) + ")" + ": " + out.id);
+      specs foreach {
+        case Precondition(e) => print("    requires "); Expr(e); println(Semi)
+        case Postcondition(e) => print("    ensures "); Expr(e); println(Semi)
+        case LockChange(ee) => print("    lockchange "); ExprList(ee); println(Semi)
+      }
+      print("  { " + Expr(e) + "}");
+  }
+  def Stmt(s: Statement, indent: int): unit = s match {
+    case Assert(e) =>
+      print("assert "); Expr(e); println(Semi)
+    case Assume(e) =>
+      print("assume "); Expr(e); println(Semi)
+    case BlockStmt(ss) =>
+      PrintBlockStmt(ss, indent); println
+    case IfStmt(guard, BlockStmt(thn), els) =>
+      print("if ("); Expr(guard); print(") ")
+      PrintBlockStmt(thn, indent)
+      els match {
+        case None => println
+        case Some(s) => print(" else "); Stmt(s, indent)
+      }
+    case WhileStmt(guard, invs, lkch, body) =>
+      print("while ("); Expr(guard); println(")")
+      for (inv <- invs) {
+        Spaces(indent+2)
+        print("invariant "); Expr(inv); println(Semi)
+      }
+      for (l <- lkch) {
+        Spaces(indent+2)
+        print("lockchange "); Expr(l); println(Semi)
+      }
+      Spaces(indent); Stmt(body, indent)
+    case Assign(lhs,rhs) =>
+      Expr(lhs); print(" := "); Rhs(rhs); println(Semi)
+    case FieldUpdate(lhs,rhs) =>
+      Expr(lhs); print(" := "); Rhs(rhs); println(Semi)
+    case LocalVar(id,t,c,g,rhs) =>
+      if (g) print("ghost ")
+      if (c) print("const ") else print("var ")
+      print(id + ": " + t.id)
+      rhs match { case None => case Some(rhs) => print(" := "); Rhs(rhs) }
+      println(Semi)
+    case Call(outs, obj, id, args) =>
+      print("call ")
+      outs match {
+        case Nil =>
+        case x :: xs => Expr(x); xs foreach { x => print(", "); Expr(x) }; print(" := ")
+      }
+      MemberSelect(obj,id,0,false)
+      print("(")
+      ExprList(args)
+      println(");")
+    case Install(obj,lower,upper) =>
+      print("reorder ")
+      Expr(obj)
+      PrintBounds(lower, upper)
+      println(Semi)
+    case Share(obj,lower,upper) =>
+      print("share ")
+      Expr(obj)
+      PrintBounds(lower, upper)
+      println(Semi)
+    case Unshare(e) =>
+      print("unshare "); Expr(e); println(Semi)
+    case Acquire(e) =>
+      print("acquire "); Expr(e); println(Semi)
+    case Release(e) =>
+      print("release "); Expr(e); println(Semi)
+    case RdAcquire(e) =>
+      print("rd acquire "); Expr(e); println(Semi)
+    case RdRelease(e) =>
+      print("rd release "); Expr(e); println(Semi)
+    case Lock(e, b, rdLock) =>
+      if (rdLock) print("rd lock (") else print("lock (")
+      Expr(e); print(") ")
+      Stmt(b, indent)
+    case Downgrade(e) =>
+      print("downgrade "); Expr(e); println(Semi)
+    case Free(e) =>
+      print("free "); Expr(e); println(Semi)
+    case Fold(e) =>
+      print("fold "); Expr(e); println(Semi)
+    case Unfold(e) =>
+      print("unfold "); Expr(e); println(Semi)
+    case CallAsync(declaresLocal, token, obj, name, args) =>
+      print("call async ");
+      if (token != null) {
+        Expr(token); print(" := ");
+      }
+      Expr(obj); print("."); print(name); print("("); ExprList(args); print(")");
+    case JoinAsync(lhs, token) =>
+      print("join async "); ExprList(lhs); print(" := "); Expr(token);
+  }
+  def PrintBounds(lower: List[Expression], upper: List[Expression]) = {
+    if (lower == Nil && upper == Nil) {
+    } else if (lower == Nil) {
+      print(" below "); ExprList(upper)
+    } else if (upper == Nil) {
+      print(" above "); ExprList(lower)
+    } else {
+      print(" between "); ExprList(lower); print(" and "); ExprList(upper)
+    }
+  }
+  def PrintBlockStmt(ss: List[Statement], indent: int) = {
+    println("{")
+    for (s <- ss) { Spaces(indent+2); Stmt(s, indent+2) }
+    Spaces(indent);  print("}")
+  }
+  def VarList(vv: List[Variable]) = vv match {
+    case Nil =>
+    case v :: rest =>
+      print(v.id + ": " + v.t.id)
+      rest foreach { v => print(", " + v.id + ": " + v.t.id) }
+  }
+  def ExprList(ee: List[Expression]) = ee match {
+    case Nil =>
+    case e :: rest =>
+      Expr(e)
+      rest foreach { e => print(", "); Expr(e) }
+  }
+  def Rhs(e: RValue) = e match {
+    case NewRhs(id, initialization) => 
+      print("new " + id); 
+      if(0 < initialization.length) { 
+        print(" {"); print(initialization(0).id); print(":="); Expr(initialization(0).e); initialization.foreach({ init => print(", "); print(init.id); print(":="); Expr(init.e); }); print("}");
+      }
+    case e: Expression => Expr(e)
+  }
+  def Expr(e: Expression): Unit = Expr(e, 0, false)
+  def Expr(e: Expression, contextBindingPower: int, fragileContext: boolean): Unit = e match {
+    case IntLiteral(n) => print(n)
+    case BoolLiteral(b) => print(b)
+    case NullLiteral() => print("null")
+    case MaxLockLiteral() => print("maxlock")
+    case LockBottomLiteral() => print("lockbottom")
+    case _:ThisExpr => print("this")
+    case _:Result => print("result")
+    case VariableExpr(id) => print(id)
+    case MemberAccess(e,f) => MemberSelect(e,f,contextBindingPower,fragileContext)
+    case Access(e,perm) =>
+      print("acc("); Expr(e)
+      perm match { case None => case Some(perm) => print(", "); Expr(perm) }
+      print(")")
+    case RdAccess(e,p) =>
+      print("rd("); Expr(e)
+      p match {
+        case None =>          print(")")
+        case Some(None) =>    print(", *)")
+        case Some(Some(e)) => print(", "); Expr(e); print(")")
+      }
+    case AccessAll(obj, perm) =>
+      print("acc("); Expr(obj); print(".*");
+      perm match { case None => case Some(perm) => print(", "); Expr(perm) }
+      print(")")
+    case RdAccessAll(obj, p) =>
+     print("rd("); Expr(e); print(".*");
+      p match {
+        case None =>          print(")")
+        case Some(None) =>    print(", *)")
+        case Some(Some(e)) => print(", "); Expr(e); print(")")
+      }
+    case Holds(e) =>
+          print("holds("); Expr(e); print(")")
+    case RdHolds(e) =>
+          print("rd holds("); Expr(e); print(")")
+    case Assigned(id) => print("assigned(" + id + ")")
+    case Old(e) =>
+          print("old("); Expr(e); print(")")
+    case IfThenElse(con, then, els) => 
+      print("ite("); Expr(con); print(", "); Expr(then); print(", "); Expr(els); print(")");
+    case Not(e) => print("!"); Expr(e, 0x80, false)
+    case FunctionApplication(obj, id, ins) =>
+      Expr(obj); print("."); print(id); print("("); ExprList(ins); print(")");
+    case Unfolding(pred, e) =>
+      print("unfolding "); Expr(pred); print(" in "); Expr(e); 
+    case e:Iff => BinExpr(e, e.OpName, 0x10, false, false, contextBindingPower, fragileContext)
+    case e:Implies => BinExpr(e, e.OpName, 0x20, true, false, contextBindingPower, fragileContext)
+    case e:And => BinExpr(e, e.OpName, 0x30, false, false, contextBindingPower, fragileContext)
+    case e:Or => BinExpr(e, e.OpName, 0x31, false, false, contextBindingPower, fragileContext)
+    case e:Eq => BinExpr(e, e.OpName, 0x40, true, true, contextBindingPower, fragileContext)
+    case e:Neq => BinExpr(e, e.OpName, 0x40, true, true, contextBindingPower, fragileContext)
+    case e:Less => BinExpr(e, e.OpName, 0x40, true, true, contextBindingPower, fragileContext)
+    case e:AtMost => BinExpr(e, e.OpName, 0x40, true, true, contextBindingPower, fragileContext)
+    case e:AtLeast => BinExpr(e, e.OpName, 0x40, true, true, contextBindingPower, fragileContext)
+    case e:Greater => BinExpr(e, e.OpName, 0x40, true, true, contextBindingPower, fragileContext)
+    case e:LockBelow => BinExpr(e, e.OpName, 0x40, true, true, contextBindingPower, fragileContext)
+    case e:Plus => BinExpr(e, e.OpName, 0x50, false, false, contextBindingPower, fragileContext)
+    case e:Minus => BinExpr(e, e.OpName, 0x50, false, true, contextBindingPower, fragileContext)
+    case e:Times => BinExpr(e, e.OpName, 0x60, false, false, contextBindingPower, fragileContext)
+    case e:Div => BinExpr(e, e.OpName, 0x60, false, true, contextBindingPower, fragileContext)
+    case e:Mod => BinExpr(e, e.OpName, 0x60, false, true, contextBindingPower, fragileContext)
+    case q:Quantification => 
+      print(q.Quantor + "{"); 
+      q.Is match {
+        case Nil =>
+        case i :: rest => print(i); rest foreach { v => print(", " + v) }
+      }
+      print(" in "); Expr(q.Seq); print("; "); Expr(q.E); print("}");
+    case EmptySeq(t) =>
+      print("nil<"); print(t.FullName); print(">");
+    case ExplicitSeq(es) =>
+      print("["); ExprList(es); print("]");
+    case Range(min, max) =>
+      print("("); Expr(min); print(":"); Expr(max); print(")");
+    case Length(e)=>
+      print("|"); Expr(e); print("|");
+    case e:At =>
+      BinExpr(e, e.OpName, 0x45, true, true, contextBindingPower, fragileContext)
+    case e:Append =>
+      BinExpr(e, e.OpName, 0x45, true, true, contextBindingPower, fragileContext)
+    case Drop(s, n) =>
+      Expr(s); print("["); Expr(n); print(" ..]");
+    case Take(s, n) =>
+      Expr(s); print("[.. "); Expr(n); print("]");
+    case Eval(h, e) =>
+      print("eval("); (h match 
+        { 
+          case AcquireState(obj) => Expr(obj); print(".acquire"); 
+          case ReleaseState(obj) => Expr(obj); print(".release"); 
+          case CallState(token, obj, id, args) => Expr(token); print(".joinable"); print(", "); Expr(obj); print("." + id + "("); ExprList(args); print(")"); 
+        }); print(", "); Expr(e); print(")"); 
+  }
+  def MemberSelect(e: Expression, f: String, contextBindingPower: int, fragileContext: boolean) = e match {
+    case e:ImplicitThisExpr => print(f)
+    case _ =>
+      ParenExpr(0x90, contextBindingPower, fragileContext, { Expr(e,0x90,false); print("." + f) })
+  }
+  def BinExpr(bin: BinaryExpr, op: String, power: int, fragileLeft: boolean, fragileRight: boolean,
+              context: int, fragileContext: boolean) = {
+    ParenExpr(power, context, fragileContext,
+          { Expr(bin.E0, power, fragileLeft); print(" " + op + " "); Expr(bin.E1, power, fragileRight) })
+  }
+  def ParenExpr(power: int, context: int, fragileContext: boolean, pe: =>Unit) {
+    val ap = power & 0xF0;
+    val cp = context & 0xF0;
+    val parensNeeded = ap < cp || (ap == cp && (power != context || fragileContext));
+    if (parensNeeded) { print("(") }
+    pe
+    if (parensNeeded) { print(")") }
+  }
+  def Spaces(N: int) = {
+    val abunchaSpaces = "          "
+    var n = N
+    while (abunchaSpaces.length <= n) {
+      print(abunchaSpaces)
+      n = n - abunchaSpaces.length
+    }
+    if (0 < n) {
+      print(abunchaSpaces.substring(0, n))
+    }
+  }
+}
diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala
new file mode 100644
index 00000000..c7bdfd15
--- /dev/null
+++ b/Chalice/src/Resolver.scala
@@ -0,0 +1,940 @@
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+import scala.util.parsing.input.Position
+import scala.util.parsing.input.Positional
+
+object Resolver {
+  sealed abstract class ResolverOutcome
+  case class Success extends ResolverOutcome
+  case class Error(pos: Position, s: String) extends ResolverOutcome
+  case class Errors(ss: List[String]) extends ResolverOutcome
+
+  var seqClasses = Map[String, SeqClass]();
+
+  class ProgramContext(classes: Map[String,Class], currentClass: Class) {
+    val Classes = classes
+    val CurrentClass = currentClass
+    var currentMember = null: Member;
+    def CurrentMember = currentMember: Member;  
+    var errors: List[String] = Nil
+    def Error(pos: Position, msg: String) {
+      errors = errors + (pos + ": " + msg)
+    }
+    def AddVariable(v: Variable): ProgramContext = {
+      new LProgramContext(v, this);
+    }
+    def LookupVariable(id: String): Option[Variable] = None
+    def IsVariablePresent(vr: Variable): boolean = false
+
+    private class LProgramContext(v: Variable, parent: ProgramContext) extends ProgramContext(parent.Classes, parent.CurrentClass) {
+      override def Error(pos: Position, msg: String) = parent.Error(pos, msg)
+      override def LookupVariable(id: String): Option[Variable] = {
+        if (id == v.id) Some(v) else parent.LookupVariable(id)
+      }
+      override def IsVariablePresent(vr: Variable): boolean = {
+        if (vr == v) true else parent.IsVariablePresent(vr)
+      }
+      override def CurrentMember() = {
+        parent.CurrentMember
+      }
+    }
+  }
+
+  def Resolve(prog: List[Class]): ResolverOutcome = {
+    // register the classes and their members
+    var classes = Map[String,Class]()
+    for (cl <- BoolClass :: IntClass :: RootClass :: NullClass :: MuClass :: prog) {
+      if (classes contains cl.id) {
+        return Error(cl.pos, "duplicate class name: " + cl.id)
+      } else {
+        for (m <- cl.members) m match {
+          case _:MonitorInvariant =>
+          case m: NamedMember =>
+            m.Parent = cl
+            if (cl.mm contains m.Id) {
+              return Error(m.pos, "duplicate member name " + m.Id + " in class " + cl.id)
+            } else {
+              cl.mm = cl.mm + (m.Id -> m)
+            }
+        }
+        classes = classes + (cl.id -> cl)
+      }
+    }
+    var errors = List[String]()
+
+    // resolve types of fields and methods
+    val contextNoCurrentClass = new ProgramContext(classes, null)
+    for (cl <- prog; m <- cl.members) m match {
+      case _:MonitorInvariant =>
+      case Field(id,t) =>
+        ResolveType(t, contextNoCurrentClass)
+      case Method(id, ins, outs, spec, body) =>
+        for (v <- ins ++ outs) {
+          ResolveType(v.t, contextNoCurrentClass)
+        }
+      case Predicate(id, definition) => 
+      case Function(id, ins, out, specs, definition) => 
+        for (v <- ins) {
+          ResolveType(v.t, contextNoCurrentClass)
+        }
+        ResolveType(out, contextNoCurrentClass)
+    }
+    errors = errors ++ contextNoCurrentClass.errors;
+
+    // now, resolve and typecheck all
+    //  * Field types and Method formal-parameter types
+    //  * Assign, FieldUpdate, and Call statements
+    //  * VariableExpr and FieldSelect expressions
+    for (cl <- prog) {
+      val context = new ProgramContext(classes, cl)
+      for (m <- cl.members) {
+        context.currentMember = m;
+        m match {
+          case MonitorInvariant(e) =>
+            ResolveExpr(e, context, true, true)(true)
+            if (!e.typ.IsBool) context.Error(m.pos, "monitor invariant requires a boolean expression (found " + e.typ.FullName + ")")
+          case _:Field => // nothing more to do
+          case m@Method(id, ins, outs, spec, body) =>
+            var ctx = context
+            for (v <- ins ++ outs) {
+              ctx = ctx.AddVariable(v)
+            }
+            spec foreach {
+              case Precondition(e) => ResolveExpr(e, ctx, false, true)(false)
+              case Postcondition(e) => ResolveExpr(e, ctx, true, true)(false)
+              case lc@LockChange(ee) => 
+              if(m.id.equals("run")) context.Error(lc.pos, "lockchange not allowed on method run") 
+              ee foreach (e => ResolveExpr(e, ctx, true, false)(false))
+            }
+            ResolveStmt(BlockStmt(body), ctx)
+          case p@Predicate(id, e) =>
+            var ctx = context;
+            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, e) =>
+            var ctx = context
+            for (v <- ins) {
+              ctx = ctx.AddVariable(v)
+            }
+            spec foreach {
+              case Precondition(e) => ResolveExpr(e, ctx, false, true)(false)
+              case pc@Postcondition(e) => assert(ctx.CurrentMember != null); ResolveExpr(e, ctx, false, true)(false)
+              case lc@LockChange(ee) => context.Error(lc.pos, "lockchange not allowed on function") 
+            }
+            ResolveExpr(e, ctx, false, false)(false)
+            if(! canAssign(out.typ, e.typ)) context.Error(e.pos, "function body does not match declared type (expected: " + out.FullName + ", found: " + e.typ.FullName + ")")
+        }
+      }
+      errors = errors ++ context.errors
+    }
+
+    if (errors.length == 0) {
+      Success()
+    } else {
+      Errors(errors)
+    }
+  }
+
+  def ResolveType(t: Type, context: ProgramContext): unit = {
+      for(p <- t.params){
+        ResolveType(p, context);
+      }
+      if(t.isInstanceOf[TokenType]){
+        val tt = t.asInstanceOf[TokenType];
+        ResolveType(tt.C, context);
+        if(! tt.C.typ.IsNormalClass) context.Error(t.pos, "Invalid token type. " + tt.C.FullName + " is not a user-defined class.");
+        tt.C.typ.LookupMember(tt.m) match {
+          case Some(m: Method) => val tc = TokenClass(tt.C, tt.m); tc.method = m; tt.typ = tc;
+          case _ => context.Error(t.pos, "Invalid token type. " + tt.C.FullName + " does not declare a method " + tt.m + ".");
+        }
+        return;
+      }
+      if (context.Classes contains t.FullName) {
+        t.typ = context.Classes(t.FullName)
+      } else {
+        if(seqClasses.contains(t.FullName)) {
+          t.typ = seqClasses(t.FullName)
+        } else if(t.id.equals("seq") && t.params.length == 1) {
+          val seqt = new SeqClass(t.params(0).typ);
+          seqClasses = seqClasses + ((seqt.FullName, seqt));
+          t.typ = seqt;
+        } else {
+          context.Error(t.pos, "undeclared type " + t.FullName)
+          t.typ = IntClass
+        }
+      }
+  }
+
+  def getSeqType(param: Class, context: ProgramContext): Class = {
+    if(seqClasses.contains("seq<" + param.FullName + ">")) {
+      seqClasses("seq<" + param.FullName + ">")
+    } else {
+      val seqt = new SeqClass(param);
+      seqClasses = seqClasses + ((seqt.FullName, seqt));
+      seqt
+    }
+  }
+
+  def ResolveStmt(s: Statement, context: ProgramContext): unit = s match {
+    case Assert(e) =>
+      ResolveExpr(e, context, true, true)(false)
+      if (!e.typ.IsBool) context.Error(e.pos, "assert statement requires a boolean expression (found " + e.typ.FullName + ")")
+    case Assume(e) =>
+      ResolveExpr(e, context, false, false)(false)  // assume expressions remain at run-time, so OLD is not allowed
+      if (!e.typ.IsBool) context.Error(e.pos, "assume statement requires a boolean expression (found " + e.typ.FullName + ")")
+      CheckNoGhost(e, context)
+    case BlockStmt(ss) =>
+      var ctx = context
+      for (s <- ss) s match {
+        case l @ LocalVar(id, t, c, g, rhs) =>
+          ResolveType(l.v.t, ctx)
+          val oldCtx = ctx
+          ctx = ctx.AddVariable(l.v)
+          rhs match {
+            case None =>
+            case Some(rhs) =>
+              val lhs = VariableExpr(id)
+              lhs.pos = l.pos;
+              ResolveExpr(lhs, ctx, false, false)(false)
+              ResolveAssign(lhs, rhs, oldCtx)
+          }
+        case c@CallAsync(declaresLocal, token, obj, id, args) =>
+          ResolveStmt(c, ctx)
+          if (declaresLocal) {
+            c.local = new Variable(token.id, TokenType(new Type(obj.typ), id))
+            ResolveType(c.local.t, ctx)
+            ctx = ctx.AddVariable(c.local)
+            ResolveExpr(token, ctx, false, false)(false)
+          }
+        case s =>
+          ResolveStmt(s, ctx)
+      }
+    case IfStmt(guard, thn, els) =>
+      ResolveExpr(guard, context, false, false)(false)
+      if (!guard.typ.IsBool) context.Error(guard.pos, "if statement requires a boolean guard (found " + guard.typ.FullName + ")")
+      CheckNoGhost(guard, context)
+      ResolveStmt(thn, context)
+      els match { case None => case Some(s) => ResolveStmt(s, context) }
+    case w@ WhileStmt(guard, invs, lkch, body) =>
+      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)
+      for (inv <- invs) {
+        ResolveExpr(inv, context, true, true)(false)
+        if (!inv.typ.IsBool) context.Error(inv.pos, "loop invariant must be boolean (found " + inv.typ.FullName + ")")
+      }
+      for (l <- lkch) {
+        ResolveExpr(l, context, true, false)(false)
+        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
+    case Assign(lhs, rhs) => 
+      ResolveExpr(lhs, context, false, false)(false)
+      ResolveAssign(lhs, rhs, context)
+      if (lhs.v != null && lhs.v.IsImmutable) {
+        if (lhs.v.IsGhost)
+          CheckNoGhost(rhs, context)
+        else
+          context.Error(lhs.pos, "cannot assign to immutable variable " + lhs.v.id)
+      }
+    case fu@FieldUpdate(lhs, rhs) =>
+      ResolveExpr(lhs, context, false, false)(false)
+      if (! lhs.isPredicate && lhs.f != null && !lhs.f.IsGhost) CheckNoGhost(lhs.e, context)
+      if (! lhs.isPredicate && lhs.f.isInstanceOf[SpecialField]) context.Error(lhs.pos, "cannot assign directly to special field: " + lhs.id)
+      ResolveExpr(rhs, context, false, false)(false)
+      if (! lhs.isPredicate && !canAssign(lhs.typ, rhs.typ)) context.Error(fu.pos, "type mismatch in assignment, lhs=" + lhs.typ.FullName + " rhs=" + rhs.typ.FullName)
+      if (! lhs.isPredicate && lhs.f != null && !lhs.f.IsGhost) CheckNoGhost(rhs, context)
+    case lv:LocalVar => throw new Exception("unexpected LocalVar; should have been handled in BlockStmt above")
+    case c @ Call(lhs, obj, id, args) =>
+      ResolveExpr(obj, context, false, false)(false)
+      CheckNoGhost(obj, context)
+      args foreach { a => ResolveExpr(a, context, false, false)(false); CheckNoGhost(a, context) }
+      var vars = Set[Variable]()
+      for (v <- lhs) {
+        ResolveExpr(v, context, false, false)(false)
+        if (v.v != null) {
+          if (v.v.IsImmutable) context.Error(v.pos, "cannot use immutable variable " + v.id + " as actual out-parameter")
+          if (vars contains v.v) {
+            context.Error(v.pos, "duplicate actual out-parameter: " + v.id)
+          } else {
+            vars = vars + v.v
+          }
+        }
+      }
+      // lookup method
+      var typ: Class = IntClass
+      obj.typ.LookupMember(id) match {
+        case None =>
+          context.Error(c.pos, "call of undeclared member " + id + " in class " + obj.typ.FullName)
+        case Some(m: Method) =>
+          c.m = m
+          if (args.length != m.ins.length)
+            context.Error(c.pos, "wrong number of actual in-parameters in call to " + obj.typ.FullName + "." + id +
+                          " (" + args.length + " instead of " + m.ins.length + ")")
+          else {
+            for((actual, formal) <- args zip m.ins){
+              if(! canAssign(formal.t.typ, actual.typ))
+                context.Error(actual.pos, "the type of the actual argument is not assignable to the formal parameter (expected: " + formal.t.FullName + ", found: " + actual.typ.FullName + ")")
+            }
+          }     
+          if (lhs.length != m.outs.length)
+            context.Error(c.pos, "wrong number of actual out-parameters in call to " + obj.typ.FullName + "." + id +
+                          " (" + lhs.length + " instead of " + m.outs.length + ")")
+          else {
+            for((out, l) <- m.outs zip lhs){
+              if(! canAssign(l.typ, out.t.typ))
+                context.Error(l.pos, "the out parameter cannot be assigned to the lhs (expected: " + l.typ.FullName + ", found: " + out.t.FullName + ")")
+            }
+          }
+
+        case _ => context.Error(c.pos, "call expression does not denote a method: " + obj.typ.FullName + "." + id)
+      }
+    case Install(obj, lowerBounds, upperBounds) =>
+      ResolveExpr(obj, context, false, false)(false)
+      if (!obj.typ.IsRef) context.Error(obj.pos, "object in install statement must be of a reference type (found " + obj.typ.FullName + ")")
+      for (b <- lowerBounds ++ upperBounds) {
+        ResolveExpr(b, context, true, false)(false)
+        if (!b.typ.IsRef && !b.typ.IsMu) context.Error(b.pos, "install bound must be of a reference type or Mu type" +
+                                                       " (found " + b.typ.FullName + ")")
+      }
+    case Share(obj, lowerBounds, upperBounds) =>
+      ResolveExpr(obj, context, false, false)(false)
+      CheckNoGhost(obj, context)
+      if (!obj.typ.IsRef) context.Error(obj.pos, "object in share statement must be of a reference type (found " + obj.typ.FullName + ")")
+      for (b <- lowerBounds ++ upperBounds) {
+        ResolveExpr(b, context, true, false)(false)
+        if (!b.typ.IsRef && !b.typ.IsMu) context.Error(b.pos, "share bound must be of a reference type or Mu type" +
+                                                       " (found " + b.typ.FullName + ")")
+      }
+    case Unshare(obj) =>
+      ResolveExpr(obj, context, false, false)(false)
+      CheckNoGhost(obj, context)
+      if (!obj.typ.IsRef) context.Error(obj.pos, "object in unshare statement must be of a reference type (found " + obj.typ.FullName + ")")
+    case Acquire(obj) =>
+      ResolveExpr(obj, context, false, false)(false)
+      CheckNoGhost(obj, context)
+      if (!obj.typ.IsRef) context.Error(obj.pos, "object in acquire statement must be of a reference type (found " + obj.typ.FullName + ")")
+    case Release(obj) =>
+      ResolveExpr(obj, context, false, false)(false)
+      CheckNoGhost(obj, context)
+      if (!obj.typ.IsRef) context.Error(obj.pos, "object in release statement must be of a reference type (found " + obj.typ.FullName + ")")
+    case RdAcquire(obj) =>
+      ResolveExpr(obj, context, false, false)(false)
+      CheckNoGhost(obj, context)
+      if (!obj.typ.IsRef) context.Error(obj.pos, "object in rd acquire statement must be of a reference type (found " + obj.typ.FullName + ")")
+    case RdRelease(obj) =>
+      ResolveExpr(obj, context, false, false)(false)
+      CheckNoGhost(obj, context)
+      if (!obj.typ.IsRef) context.Error(obj.pos, "object in rd release statement must be of a reference type (found " + obj.typ.FullName + ")")
+    case Lock(obj, b, rdLock) =>
+      ResolveExpr(obj, context, false, false)(false)
+      CheckNoGhost(obj, context)
+      if (!obj.typ.IsRef) {
+        val sname = if (rdLock) "rd lock" else "lock";
+        context.Error(obj.pos, "object in " + sname + " statement must be of a reference type (found " + obj.typ.FullName + ")")
+                                       
+      }
+      ResolveStmt(b, context)
+    case Downgrade(obj) =>
+      ResolveExpr(obj, context, false, false)(false)
+      CheckNoGhost(obj, context)
+      if (!obj.typ.IsRef) context.Error(obj.pos, "object in downgrade statement must be of a reference type (found " + obj.typ.FullName + ")")
+    case Free(obj) =>
+      ResolveExpr(obj, context, false, false)(false)
+      CheckNoGhost(obj, context)
+      if (!obj.typ.IsRef) context.Error(obj.pos, "object in free statement must be of a reference type (found " + obj.typ.FullName + ")")
+    case fld@Fold(e) =>
+      ResolveExpr(e, context, false, true)(false);
+      CheckNoGhost(e, context);
+      if(!e.getMemberAccess.isPredicate) context.Error(fld.pos, "Fold can only be applied to predicates.")
+    case ufld@Unfold(e) =>
+      ResolveExpr(e, context, false, true)(false);
+      CheckNoGhost(e, context);
+      if(!e.getMemberAccess.isPredicate) context.Error(ufld.pos, "Unfold can only be applied to predicates.")
+    case c@CallAsync(declaresLocal, token, obj, id, args) => 
+      // resolve receiver      
+      ResolveExpr(obj, context, false, false)(false)
+      CheckNoGhost(obj, context)
+      // resolve arguments
+      args foreach { a => ResolveExpr(a, context, false, false)(false); CheckNoGhost(a, context) }
+      // lookup method
+      var typ: Class = IntClass
+      obj.typ.LookupMember(id) match {
+        case None =>
+          context.Error(c.pos, "call of undeclared member " + id + " in class " + obj.typ.FullName)
+        case Some(m: Method) =>
+          c.m = m
+          if (args.length != m.ins.length)
+            context.Error(c.pos, "wrong number of actual in-parameters in call to " + obj.typ.FullName + "." + id +
+                          " (" + args.length + " instead of " + m.ins.length + ")")
+          else {
+            for((actual, formal) <- args zip m.ins){
+              if(! canAssign(formal.t.typ, actual.typ))
+                context.Error(actual.pos, "the type of the actual argument is not assignable to the formal parameter (expected: " + formal.t.FullName + ", found: " + actual.typ.FullName + ")")
+            }
+          }
+        case _ => context.Error(c.pos, "call expression does not denote a method: " + obj.typ.FullName + "." + id)
+      }
+      // resolve the token
+      if (declaresLocal) {
+        // this is taken care of in the caller that handles the enclosing block statement
+      } else if (token != null) {
+        ResolveExpr(token, context, false, false)(false)
+        if(! canAssign(token.typ, TokenClass(new Type(obj.typ), id)))
+          context.Error(token.pos, "wrong token type")
+      }
+    case jn@JoinAsync(lhs, token) =>
+      // resolve the assignees
+      var vars = Set[Variable]()
+      for (v <- lhs) {
+        ResolveExpr(v, context, false, false)(false)
+        if (v.v != null) {
+          if (v.v.IsImmutable) context.Error(v.pos, "cannot use immutable variable " + v.id + " as actual out-parameter")
+          if (vars contains v.v) {
+            context.Error(v.pos, "duplicate actual out-parameter: " + v.id)
+          } else {
+            vars = vars + v.v
+          }
+        }
+      }
+      // resolve the token
+      ResolveExpr(token, context, false, false)(false);
+      if(token.typ == null || ! token.typ.IsToken || ! token.typ.isInstanceOf[TokenClass] || token.typ.asInstanceOf[TokenClass].method == null)
+        context.Error(token.pos, "the first argument of a join async must be a token")
+      else {
+        val m = token.typ.asInstanceOf[TokenClass].method;
+        jn.m = m
+        if (lhs.length != m.outs.length)
+          context.Error(jn.pos, "wrong number of actual out-parameters in join async of " + m.FullName +
+                         " (" + lhs.length + " instead of " + m.outs.length + ")")
+        else {
+          for((out, l) <- m.outs zip lhs){
+            if(! canAssign(l.typ, out.t.typ))
+              context.Error(l.pos, "the out parameter cannot be assigned to the lhs (expected: " + l.typ.FullName + ", found: " + out.t.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 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
+      case _ => ResolveExpr(rhs, context, false, false)(false)
+    }
+    if (! canAssign(lhs.typ, rhs.typ))
+      context.Error(lhs.pos, "type mismatch in assignment, lhs=" + lhs.typ.FullName + " rhs=" + rhs.typ.FullName)
+    if (lhs.v != null && !lhs.v.IsGhost) CheckNoGhost(rhs, context)
+  }
+
+  // ResolveExpr resolves all parts of an RValue, if possible, and (always) sets the RValue's typ field
+  def ResolveExpr(e: RValue, context: ProgramContext,
+                  twoStateContext: boolean, specContext: boolean)(implicit inPredicate: Boolean): unit = e match {
+    case e @ NewRhs(id, initialization) =>
+      if (context.Classes contains id) {
+        e.typ = context.Classes(id)
+        var fieldNames = Set[String]()
+        for(ini@Init(f, init) <- initialization) {
+          if (fieldNames contains f) {
+            context.Error(ini.pos, "The field " + f + " occurs more than once in initializer.")
+          } else {
+            fieldNames = fieldNames + f
+            e.typ.LookupMember(f) match {
+              case Some(field@Field(name, tp)) =>
+                if(field.isInstanceOf[SpecialField]) context.Error(init.pos, "Initializer cannot assign to special field " + name + ".");
+                ResolveExpr(init, context, false, false);
+                if(! canAssign(tp.typ, init.typ)) context.Error(init.pos, "The field " + name + " cannot be initialized with an expression of type " + init.typ.id + ".");
+                ini.f = field;
+              case _ => 
+                context.Error(e.pos, "The type " + id + " does not declare a field " + f + ".");  
+            }
+          }
+        }
+      } else {
+        context.Error(e.pos, "undefined class " + id + " used in new expression")
+        e.typ = IntClass
+      }
+    case i:IntLiteral =>
+      i.typ = IntClass
+    case b:BoolLiteral =>
+      b.typ = BoolClass
+    case n:NullLiteral =>
+      n.typ = NullClass
+    case mx:MaxLockLiteral =>
+      mx.typ = MuClass
+    case mx:LockBottomLiteral =>
+      mx.typ = MuClass
+    case r:Result =>
+      assert(context.CurrentMember!=null);
+      r.typ = IntClass
+      if(context.CurrentMember==null || ! context.CurrentMember.isInstanceOf[Function]){
+        context.Error(r.pos, "The variable result can only be used in the postcondition of a function.");
+      } else {
+        r.typ = context.CurrentMember.asInstanceOf[Function].out.typ;
+      }
+    case ve @ VariableExpr(id) =>
+      context.LookupVariable(id) match {
+        case None => context.Error(ve.pos, "undefined local variable " + id); ve.typ = IntClass
+        case Some(v) => ve.v = v; ve.typ = v.t.typ }
+    case v:ThisExpr => v.typ = context.CurrentClass
+    case sel @ MemberAccess(e, id) =>
+      ResolveExpr(e, context, twoStateContext, false)
+      var typ: Class = IntClass
+      e.typ.LookupMember(id) match {
+        case None =>
+          context.Error(sel.pos, "undeclared member " + id + " in class " + e.typ.FullName)
+        case Some(f: Field) => sel.f = f; typ = f.typ.typ
+        case Some(pred@Predicate(id, body)) =>
+          if(! specContext)
+            context.Error(sel.pos, "predicate can only be used in positive predicate contexts")
+          sel.predicate = pred;
+          sel.isPredicate = true;
+          typ = BoolClass
+        case _ => context.Error(sel.pos, "field-select expression does not denote a field: " + e.typ.FullName + "." + id);
+      }
+      sel.typ = typ
+    case expr@ Access(e, perm) =>
+      if (!specContext) context.Error(expr.pos, "acc expression is allowed only in positive predicate contexts")
+      ResolveExpr(e, context, twoStateContext, true)
+      perm match {
+        case None =>
+        case Some(perm) => ResolveExpr(perm, context, twoStateContext, false) }
+      expr.typ = BoolClass
+    case expr@ RdAccess(e,perm) =>
+      if (!specContext) context.Error(expr.pos, "rd expression is allowed only in positive predicate contexts")
+      ResolveExpr(e, context, twoStateContext, true)
+      perm match {
+        case Some(Some(p)) => ResolveExpr(p, context, twoStateContext, false)
+        case _ => }
+      expr.typ = BoolClass
+    case expr@AccessAll(obj, perm) =>
+      if (!specContext) context.Error(expr.pos, "acc expression is allowed only in positive predicate contexts")
+      ResolveExpr(obj, context, twoStateContext, false)
+      if(!obj.typ.IsRef) context.Error(expr.pos, "Target of .* must be object reference.")
+      perm match {
+        case None =>
+        case Some(perm) => ResolveExpr(perm, context, twoStateContext, false) }
+      expr.typ = BoolClass
+    case expr@RdAccessAll(obj,perm) =>
+      if (!specContext) context.Error(expr.pos, "rd expression is allowed only in positive predicate contexts")
+      ResolveExpr(obj, context, twoStateContext, false)
+      if(!obj.typ.IsRef) context.Error(expr.pos, "Target of .* must be object reference.")
+      perm match {
+        case Some(Some(p)) => ResolveExpr(p, context, twoStateContext, false)
+        case _ => }
+      expr.typ = BoolClass
+    case expr@ Holds(e) =>
+      if(inPredicate) context.Error(expr.pos, "holds cannot be mentioned in monitor invariants or predicates")
+      if(! specContext)
+        context.Error(expr.pos, "holds is allowed only in positive predicate contexts"); 
+      //todo: check that we are not in an invariant
+      ResolveExpr(e, context, twoStateContext, false)
+      expr.typ = BoolClass
+    case expr@ RdHolds(e) =>
+      if(inPredicate) context.Error(expr.pos, "rdholds cannot be mentioned in monitor invariants or predicates")
+      ResolveExpr(e, context, twoStateContext, false)
+      expr.typ = BoolClass
+    case expr@ Assigned(id) =>
+      context.LookupVariable(id) match {
+        case None => context.Error(expr.pos, "undefined local variable " + id)
+        case Some(v) =>
+          expr.v = v
+          if (!(v.IsImmutable && v.IsGhost))
+            context.Error(expr.pos, "assigned can only be used with ghost consts")
+      }
+      expr.typ = BoolClass
+    case expr@ Old(e) =>
+      if (! twoStateContext) { context.Error(expr.pos, "old expression is not allowed here") }
+      ResolveExpr(e, context, twoStateContext, false)
+      expr.typ = e.typ
+    case ite@IfThenElse(con, then, els) => 
+      ResolveExpr(con, context, twoStateContext, false); ResolveExpr(then, context, twoStateContext, specContext); ResolveExpr(els, context, twoStateContext, specContext);
+      if (!con.typ.IsBool) context.Error(con.pos, "condition of if-then-else expression must be a boolean");
+      if (! canAssign(then.typ, els.typ)) context.Error(ite.pos, "the then and else branch of an if-then-else expression must have compatible types");
+      ite.typ = then.typ;
+    case expr@ Not(e) =>
+      ResolveExpr(e, context, twoStateContext, false)
+      if (!e.typ.IsBool) context.Error(expr.pos, "not-expression requires boolean operand")
+      expr.typ = BoolClass
+    case appl@FunctionApplication(obj, id, args) =>
+      ResolveExpr(obj, context, twoStateContext, false);
+      args foreach { arg => ResolveExpr(arg, context, twoStateContext, false)};
+      // lookup function
+      appl.typ = IntClass
+      obj.typ.LookupMember(id) match {
+        case None =>
+          context.Error(appl.pos, "function " + id + " not found in class " + obj.typ.FullName)
+        case Some(func@Function(f, ins, out, specs, body)) =>
+          appl.f = func
+          appl.typ = func.out.typ;
+          if (args.length != ins.length)
+            context.Error(appl.pos, "wrong number of actual arguments in function application of " + obj.typ.FullName + "." + id +
+                          " (" + args.length + " instead of " + ins.length + ")")
+          else {
+            for((actual, formal) <- args zip func.ins){
+              if(! canAssign(formal.t.typ, actual.typ))
+                context.Error(actual.pos, "the type of the actual argument is not assignable to the formal parameter (expected: " + formal.t.FullName + ", found: " + actual.typ.FullName + ")")
+            }
+          }
+        case _ => context.Error(appl.pos, obj.typ.id + "." + id + " is not a function")
+      }
+    case uf@Unfolding(pred, e) =>
+      ResolveExpr(pred, context, twoStateContext, true);
+      ResolveExpr(e, context, twoStateContext, false);
+      if(! pred.getMemberAccess.isPredicate) context.Error(uf.pos, "Only predicates can be unfolded.")
+      uf.typ = e.typ;
+    case bin: EqualityCompareExpr =>
+      ResolveExpr(bin.E0, context, twoStateContext, false)
+      ResolveExpr(bin.E1, context, twoStateContext, false)
+      if (bin.E0.typ == bin.E1.typ) { /* all is well */ }
+      else if (bin.E0.typ.IsRef && bin.E1.typ.IsNull) { /* all is well */ }
+      else if (bin.E0.typ.IsNull && bin.E1.typ.IsRef) { /* all is well */ }
+      else
+        context.Error(bin.pos, bin.OpName + " requires operands of the same type, found " + bin.E0.typ.FullName + " and " + bin.E1.typ.FullName)
+      bin.typ = BoolClass
+    case bin: LockBelow =>
+      ResolveExpr(bin.E0, context, twoStateContext, false)
+      ResolveExpr(bin.E1, context, twoStateContext, false)
+      if (!(bin.E0.typ.IsRef || bin.E0.typ.IsMu))
+        context.Error(bin.pos, "type of " + bin.OpName + " LHS operand must be a reference or Mu type (found " + bin.E0.typ.FullName + ")")
+      if (!(bin.E1.typ.IsRef || bin.E1.typ.IsMu))
+        context.Error(bin.pos, "type of " + bin.OpName + " RHS operand must be a reference or Mu type (found " + bin.E1.typ.FullName + ")")
+      bin.typ = BoolClass
+    case app@Append(e0, e1) =>
+      ResolveExpr(e0, context, twoStateContext, false);
+      ResolveExpr(e1, context, twoStateContext, false);
+      if(! e0.typ.IsSeq) context.Error(app.pos, "LHS operand of ++ must be sequence (found: " + e0.typ.FullName + ").");
+      if(! e1.typ.IsSeq) context.Error(app.pos, "RHS operand of ++ must be sequence (found: " + e1.typ.FullName + ").");
+      if(e0.typ != e1.typ) context.Error(app.pos, "++ can only be applied to sequences of the same type.");
+      app.typ = e0.typ;
+    case at@At(e0, e1) =>
+      ResolveExpr(e0, context, twoStateContext, false);
+      ResolveExpr(e1, context, twoStateContext, false);
+      if(! e0.typ.IsSeq) context.Error(at.pos, "LHS operand of @ must be sequence. (found: " + e0.typ.FullName + ").");
+      if(! e1.typ.IsInt) context.Error(at.pos, "RHS operand of @ must be an integer (found: " + e1.typ.FullName + ").");
+      if(e0.typ.IsSeq) at.typ = e0.typ.parameters(0) else at.typ = IntClass;
+    case drop@Drop(e0, e1) =>
+      ResolveExpr(e0, context, twoStateContext, false);
+      ResolveExpr(e1, context, twoStateContext, false);
+      if(! e0.typ.IsSeq) context.Error(drop.pos, "LHS operand of drop must be sequence. (found: " + e0.typ.FullName + ").");
+      if(! e1.typ.IsInt) context.Error(drop.pos, "RHS operand of drop must be an integer (found: " + e1.typ.FullName + ").");
+      drop.typ = e0.typ;
+    case take@Take(e0, e1) =>
+      ResolveExpr(e0, context, twoStateContext, false);
+      ResolveExpr(e1, context, twoStateContext, false);
+      if(! e0.typ.IsSeq) context.Error(take.pos, "LHS operand of take must be sequence. (found: " + e0.typ.FullName + ").");
+      if(! e1.typ.IsInt) context.Error(take.pos, "RHS operand of take must be an integer (found: " + e1.typ.FullName + ").");
+      take.typ = e0.typ;
+    case bin: BinaryExpr =>
+      ResolveExpr(bin.E0, context, twoStateContext, specContext && bin.isInstanceOf[And])
+      ResolveExpr(bin.E1, context, twoStateContext, specContext && (bin.isInstanceOf[And] || bin.isInstanceOf[Implies]))
+      if (bin.E0.typ != bin.ExpectedLhsType)
+        context.Error(bin.E0.pos, "incorrect type of " + bin.OpName + " LHS" +
+                      " (expected " + bin.ExpectedLhsType.FullName + 
+                      ", found " + bin.E0.typ.FullName + ")")
+      if (bin.E1.typ != bin.ExpectedRhsType)
+        context.Error(bin.E1.pos, "incorrect type of " + bin.OpName + " RHS" +
+                      " (expected " + bin.ExpectedRhsType.FullName + ", found " + bin.E1.typ.FullName + ")")
+      bin.typ = bin.ResultType
+    case q: Quantification =>
+      q.Is foreach { i => if(context.LookupVariable(i).isDefined) context.Error(q.pos, "The variable " + i + " hides another local.") }
+      ResolveExpr(q.Seq, context, twoStateContext, false);
+      if(! q.Seq.typ.IsSeq) 
+        context.Error(q.Seq.pos, "A quantification must range over a sequence. (found: " + q.Seq.typ.FullName + ").");
+      else {
+        val elementType = q.Seq.typ.parameters(0);
+        var bodyContext = context;
+        var bvariables = Nil: List[Variable];
+        q.Is foreach { i =>
+          val variable = new Variable(i, new Type(elementType));
+          bodyContext = bodyContext.AddVariable(variable);
+          bvariables = bvariables + variable;
+        }
+        ResolveExpr(q.E, bodyContext, twoStateContext, true);
+        if(! q.E.typ.IsBool) context.Error(q.E.pos, "Body of quantification must be a boolean. (found: " +  q.E.typ.FullName + ").");
+        q.variables = bvariables;
+      }
+      q.typ = BoolClass
+    case seq@EmptySeq(t) =>
+      ResolveType(t, context)
+      seq.typ = getSeqType(t.typ, context);
+    case seq@ExplicitSeq(es) =>
+      es foreach { e => ResolveExpr(e, context, twoStateContext, false) }
+      es match {
+        case Nil => seq.typ = getSeqType(IntClass, context);
+        case h :: t =>
+          t foreach { e => if(! (e.typ == h.typ)) context.Error(e.pos, "The elements of the sequence expression have different types.")};
+          seq.typ = getSeqType(h.typ, context);
+      }
+    case ran@Range(min, max) =>
+      ResolveExpr(min, context, twoStateContext, false);
+      if(! min.typ.IsInt) context.Error(min.pos, "The mininum of a range expression must be an integer (found: " + min.typ.FullName + ").");
+      ResolveExpr(max, context, twoStateContext, false);
+      if(! max.typ.IsInt) context.Error(max.pos, "The maximum of a range expression must be an integer (found: " + max.typ.FullName + ").");
+      ran.typ = getSeqType(IntClass, context);
+    case len@Length(e) =>
+      ResolveExpr(e, context, twoStateContext, false);
+      if(! e.typ.IsSeq) context.Error(len.pos, "The operand of a length expression must be sequence. (found: " + e.typ.FullName + ").");
+      len.typ = IntClass;
+    case ev@Eval(h, e) =>
+      if(inPredicate) context.Error(ev.pos, "eval cannot be used in monitor invariants or predicates")
+      h match {
+        case AcquireState(obj) => 
+          ResolveExpr(obj, context, twoStateContext, false)
+          if(! obj.typ.IsRef) context.Error(ev.pos, "The target of acquire must be a reference.");
+        case ReleaseState(obj) => ResolveExpr(obj, context, twoStateContext, false)
+          if(! obj.typ.IsRef) context.Error(ev.pos, "The target of acquire must be a reference.");
+        case c@CallState(token, obj, id, args) =>
+          ResolveExpr(token, context, twoStateContext, false);
+          if( ! token.typ.IsToken) context.Error(token.pos, "joinable is only applicable to tokens");
+          ResolveExpr(obj, context, false, false)
+          CheckNoGhost(obj, context)
+          args foreach { a => ResolveExpr(a, context, false, false); CheckNoGhost(a, context) }
+          // lookup method
+          var typ: Class = IntClass
+          obj.typ.LookupMember(id) match {
+            case None =>
+              context.Error(obj.pos, "call of undeclared member " + id + " in class " + obj.typ.FullName)
+            case Some(m: Method) =>
+              c.m = m
+              if (args.length != m.ins.length)
+                context.Error(obj.pos, "wrong number of actual in-parameters in call to " + obj.typ.FullName + "." + id +
+                          " (" + args.length + " instead of " + m.ins.length + ")")
+              else {
+                for((actual, formal) <- args zip m.ins){
+                  if(! canAssign(formal.t.typ, actual.typ))
+                   context.Error(actual.pos, "the type of the actual argument is not assignable to the formal parameter (expected: " + formal.t.FullName + ", found: " + actual.typ.FullName + ")")
+              }
+            }
+          case _ => context.Error(obj.pos, "call expression does not denote a method: " + obj.typ.FullName + "." + id)
+      }
+            
+          
+      }
+      ResolveExpr(e, context, false, specContext)
+      ev.typ = e.typ;
+  }
+
+  def LookupRunMethod(cl: Class, context: ProgramContext, op: String, pos: Position): Option[Method] = {
+    cl.LookupMember("run") match {
+      case None =>
+        context.Error(pos, "object given in " + op + " statement must be of a type with a parameter-less run method" +
+                      " (found type " + cl.id + ")")
+        None
+      case Some(m: Method) =>
+        m.spec foreach {
+          case Precondition(e) => CheckRunSpecification(e, context, true)
+          case Postcondition(e) => CheckRunSpecification(e, context, false)
+          case lc: LockChange => context.Error(lc.pos, "lockchange is not allowed in specification of run method")
+        }
+        if(0<m.ins.length || 0<m.outs.length) {
+          context.Error(pos, "object given in " + op + " statement must be of a type with a parameter-less run method" +
+                      " (found " + m.ins.length + " in-parameters and " + m.outs.length + " out-parameters)"); None
+        } else
+          Some(m)
+      case _ =>
+        context.Error(pos, "object given in " + op + " statement must be of a type with a parameter-less run method" +
+                      " (found non-method member)")
+        None
+    }
+  }
+
+  // assumes that lhs and rhs are resolved
+  def canAssign(lhs: Class, rhs: Class): Boolean = {
+    (lhs, rhs) match {
+      case (TokenClass(c1, m1), TokenClass(c2, m2)) => c1.id.equals(c2.id) && m1.equals(m2)
+      case (TokenClass(c1, m1), _) => false
+      case (_, TokenClass(c2, m2)) => false
+      case (lhs, rhs) => lhs == rhs || (lhs.IsRef && rhs.IsNull)
+    }
+  }
+
+  def CheckNoGhost(expr: RValue, context: ProgramContext): Unit = {
+    def specOk(e: RValue): Unit = { 
+      e match {
+        case ve: VariableExpr =>
+          if (ve.v != null && ve.v.IsGhost) context.Error(ve.pos, "ghost variable not allowed here")
+        case fs@ MemberAccess(e, id) =>
+          if (!fs.isPredicate && fs.f != null && fs.f.IsGhost) context.Error(fs.pos, "ghost fields not allowed here")
+          CheckNoGhost(e, context)
+        case a: Assigned =>
+          if (a.v != null && a.v.IsGhost) context.Error(a.pos, "ghost variable not allowed here")
+        case _ => visitE(e, specOk)
+      }
+    }
+    specOk(expr)
+  }
+
+  def CheckNoImmutableGhosts(expr: RValue, context: ProgramContext): Unit = {
+    def specOk(e: RValue): Unit = { 
+      e match {
+        case ve: VariableExpr =>
+          if (ve.v != null && ve.v.IsGhost && ve.v.IsImmutable) context.Error(ve.pos, "ghost const not allowed here")
+        case a: Assigned =>
+          if (a.v != null && a.v.IsGhost && a.v.IsImmutable) context.Error(a.pos, "ghost const not allowed here")
+        case _ => visitE(e, specOk)
+      }
+    }
+    specOk(expr)
+  }
+
+  def CheckRunSpecification(e: Expression, context: ProgramContext, allowMaxLock: boolean): unit = e match {
+    case _:MaxLockLiteral =>
+      if (!allowMaxLock) context.Error(e.pos, "specification of run method is not allowed to mention maxlock here")
+    case _:Literal =>
+    case _:VariableExpr =>
+    case _:ThisExpr =>
+    case _:Result =>
+    case MemberAccess(e, id) =>
+      CheckRunSpecification(e, context, false)
+    case Access(e, perm) =>
+      CheckRunSpecification(e, context, false)
+      perm match { case None => case Some(perm) => CheckRunSpecification(perm, context, false) }
+    case RdAccess(e, perm) =>
+      CheckRunSpecification(e, context, false)
+      perm match { case Some(Some(p)) => CheckRunSpecification(p, context, false) case _ => }
+    case AccessAll(obj, perm) =>
+      CheckRunSpecification(obj, context, false)
+      perm match { case None => case Some(perm) => CheckRunSpecification(perm, context, false) }
+    case RdAccessAll(obj, perm) =>
+      CheckRunSpecification(obj, context, false)
+      perm match { case Some(Some(p)) => CheckRunSpecification(p, context, false) case _ => }
+    case Holds(e) =>
+      context.Error(e.pos, "holds is not allowed in specification of run method")
+    case RdHolds(e) =>
+      context.Error(e.pos, "rd holds is not allowed in specification of run method")
+    case _:Assigned =>
+    case Old(e) =>
+      CheckRunSpecification(e, context, false)  // OLD occurs only in postconditions and monitor invariants, where maxlock is not allowed anyhow
+    case IfThenElse(con, then, els) =>
+      CheckRunSpecification(con, context, false);
+      CheckRunSpecification(con, context, allowMaxLock); 
+      CheckRunSpecification(con, context, allowMaxLock); 
+    case Not(e) =>
+      CheckRunSpecification(e, context, false)
+    case FunctionApplication(obj, id, args) =>
+      obj :: args foreach { arg => CheckRunSpecification(arg, context, false)} 
+    case Unfolding(pred, e) =>
+      CheckRunSpecification(pred, context, true);
+      CheckRunSpecification(e, context, allowMaxLock);
+    case LockBelow(e0,e1) =>
+      CheckRunSpecification(e0, context, allowMaxLock)
+      CheckRunSpecification(e1, context, false)
+    case And(e0,e1) =>
+      CheckRunSpecification(e0, context, allowMaxLock)
+      CheckRunSpecification(e1, context, allowMaxLock)
+    case Implies(e0,e1) =>
+      CheckRunSpecification(e0, context, false)
+      CheckRunSpecification(e1, context, allowMaxLock)
+    case bin: BinaryExpr =>
+      CheckRunSpecification(bin.E0, context, false)
+      CheckRunSpecification(bin.E1, context, false)
+    case q: Quantification =>
+      CheckRunSpecification(q.Seq, context, false)
+      CheckRunSpecification(q.E, context, true)
+    case Length(e) =>
+      CheckRunSpecification(e, context, false);
+    case ExplicitSeq(es) =>
+      es foreach { e => CheckRunSpecification(e, context, false) }
+    case Range(min, max) =>
+      CheckRunSpecification(min, context, false)
+      CheckRunSpecification(max, context, false)
+    case Eval(h, e) =>
+      h match {
+        case AcquireState(obj) =>  CheckRunSpecification(obj, context, false);
+        case ReleaseState(obj) =>  CheckRunSpecification(obj, context, false);
+        case CallState(token, obj, id, args) => CheckRunSpecification(token, context, false); CheckRunSpecification(obj, context, false);  args foreach { a: Expression => CheckRunSpecification(a, context, false)};
+      }
+      CheckRunSpecification(e, context, allowMaxLock)
+  }
+
+  def visitE(expr: RValue, func: RValue => Unit): Unit = {
+    expr match {
+      case _:NewRhs =>
+      case e: Literal => ;
+      case _:ThisExpr => ;
+      case _:Result => ;
+      case e:VariableExpr => ;
+      case acc@MemberAccess(e,f) =>
+        func(e);
+      case Access(e, perm) =>
+        func(e); perm match { case Some(p) => func(p); case _ => ; }
+      case RdAccess(e, perm) =>
+        func(e); perm match { case Some(Some(p)) => func(p); case _ => ; }
+      case AccessAll(obj, perm) =>
+        func(obj); perm match { case Some(p) => func(p); case _ => ; }
+      case RdAccessAll(obj, perm) =>
+        func(obj); perm match { case Some(Some(p)) => func(p); case _ => ; }
+      case Holds(e) => func(e);
+      case RdHolds(e) => func(e);
+      case e: Assigned => e
+      case Old(e) => func(e);
+      case IfThenElse(con, then, els) => func(con); func(then); func(els);
+      case Not(e) => func(e);
+      case funapp@FunctionApplication(obj, id, args) =>
+        func(obj); args foreach { arg => func(arg) };
+      case Unfolding(pred, e) =>
+        func(pred); func(e); 
+      case Iff(e0,e1) => func(e0); func(e1);
+      case Implies(e0,e1) => func(e0); func(e1);
+      case And(e0,e1) =>func(e0); func(e1);
+      case Or(e0,e1) => func(e0); func(e1);
+      case Eq(e0,e1) => func(e0); func(e1);
+      case Neq(e0,e1) => func(e0); func(e1);
+      case Less(e0,e1) => func(e0); func(e1);
+      case AtMost(e0,e1) => func(e0); func(e1);
+      case AtLeast(e0,e1) => func(e0); func(e1);
+      case Greater(e0,e1) => func(e0); func(e1);
+      case LockBelow(e0,e1) => func(e0); func(e1);
+      case Plus(e0,e1) => func(e0); func(e1);
+      case Minus(e0,e1) => func(e0); func(e1);
+      case Times(e0,e1) => func(e0); func(e1);
+      case Div(e0,e1) => func(e0); func(e1);
+      case Mod(e0,e1) => func(e0); func(e1);
+      case Forall(i, seq, e) => func(seq); func(e);
+      case ExplicitSeq(es) =>
+        es foreach { e => func(e) }
+      case Range(min, max) =>
+        func(min); func(max);
+      case Append(e0, e1) =>
+        func(e0); func(e1);
+      case at@At(e0, e1) =>
+        func(e0); func(e1);
+      case Drop(e0, e1) =>
+        func(e0); func(e1);
+      case Take(e0, e1) =>
+        func(e0); func(e1);
+      case Length(e) =>
+        func(e)
+      case Eval(h, e) =>
+        h match {
+          case AcquireState(obj) => func(obj);
+          case ReleaseState(obj) => func(obj);
+          case CallState(token, obj, id, args) => func(token); func(obj); args foreach {a : Expression => func(a)};
+        }
+        func(e);
+    }
+  }
+}
diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
new file mode 100644
index 00000000..9ec41448
--- /dev/null
+++ b/Chalice/src/Translator.scala
@@ -0,0 +1,2260 @@
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+import scala.util.parsing.input.Position
+
+import Boogie.Proc, Boogie.NamedType, Boogie.NewBVar, Boogie.Havoc, Boogie.Stmt, Boogie.Const,
+       Boogie.Decl, Boogie.Expr, Boogie.FunctionApp, Boogie.Axiom, Boogie.BVar, Boogie.BType,
+       Boogie.VarExpr, Boogie.IndexedType, Boogie.Comment, Boogie.MapUpdate, Boogie.MapSelect,
+       Boogie.If;
+
+case class ErrorMessage(pos: Position, message: String)
+
+object TranslationOptions {
+  // note: the initial values should match those Chalice.scala
+
+  var defaults = 0: int;
+  var autoFold = false: Boolean;
+  var checkLeaks = false: Boolean;
+  var autoMagic = false: Boolean;
+}
+
+class Translator {
+  import TranslationHelper._;
+  import TranslationOptions._;
+  var currentClass = null: Class;
+  var currentMethod = null: Method;
+  var modules = Nil: List[String]
+  var etran = new ExpressionTranslator(null);
+
+  def translateProgram(classes: List[Class]): List[Decl] = {
+    classes flatMap { translateClass(_) }
+  }
+
+  def translateClass(cl: Class): List[Decl] = {
+    currentClass = cl;
+    etran = new ExpressionTranslator(cl);
+    var declarations = Nil: List[Decl]
+    // add module (if no added yet)
+    if(modules forall {mname => ! mname.equals(cl.module)}) {
+      declarations = declarations + Const(ModuleName(cl), true, ModuleType);
+      modules = modules + cl.module;
+    }
+    // add class name
+    declarations = declarations + Const(cl.id + "#t", true, TypeName);
+    // translate monitor invariant
+    declarations = declarations ::: translateMonitorInvariant(cl.Invariants);
+    // translate each member
+    for(member <- cl.members) {
+      declarations = declarations ::: translateMember(member);
+    }
+    declarations
+  }
+
+  /**********************************************************************
+  *****************            MEMBERS                  *****************
+  **********************************************************************/
+
+  def translateMember(member: Member): List[Decl] = {
+    member match {
+      case f: Field =>
+        translateField(f)
+      case m: Method =>
+        translateMethod(m)
+      case f: Function => 
+        translateFunction(f)
+      case pred: Predicate =>
+        translatePredicate(pred)
+      case inv: MonitorInvariant =>
+        Nil // already dealt with before
+    }
+  }
+
+  def translateMonitorInvariant(invs: List[MonitorInvariant]): List[Decl] = {
+    val (m1V, m1) = NewBVar("m1", tmask, true); val (h1V, h1) = NewBVar("h1", theap, true);
+    val (m2V, m2) = NewBVar("m2", tmask, true); val (h2V, h2) = NewBVar("h2", theap, true);
+    val (lkV, lk) = NewBVar("lk", tref, true);
+    val oldTranslator = new ExpressionTranslator(List(h2, m2), List(h1, m1), currentClass);
+    Proc(currentClass.id + "$monitorinvariant$checkDefinedness",
+      List(NewBVarWhere("this", new Type(currentClass))),
+      Nil,
+      GlobalNames,
+      DefaultPrecondition(),
+        BLocal(h1V) :: BLocal(m1V) ::BLocal(h2V) :: BLocal(m2V) :: BLocal(lkV) ::
+        bassume(wf(h1, m1)) :: bassume(wf(h2, m2)) ::
+        (oldTranslator.Mask := ZeroMask) ::
+        oldTranslator.Inhale(invs map { mi => mi.e}, "monitor invariant", false) :::
+        (etran.Mask := ZeroMask) :: 
+        Havoc(etran.Heap) ::
+        // check that invariant is well-defined
+        etran.WhereOldIs(h2, m2).Inhale(invs map { mi => mi.e}, "monitor invariant", true) :::
+        (if (!checkLeaks || invs.length == 0) Nil else
+          // check that there are no loops among .mu permissions in monitors
+          // !CanWrite[this,mu]
+          bassert(!etran.CanWrite(VarExpr("this"), "mu"), invs(0).pos, "Monitor invariant is not allowed to hold write permission to this.mu") ::
+          // (forall lk :: lk != null && lk != this && CanRead[lk,mu] ==>
+          //   CanRead[this,mu] && Heap[this,mu] << Heap[lk,mu])
+          bassert(
+            (lk !=@ NullLiteral() && lk !=@ VarExpr("this") && etran.CanRead(lk, "mu")) ==>
+            (etran.CanRead(VarExpr("this"), "mu") &&
+             new FunctionApp("MuBelow", etran.Heap.select(VarExpr("this"), "mu"), etran.Heap.select(lk, "mu"))),
+            invs(0).pos,
+            "Monitor invariant can hold permission of other o.mu field only this.mu if this.mu<<o.mu")
+        ) :::
+        //check that invariant is reflexive
+        etran.UseCurrentAsOld().Exhale(invs map {mi => (mi.e, ErrorMessage(mi.pos, "Monitor invariant might not be reflexive."))}, "invariant reflexive?", false))
+  }
+
+  def translateField(f: Field): List[Decl] = {
+    Const(f.FullName, true, FieldType(f.typ)) ::
+    Axiom(NonPredicateField(f.FullName))
+  }
+
+  def translateFunction(f: Function): List[Decl] = {
+    val myresult = BVar("result", Boogie.ClassType(f.out.typ));
+    etran.checkTermination = true;
+    val checkBody = isDefined(f.definition);
+    etran.checkTermination = false;
+    // BoogiePL function that represents the dafny function
+    Boogie.Function(functionName(f), BVar("heap", theap) :: Boogie.BVar("mask", tmask) :: Boogie.BVar("this", tref) :: (f.ins map Variable2BVar), new Boogie.BVar("$myresult", Boogie.ClassType(f.out.typ))) ::
+    // check definedness of the function's precondition and body
+    Proc(f.FullName + "$checkDefinedness", 
+      NewBVarWhere("this", new Type(currentClass)) :: (f.ins map {i => Variable2BVarWhere(i)}),
+      Nil,
+      GlobalNames,
+      DefaultPrecondition(),
+      DefinePreInitialState :::
+      // check definedness of the precondition
+      InhaleWithChecking(Preconditions(f.spec) map { p => (if(0<defaults) UnfoldPredicatesWithReceiverThis(p) else p)}, "precondition") :::
+      bassume(CurrentModule ==@ VarExpr(ModuleName(currentClass))) :: // verify the body assuming that you are in the module
+      // check definedness of function body
+      checkBody :::
+      BLocal(myresult) ::
+      (Boogie.VarExpr("result") := etran.Tr(f.definition)) ::
+      // check that postcondition holds
+      ExhaleWithChecking(Postconditions(f.spec) map { post => ((if(0<defaults) UnfoldPredicatesWithReceiverThis(post) else post), ErrorMessage(f.pos, "Postcondition at " + post.pos + " might not hold."))}, "function postcondition")) :: 
+      // definition axiom
+      definitionAxiom(f) ::
+      // framing axiom (+ frame function)
+      framingAxiom(f) :::
+      // postcondition axiom(s)
+      postconditionAxiom(f)
+  }
+
+  def definitionAxiom(f: Function): Axiom = {
+    val version = Version(Preconditions(f.spec).foldLeft(BoolLiteral(true): Expression)({ (a, b) => And(a, b) }), etran);
+    val inArgs = (f.ins map {i => Boogie.VarExpr(i.UniqueName)});
+    val frameFunctionName = "##" + f.FullName;
+    
+    /* axiom (forall h: HeapType, m: MaskType, this: ref, x_1: t_1, ..., x_n: t_n ::
+         wf(h, m) && CurrentModule == module#C ==> #C.f(h, m, this, x_1, ..., x_n) == tr(body))
+    */
+    val args = VarExpr("this") :: inArgs;
+    val applyF = f.apply(List(etran.Heap, etran.Mask) ::: args);
+    Axiom(new Boogie.Forall(
+      BVar(HeapName, theap) :: BVar(MaskName, tmask) :: BVar("this", tref) :: (f.ins map Variable2BVar),
+      List(applyF),
+        (wf(Heap, Mask) && (CurrentModule ==@ ModuleName(currentClass)))
+        ==>
+        (applyF ==@ etran.Tr(f.definition)))
+    )
+  }
+
+  def framingAxiom(f: Function): List[Decl] = {
+    /* function ##C.f(state, ref, t_1, ..., t_n) returns (t);       
+       axiom (forall h: HeapType, m: MaskType, this: ref, x_1: t_1, ..., x_n: t_n ::
+          wf(h, m) && IsGoodState(version) ==> #C.f(h, m, this, x_1, ..., x_n) ==  ##C.f(version, this, x_1, ..., x_n))
+    */
+    val version = Version(Preconditions(f.spec).foldLeft(BoolLiteral(true): Expression)({ (a, b) => And(a, b) }), etran);
+    val inArgs = (f.ins map {i => Boogie.VarExpr(i.UniqueName)});
+    val frameFunctionName = "##" + f.FullName;
+
+    val args = VarExpr("this") :: inArgs;
+    val applyF = f.apply(List(etran.Heap, etran.Mask) ::: args);
+    val applyFrameFunction = FunctionApp(frameFunctionName, version :: args);
+    Boogie.Function("##" + f.FullName, Boogie.BVar("state", theap) :: Boogie.BVar("this", tref) :: (f.ins map Variable2BVar), new BVar("$myresult", f.out)) ::
+    Axiom(new Boogie.Forall(
+      BVar(HeapName, theap) :: BVar(MaskName, tmask) :: BVar("this", tref) :: (f.ins map Variable2BVar),
+      List(applyF),
+        (wf(Heap, Mask) && IsGoodState(version) && CanAssumeFunctionDefs)
+        ==>
+        (applyF ==@ applyFrameFunction))
+    )
+  }
+
+  def postconditionAxiom(f: Function): List[Decl] = {
+    /* function ##C.f(state, ref, t_1, ..., t_n) returns (t);       
+       axiom (forall h: HeapType, m: MaskType, this: ref, x_1: t_1, ..., x_n: t_n ::
+          wf(h, m) && CanAssumeFunctionDefs ==> Q[#C.f(h, m, this, x_1, ..., x_n)/result]
+    */
+    val version = Version(Preconditions(f.spec).foldLeft(BoolLiteral(true): Expression)({ (a, b) => And(a, b) }), etran);
+    val inArgs = (f.ins map {i => Boogie.VarExpr(i.UniqueName)});
+    val myresult = Boogie.BVar("result", Boogie.ClassType(f.out.typ));
+    val args = VarExpr("this") :: inArgs;
+    val applyF = f.apply(List(Heap, Mask) ::: args)
+    //postcondition axioms
+    (Postconditions(f.spec) map { post : Expression =>
+      Axiom(new Boogie.Forall(
+        BVar(HeapName, theap) :: BVar(MaskName, tmask) :: BVar("this", tref) :: (f.ins map Variable2BVar),
+        List(applyF),
+        (wf(Heap, Mask) && CanAssumeFunctionDefs)
+          ==>
+        etran.Tr(SubstResult(post, f.apply(ExplicitThisExpr(), f.ins map { arg => new VariableExpr(arg) })))
+        ))
+     })
+  }
+
+  def translatePredicate(pred: Predicate): List[Decl] = {
+    // const unique class.name: HeapType;
+    Const(pred.FullName, true, FieldType(theap)) ::
+    // axiom PredicateField(f);
+    Axiom(PredicateField(pred.FullName)) ::
+    // check definedness of predicate body
+    Proc(pred.FullName + "$checkDefinedness",
+      List(NewBVarWhere("this", new Type(currentClass))),
+      Nil,
+      GlobalNames,
+      DefaultPrecondition(),
+      DefinePreInitialState :::
+      InhaleWithChecking(List(DefinitionOf(pred)), "predicate definition"))
+  }
+
+  def translateMethod(method: Method): List[Decl] = {
+    // check definedness of the method contract
+    Proc(method.FullName + "$checkDefinedness", 
+      NewBVarWhere("this", new Type(currentClass)) :: (method.ins map {i => Variable2BVarWhere(i)}),
+      method.outs map {i => Variable2BVarWhere(i)},
+      GlobalNames,
+      DefaultPrecondition(),
+        DefinePreInitialState :::
+        bassume(CanAssumeFunctionDefs) ::
+        // check precondition
+        InhaleWithChecking(Preconditions(method.spec), "precondition") :::
+        DefineInitialState :::
+        (Mask := ZeroMask) :: 
+        Havoc(etran.Heap) ::
+        // check postcondition
+        InhaleWithChecking(Postconditions(method.spec), "postcondition") :::
+        // check lockchange
+        (LockChanges(method.spec) flatMap { lc => isDefined(lc)})) ::
+    // check that method body satisfies the method contract
+    Proc(method.FullName,
+      NewBVarWhere("this", new Type(currentClass)) :: (method.ins map {i => Variable2BVarWhere(i)}),
+      method.outs map {i => Variable2BVarWhere(i)},
+      GlobalNames,
+      DefaultPrecondition(),
+        bassume(CurrentModule ==@ Boogie.VarExpr(ModuleName(currentClass))) ::
+        bassume(CanAssumeFunctionDefs) ::
+        DefinePreInitialState :::
+        Inhale(Preconditions(method.spec) map { p => (if(0<defaults) UnfoldPredicatesWithReceiverThis(p) else p)}, "precondition") :::
+        DefineInitialState :::
+        translateStatements(method.body) :::
+        Exhale(Postconditions(method.spec) map { p => ((if(0<defaults) UnfoldPredicatesWithReceiverThis(p) else p), ErrorMessage(method.pos, "The postcondition at " + p.pos + " might not hold."))}, "postcondition") :::
+        (if(checkLeaks) isLeaking(method.pos, "Method " + method.FullName + " might leak refereces.") else Nil) :::
+        bassert(LockFrame(LockChanges(method.spec), etran), method.pos, "Method might lock/unlock more than allowed.")) :: Nil
+  }
+
+  def DefaultPrecondition() : List[String] = 
+  {
+    List("requires this!=null;", "free requires wf(Heap, Mask);")
+  }
+  def DefinePreInitialState = {
+    Comment("define pre-initial state") ::
+    (etran.Mask := ZeroMask)
+  }
+  def DefineInitialState = {
+    Comment("define initial state") ::
+    bassume(etran.Heap ==@ Boogie.Old(etran.Heap)) ::
+    bassume(etran.Mask ==@ Boogie.Old(etran.Mask))
+  }
+
+  /**********************************************************************
+  *****************           STATEMENTS                *****************
+  **********************************************************************/
+  def translateStatements(statements: List[Statement]): List[Stmt] = {
+    statements flatMap translateStatement
+  }
+
+  def translateStatement(s: Statement): List[Stmt] = {
+    s match {
+      case Assert(e) =>
+        val newGlobals = etran.FreshGlobals("assert");
+        val tmpHeap = Boogie.NewBVar(HeapName, theap, true);
+        val tmpMask = Boogie.NewBVar(MaskName, tmask, true); 
+        val tmpTranslator = new ExpressionTranslator(List(tmpHeap._1.id, tmpMask._1.id), currentClass);
+        Comment("assert") ::
+        // exhale e in a copy of the heap/mask
+        BLocal(tmpHeap._1) :: (tmpHeap._2 := Heap) ::
+        BLocal(tmpMask._1) :: (tmpMask._2 := Mask) ::
+        tmpTranslator.Exhale(List((e, ErrorMessage(s.pos, "Assertion might not hold."))), "assert", true)
+      case Assume(e) =>
+        Comment("assume") ::
+        isDefined(e) :::
+        bassume(e)
+      case BlockStmt(ss) =>
+        translateStatements(ss)
+      case IfStmt(guard, then, els) =>
+        val tt = translateStatement(then)
+        val et = els match {
+          case None => Nil
+          case Some(els) => translateStatement(els) }
+        Comment("if") ::
+        isDefined(guard) :::
+        Boogie.If(guard, tt, et)
+      case w: WhileStmt =>
+        translateWhile(w)
+      case Assign(lhs, rhs) =>
+        def assignOrAssumeEqual(r: Boogie.Expr): List[Boogie.Stmt] = {
+          if (lhs.v.isInstanceOf[ImmutableVariable]) {
+            // this must be a "ghost const"
+            val name = lhs.v.UniqueName
+            bassert(! VarExpr("assigned$" + name), lhs.pos, "Const variable can be assigned to only once.") ::
+            bassume(lhs ==@ r) ::
+            (VarExpr("assigned$" + name) := true)
+          } else {
+            lhs := r
+          }
+        }
+        Comment("assigment to " + lhs.id) ::
+        (rhs match {
+          case rhs@NewRhs(c, initialization) => // x := new C;
+            val (nw, ss) = translateAllocation(rhs.typ, initialization);
+            ss ::: assignOrAssumeEqual(new VarExpr(nw)) 
+          case rhs: Expression => // x := E;
+            isDefined(rhs) ::: assignOrAssumeEqual(rhs)
+        })
+      case FieldUpdate(lhs@MemberAccess(target, f), rhs) =>
+        val (statements, toStore : Expr) = 
+          (rhs match {
+            case rhs @ NewRhs(c, initialization) =>
+              // e.f := new C;
+              val (nw,ss) = translateAllocation(rhs.typ, initialization)
+              (ss, new VarExpr(nw))
+            case rhs : Expression =>
+              // e.f := E; 
+              (isDefined(rhs), TrExpr(rhs))
+           });
+        Comment("update field " + f) ::
+        isDefined(target) :::
+        bassert(CanWrite(target, lhs.f), s.pos, "Location might not be writable") ::
+        statements ::: etran.Heap.store(target, lhs.f, toStore) :: bassume(wf(Heap, Mask))
+      case lv @ LocalVar(id, t, const, ghost, rhs) =>
+        val bv = Variable2BVarWhere(lv.v)
+        val isAssignedVar = if (const) new Boogie.BVar("assigned$" + bv.id, Boogie.ClassType(BoolClass)) else null
+        Comment("local " + (if (ghost) "ghost " else "") + (if (const) "const " else "var ") + id) ::
+        BLocal(bv) :: 
+        { if (const)
+            // havoc x; var assigned$x: bool; assigned$x := false; 
+            Havoc(new Boogie.VarExpr(bv)) ::
+            BLocal(isAssignedVar) :: (new Boogie.VarExpr(isAssignedVar) := false)
+          else
+            List() } :::
+        { rhs match {
+          //update the local, provided a rhs was provided
+          case None => List()
+          case Some(rhs) => translateStatement(Assign(new VariableExpr(lv.v), rhs)) }}
+      case c: Call =>
+        translateCall(c)
+      case Install(obj, lowerBounds, upperBounds) =>
+        Comment("install") ::
+        isDefined(obj) :::
+        bassert(nonNull(obj), s.pos, "The target of the install statement might be null.") ::
+        bassert(isHeld(obj), s.pos, "The lock of the target of the install statement might not be held.") ::
+        // assert CanWrite(obj.mu); assume lowerbounds < obj.mu < upperBounds;
+        UpdateMu(obj, false, lowerBounds, upperBounds, ErrorMessage(s.pos, "Install might fail."))
+      case Share(obj, lowerBounds, upperBounds) =>
+        val (preShareMaskV, preShareMask) = Boogie.NewBVar("preShareMask", tmask, true)    
+        Comment("share") ::
+        // remember the mask immediately before the share
+        BLocal(preShareMaskV) :: Boogie.Assign(preShareMask, etran.Mask) ::
+        isDefined(obj) :::
+        bassert(nonNull(obj), s.pos, "The target of the share statement might be null.") ::
+        UpdateMu(obj, true, lowerBounds, upperBounds, ErrorMessage(s.pos, "Share might fail.")) :::
+        bassume(!isHeld(obj) && ! isRdHeld(obj)) :: // follows from o.mu==lockbottom
+        // no permission to o.held
+        etran.SetNoPermission(etran.Tr(obj), "held", etran.Mask) ::
+        // exhale the monitor invariant (using the current state as the old state)
+        ExhaleInvariants(obj, false, ErrorMessage(s.pos, "Monitor invariant might not hold."), etran.UseCurrentAsOld()) :::
+        // assume a seen state is the one right before the share
+        bassume(LastSeenHeap(etran.Heap.select(obj, "mu"), etran.Heap.select(obj, "held")) ==@ etran.Heap) ::
+        bassume(LastSeenMask(etran.Heap.select(obj, "mu"), etran.Heap.select(obj, "held")) ==@ preShareMask)
+      case Unshare(obj) =>
+        val (heldV, held) = Boogie.NewBVar("held", Boogie.NamedType("int"), true)
+        val o = TrExpr(obj)
+        Comment("unshare") ::
+        isDefined(obj) :::
+        bassert(nonNull(o), s.pos, "The target of the unshare statement might be null.") ::
+        bassert(CanWrite(o, "mu"), s.pos, "The mu field of the target of the unshare statement might not be writable.") ::
+        bassert(CanWrite(o, "held"), s.pos, "The held field of the target of the unshare statement might not be writable.") ::
+        bassert(isShared(o), s.pos, "The target of the unshare statement might not be shared.") ::
+        bassert(isHeld(o), s.pos, "The target of the unshare statement might not be locked by the current thread.") :: // locked or read-locked
+        etran.Heap.store(o, "mu", bLockBottom) ::
+        // havoc o.held where 0<=o.held 
+        BLocal(heldV) :: Boogie.Havoc(held) :: bassume(held <= 0) ::
+        etran.Heap.store(o, "held", held) ::
+        // set the permission of o.held to 0
+        etran.SetNoPermission(o, "held", etran.Mask) ::
+        // set o.rdheld to false
+        etran.Heap.store(o, "rdheld", false)
+      case Acquire(obj) =>
+        Comment("acquire") ::
+        isDefined(obj) :::
+        bassert(nonNull(TrExpr(obj)), s.pos, "The target of the acquire statement might be null.") ::
+        TrAcquire(s, obj)
+      case Release(obj) =>
+        Comment("release") ::
+        isDefined(obj) :::
+        bassert(nonNull(TrExpr(obj)), s.pos, "The target of the release statement might be null.") ::
+        TrRelease(s, obj)
+      case Lock(e, body, readonly) =>
+        val objV = new Variable("lock", new Type(e.typ))
+        val obj = new VariableExpr(objV)
+        val sname = if (readonly) "rd lock" else "lock"
+        val o = TrExpr(obj)
+        Comment(sname) ::
+        isDefined(e) :::
+        BLocal(Variable2BVar(objV)) :: (o := TrExpr(e)) ::
+        bassert(nonNull(o), s.pos, "The target of the " + sname + " statement might be null.") ::
+        { if (readonly) {
+            TrRdAcquire(s, obj) :::
+            translateStatement(body) :::
+            TrRdRelease(s, obj)
+          } else {
+            TrAcquire(s, obj) :::
+            translateStatement(body) :::
+            TrRelease(s, obj)
+          }
+        }
+      case RdAcquire(obj) =>
+        Comment("rd acquire") ::
+        isDefined(obj) :::
+        bassert(nonNull(TrExpr(obj)), s.pos, "The target of the read-acquire statement might be null.") ::
+        TrRdAcquire(s, obj)
+      case rdrelease@RdRelease(obj) =>
+        Comment("rd release") ::
+        isDefined(obj) :::
+        bassert(nonNull(TrExpr(obj)), obj.pos, "The target of the read-release statement might be null.") ::
+        TrRdRelease(s, obj)
+      case downgrade@Downgrade(obj) =>
+        val o = TrExpr(obj);
+        val prevHeapV = new Boogie.BVar("prevHeap", theap, true)
+        Comment("downgrade") ::
+        isDefined(obj) :::
+        bassert(nonNull(o), s.pos, "The target of the downgrade statement might be null.") ::
+        bassert(isHeld(o), s.pos, "The lock of the target of the downgrade statement might not be held by the current thread.") ::
+        bassert(! isRdHeld(o), s.pos, "The current thread might hold the read lock.") ::
+        ExhaleInvariants(obj, false, ErrorMessage(downgrade.pos, "Monitor invariant might not hold.")) :::
+        BLocal(prevHeapV) ::
+        InhaleInvariants(obj, true) :::
+        bassume(etran.Heap ==@ new Boogie.VarExpr(prevHeapV)) ::
+        etran.Heap.store(o, "rdheld", true)
+      case Free(obj) =>
+        val o = TrExpr(obj);
+        isDefined(obj) :::
+        bassert(nonNull(o), s.pos, "The target of the free statement might be null.") ::
+        (for (f <- obj.typ.Fields ++ RootClass.MentionableFields) yield
+          bassert(CanWrite(o, f.FullName), s.pos, "The field " + f.id + " of the target of the free statement might not be writable.")) :::
+        (for (f <- obj.typ.Fields ++ RootClass.MentionableFields) yield
+          etran.SetNoPermission(o, f.FullName, etran.Mask))
+        // probably need to havoc all the fields! Do we check enough?
+      case fold@Fold(acc@Access(pred@MemberAccess(e, f), fraction)) =>   
+        val o = TrExpr(e);
+        var definition = if(fraction.isDefined) FractionOf(SubstThis(DefinitionOf(pred.predicate), e), fraction.get) else SubstThis(DefinitionOf(pred.predicate), e);
+        Comment("fold") ::
+        isDefined(e) :::
+        bassert(nonNull(o), s.pos, "The target of the fold statement might be null.") ::
+        (if(fraction.isDefined) isDefined(fraction.get) ::: 
+          bassert(0 <= etran.Tr(fraction.get), s.pos, "Fraction might be negative.") :: 
+          bassert(etran.Tr(fraction.get) <= 100, s.pos, "Fraction might be larger than 100.") :: Nil else Nil) :::
+        // remove the definition from the current state, and replace by predicate itself
+        Exhale(List((definition, ErrorMessage(s.pos, "Fold might fail because the definition of " + pred.predicate.FullName + " does not hold."))), "fold") :::
+        Inhale(List(acc), "fold") :::
+        etran.Heap.store(o, pred.predicate.FullName, etran.Heap) :: // Is this necessary?      
+        bassume(wf(etran.Heap, etran.Mask))
+      case fld@Fold(acc@RdAccess(pred@MemberAccess(e, f), nbEpsilons)) =>
+        val o = TrExpr(e);
+        var (definition, checkEpsilons) = nbEpsilons match {
+          case None => (EpsilonsOf(SubstThis(pred.predicate.definition, e), IntLiteral(1)), Nil)
+          case Some(None) => throw new Exception("Not supported yet!");
+          case Some(Some(i)) => (EpsilonsOf(SubstThis(DefinitionOf(pred.predicate), e), i), isDefined(i) ::: bassert(Boogie.IntLiteral(0) <= i, s.pos, "Number of epsilons might be negative.") :: Nil)
+        }
+        Comment("fold") ::
+        isDefined(e) :::
+        bassert(nonNull(o), s.pos, "The target of the fold statement might be null.") ::
+        checkEpsilons :::
+        Exhale(List((definition, ErrorMessage(fld.pos, "Fold might fail because the definition of " + pred.predicate.FullName + " does not hold."))), "fold") :::
+        Inhale(List(acc), "fold") :::
+        etran.Heap.store(e, pred.predicate.FullName, etran.Heap) ::
+        bassume(wf(etran.Heap, etran.Mask))
+      case unfld@Unfold(acc@Access(pred@MemberAccess(e, f), fraction)) =>
+        val o = TrExpr(e);
+        var definition = if(fraction.isDefined) FractionOf(SubstThis(DefinitionOf(pred.predicate), e), fraction.get) else SubstThis(DefinitionOf(pred.predicate), e);
+        Comment("unfold") ::
+        isDefined(e) :::
+        bassert(nonNull(o), s.pos, "The target of the fold statement might be null.") ::
+        (if(fraction.isDefined) isDefined(fraction.get) ::: 
+          bassert(Boogie.IntLiteral(0) <= fraction.get, s.pos, "Fraction might be negative.") :: 
+          bassert(fraction.get <= 100, s.pos, "Fraction might be larger than 100.") :: Nil else Nil) :::
+        Exhale(List((acc, ErrorMessage(s.pos, "unfold might fail because the predicate " + pred.predicate.FullName + " does not hold."))), "unfold") :::
+        etran.InhaleFrom(List(definition), "unfold", false, etran.Heap.select(o, pred.predicate.FullName))
+      case unfld@Unfold(acc@RdAccess(pred@MemberAccess(e, f), nbEpsilons)) =>
+        val o = TrExpr(e);
+        var (definition, checkEpsilons) = nbEpsilons match {
+          case None => (EpsilonsOf(SubstThis(DefinitionOf(pred.predicate), e), IntLiteral(1)), Nil)
+          case Some(None) => throw new Exception("Not supported yet!");
+          case Some(Some(i)) => (EpsilonsOf(SubstThis(DefinitionOf(pred.predicate), e), i), isDefined(i) ::: bassert(Boogie.IntLiteral(0) <= i, s.pos, "Number of epsilons might be negative.") :: Nil)
+        }
+        Comment("unfold") ::
+        isDefined(e) :::
+        bassert(nonNull(o), s.pos, "The target of the fold statement might be null.") ::
+        checkEpsilons :::
+        Exhale(List((acc, ErrorMessage(s.pos, "Unold might fail because the predicate " + pred.predicate.FullName + " does not hold."))), "unfold") :::
+        etran.InhaleFrom(List(definition), "unfold", false, etran.Heap.select(o, pred.predicate.FullName))
+      case c@CallAsync(declaresLocal, token, obj, id, args) =>
+        val formalThisV = new Variable("this", new Type(c.m.Parent))
+        val formalThis = new VariableExpr(formalThisV)
+        val formalInsV = for (p <- c.m.ins) yield new Variable(p.id, p.t)
+        val formalIns = for (v <- formalInsV) yield new VariableExpr(v)
+        
+        val (tokenV,tokenId) = NewBVar("token", tref, true)
+        val (asyncStateV,asyncState) = NewBVar("asyncstate", tint, true)
+        val (preCallMaskV, preCallMask) = NewBVar("preCallMask", tmask, true)
+        val (preCallHeapV, preCallHeap) = NewBVar("preCallHeap", theap, true)
+        val (argsSeqV, argsSeq) = NewBVar("argsSeq", tArgSeq, true)
+        val argsSeqLength = 1 + args.length;
+        Comment("call " + id) ::
+        // declare the local variable, if needed
+        { if (c.local == null)
+            List[Stmt]()
+          else
+            List(BLocal(Variable2BVarWhere(c.local))) } :::
+        // remember the value of the heap and mask
+        BLocal(preCallMaskV) :: (preCallMask := etran.Mask) ::
+        BLocal(preCallHeapV) :: (preCallHeap := etran.Heap) ::
+        BLocal(argsSeqV) ::
+        // introduce formal parameters and pre-state globals
+        (for (v <- formalThisV :: formalInsV) yield BLocal(Variable2BVarWhere(v))) :::
+        // check definedness of arguments
+        isDefined(obj) :::
+        bassert(nonNull(obj), c.pos, "The target of the method call might be null.") ::
+        (args flatMap { e: Expression => isDefined(e)}) :::
+        // assign actual ins to formal ins
+        (formalThis := obj) ::
+        (for ((v,e) <- formalIns zip args) yield (v := e)) :::
+        // insert all arguments in the argument sequence
+        Boogie.AssignMap(argsSeq, 0, formalThis) ::
+        { var i = 1
+          for (v <- formalIns) yield { val r = Boogie.AssignMap(argsSeq, i, v); i += 1; r }
+        } :::
+        // exhale preconditions
+        Exhale(Preconditions(c.m.spec) map
+          (p => SubstThisAndVars(p, formalThis, c.m.ins, formalIns)) zip (Preconditions(c.m.spec) map { p => ErrorMessage(c.pos, "The precondition at " + p.pos + " might not hold.")}), "precondition") :::
+        // create a new token
+        BLocal(tokenV) :: Havoc(tokenId) :: bassume(nonNull(tokenId)) ::
+        // the following assumes help in proving that the token is fresh
+        bassume(Heap.select(tokenId, "joinable") ==@ 0) ::
+        bassume(new Boogie.MapSelect(Mask, tokenId, "joinable", "perm$N")==@ 0) ::
+        bassume(new Boogie.MapSelect(Mask, tokenId, "joinable", "perm$R")==@ 0) ::
+        etran.IncPermission(tokenId, "joinable", 100) ::
+        // create a fresh value for the joinable field
+        BLocal(asyncStateV) :: Boogie.Havoc(asyncState) :: bassume(asyncState !=@ 0) ::
+        etran.Heap.store(tokenId, "joinable", asyncState) ::
+        // assume the pre call state for the token is the state before inhaling the precondition
+        bassume(CallHeap(asyncState) ==@ preCallHeap) ::
+        bassume(CallMask(asyncState) ==@ preCallMask) ::
+        bassume(CallArgs(asyncState) ==@ argsSeq) ::
+        // assign the returned token to the variable
+        { if (token != null) List(token := tokenId) else List() }
+      case jn@JoinAsync(lhs, token) =>
+        val formalThisV = new Variable("this", new Type(jn.m.Parent))
+        val formalThis = new VariableExpr(formalThisV)
+        val formalInsV = for (p <- jn.m.ins) yield new Variable(p.id, p.t)
+        val formalIns = for (v <- formalInsV) yield new VariableExpr(v)
+        val formalOutsV = for (p <- jn.m.outs) yield new Variable(p.id, p.t)
+        val formalOuts = for (v <- formalOutsV) yield new VariableExpr(v)
+
+        val (argsSeqV, argsSeq) = NewBVar("argsSeq", tArgSeq, true)
+        val (preCallHeapV, preCallHeap) = NewBVar("preCallHeap", theap, true);
+        val (preCallMaskV, preCallMask) = NewBVar("preCallMask", tmask, true);
+        val preGlobals = List(preCallHeap, preCallMask);
+        val postEtran = new ExpressionTranslator(List(etran.Heap, etran.Mask), preGlobals, currentClass);
+        Comment("join async") :: 
+        // check that we did not join yet
+        bassert(CanWrite(token, "joinable"), jn.pos, "The joinable field might not be writable.") ::
+        bassert(etran.Heap.select(token, "joinable") !=@ 0, jn.pos, "The joinable field might not be true.") ::
+        // lookup token.joinable
+        BLocal(argsSeqV) :: (argsSeq := CallArgs(etran.Heap.select(token, "joinable"))) ::
+        // check that token is well-defined
+        isDefined(token) :::
+        // retrieve the call's pre-state from token.joinable
+        BLocal(preCallHeapV) :: (preCallHeap := CallHeap(etran.Heap.select(token, "joinable"))) :: 
+        BLocal(preCallMaskV) :: (preCallMask := CallMask(etran.Heap.select(token, "joinable"))) ::
+        // introduce locals for the out parameters
+        (for (v <- formalThisV :: formalInsV ::: formalOutsV) yield BLocal(Variable2BVarWhere(v))) :::
+        // initialize the in parameters
+        (formalThis := new MapSelect(argsSeq, 0)) ::
+        { var i = 1
+          (formalIns map { v => val r = (v := new MapSelect(argsSeq, i)); i += 1; r })
+        } :::
+        // havoc formal outs
+        (for (v <- formalOuts) yield Havoc(v)) :::
+        // set joinable to false
+        etran.Heap.store(token, "joinable", 0) ::
+        etran.SetNoPermission(token, "joinable", etran.Mask) ::
+        // inhale postcondition of the call
+        postEtran.Inhale(Postconditions(jn.m.spec) map
+                         { p => SubstThisAndVars(p, formalThis, jn.m.ins ++ jn.m.outs, formalIns ++ formalOuts)}, "postcondition", false) :::
+        // assign formal outs to actual outs
+        (for ((v,e) <- lhs zip formalOuts) yield (v :=e))
+    }
+  }
+  
+  def translateAllocation(cl: Class, initialization: List[Init]): (Boogie.BVar, List[Boogie.Stmt]) = {
+    val (nw, nwe) = NewBVar("nw", Boogie.ClassType(cl), true)
+    val (ttV,tt) = Boogie.NewTVar("T")
+    val f = new Boogie.BVar("f", FieldType(tt))
+    (nw,
+      Comment("new") ::
+      BLocal(nw) :: Havoc(nwe) ::
+      bassume(nonNull(nwe) && (dtype(nwe) ==@ TrType(cl))) ::
+      bassume(new Boogie.Forall(ttV, f, etran.HasNoPermission(nwe, f.id))) ::
+      // initial values of fields:
+      bassume(etran.Heap.select(nwe, "mu") ==@ bLockBottom) ::
+      bassume(etran.Heap.select(nwe, "held") <= 0) ::
+      bassume(etran.Heap.select(nwe, "rdheld") ==@ false) ::
+      // give access to user-defined fields and special fields:
+      (for (f <- cl.Fields ++ RootClass.MentionableFields) yield
+        etran.IncPermission(nwe, f.FullName, 100)) :::
+      // initialize fields according to the initialization
+      (initialization flatMap { init => isDefined(init.e) ::: etran.Heap.store(nwe, init.f.FullName, init.e) })
+    )
+  }
+
+  def TrAcquire(s: Statement, nonNullObj: Expression) = {
+    val o = TrExpr(nonNullObj);
+    val (lastAcquireVar, lastAcquire) = Boogie.NewBVar("lastAcquire", Boogie.ClassType(IntClass), true)
+    val (lastSeenHeldV, lastSeenHeld) = Boogie.NewBVar("lastSeenHeld", tint, true)
+    val (lastSeenMuV, lastSeenMu) = Boogie.NewBVar("lastSeenMu", tmu, true)
+    bassert(CanRead(o, "mu"), s.pos, "The mu field of the target of the acquire statement might not be readable.") ::
+    bassert(etran.MaxLockIsBelowX(etran.Heap.select(o,"mu")), s.pos, "The mu field of the target of the acquire statement might not be above maxlock.") ::
+    bassume(etran.Heap.select(o,"mu") !=@ bLockBottom) ::  // this isn't strictly necessary, it seems; but we might as well include it
+    // remember the state right before releasing
+    BLocal(lastSeenMuV) :: (lastSeenMu := etran.Heap.select(o, "mu")) ::
+    BLocal(lastSeenHeldV) :: Havoc(lastSeenHeld) :: (lastSeenHeld := etran.Heap.select(o, "held")) ::
+    bassume(! isHeld(o) && ! isRdHeld(o)) :: // this assume follows from the previous assert
+    // update the thread's locking state
+    BLocal(lastAcquireVar) :: Havoc(lastAcquire) :: bassume(0 < lastAcquire) ::
+    etran.SetFullPermission(o, "held") ::
+    etran.Heap.store(o, "held", lastAcquire) ::
+    InhaleInvariants(nonNullObj, false, etran.WhereOldIs(LastSeenHeap(lastSeenMu, lastSeenHeld), LastSeenMask(lastSeenMu, lastSeenHeld))) :::
+    // remember values of Heap/Mask globals (for proving history constraint at release)
+    bassume(AcquireHeap(lastAcquire) ==@ etran.Heap) ::
+    bassume(AcquireMask(lastAcquire) ==@ etran.Mask)
+  }
+  def TrRelease(s: Statement, nonNullObj: Expression) = {
+    val (heldV, held) = Boogie.NewBVar("held", tint, true) 
+    val (prevLmV, prevLm) = Boogie.NewBVar("prevLM", tref, true)
+    val (preReleaseMaskV, preReleaseMask) = NewBVar("preReleaseMask", tmask, true)
+    val (preReleaseHeapV, preReleaseHeap) = NewBVar("preReleaseHeap", theap, true)
+    val o = TrExpr(nonNullObj);
+    BLocal(preReleaseMaskV) :: (preReleaseMask := etran.Mask) ::
+    BLocal(preReleaseHeapV) :: (preReleaseHeap := etran.Heap) ::
+    bassert(CanWrite(o, "held"), s.pos, "The held field of the target of the release statement might not be writable.") ::
+    bassert(isHeld(o), s.pos, "The target of the release statement might be not be locked by the current thread.") ::
+    bassert(!isRdHeld(o), s.pos, "Release might fail because the current thread might hold the read lock.") ::
+    ExhaleInvariants(nonNullObj, false, ErrorMessage(s.pos, "Monitor invariant might hot hold."), etran.WhereOldIs(AcquireHeap(etran.Heap.select(o, "held")), AcquireMask(etran.Heap.select(o, "held")))) :::
+    // havoc o.held where 0<=o.held 
+    BLocal(heldV) :: Havoc(held) :: bassume(held <= 0) ::
+    etran.Heap.store(o, "held", held) ::
+    etran.SetNoPermission(o, "held", etran.Mask) ::
+    // assume a seen state is the one right before the share
+    bassume(LastSeenHeap(etran.Heap.select(o, "mu"), held) ==@ preReleaseHeap) ::
+    bassume(LastSeenMask(etran.Heap.select(o, "mu"), held) ==@ preReleaseMask)
+  }
+  def TrRdAcquire(s: Statement, nonNullObj: Expression) = {
+    val (heldV, held) = Boogie.NewBVar("held", tint, true)
+    val o = TrExpr(nonNullObj)
+    bassert(CanRead(o, "mu"), s.pos, "The mu field of the target of the read-acquire statement might not be readable.") ::
+    bassert(etran.MaxLockIsBelowX(etran.Heap.select(o, "mu")), s.pos, "The mu field of the target of the read-acquire statement might not be above maxlock.") ::
+    bassume(etran.Heap.select(o,"mu") !=@ bLockBottom) ::  // this isn't strictly necessary, it seems; but we might as well include it
+    bassume(! isHeld(o) && ! isRdHeld(o)) ::
+    BLocal(heldV) :: Havoc(held) :: bassume(held <= 0) ::
+    etran.Heap.store(o, "held", held) ::
+    etran.Heap.store(o, "rdheld", true) ::
+    InhaleInvariants(nonNullObj, true)
+  }
+  def TrRdRelease(s: Statement, nonNullObj: Expression) = {
+    val (heldV, held) = Boogie.NewBVar("held", tint, true)
+    val o = TrExpr(nonNullObj);
+    bassert(isRdHeld(o), s.pos, "The current thread might not hold the read-lock of the object being released.") ::
+    ExhaleInvariants(nonNullObj, true, ErrorMessage(s.pos, "Monitor invariant might not hold.")) :::
+    BLocal(heldV) :: Havoc(held) :: bassume(held <= 0) ::
+    etran.Heap.store(o, "held", held) ::
+    etran.Heap.store(o, "rdheld", false)
+  }
+
+  def translateCall(c: Call): List[Stmt] = {
+    val obj = c.obj;
+    val lhs = c.lhs;
+    val id = c.id;
+    val args = c.args;
+    val formalThisV = new Variable("this", new Type(c.m.Parent))
+    val formalThis = new VariableExpr(formalThisV)
+    val formalInsV = for (p <- c.m.ins) yield new Variable(p.id, p.t)
+    val formalIns = for (v <- formalInsV) yield new VariableExpr(v)
+    val formalOutsV = for (p <- c.m.outs) yield new Variable(p.id, p.t)
+    val formalOuts = for (v <- formalOutsV) yield new VariableExpr(v)
+    val preGlobals = etran.FreshGlobals("call")
+    val postEtran = etran.FromPreGlobals(preGlobals)
+    Comment("call " + id) ::
+    // introduce formal parameters and pre-state globals
+    (for (v <- formalThisV :: formalInsV ::: formalOutsV) yield BLocal(Variable2BVarWhere(v))) :::
+    (for (v <- preGlobals) yield BLocal(v)) :::
+    // remember values of globals
+    (for ((o,g) <- preGlobals zip etran.Globals) yield (new Boogie.VarExpr(o) := g)) :::
+    // check definedness of arguments
+    isDefined(obj) :::
+    bassert(nonNull(obj), c.pos, "The target of the method call might be null.") ::
+    (args flatMap { e: Expression => isDefined(e)}) :::
+    // assign actual ins to formal ins
+    (formalThis := obj) ::
+    (for ((v,e) <- formalIns zip args) yield (v := e)) :::
+    // exhale preconditions
+    Exhale(Preconditions(c.m.spec) map
+          (p => SubstThisAndVars(p, formalThis, c.m.ins, formalIns)) zip (Preconditions(c.m.spec) map { p => ErrorMessage(c.pos, "The precondition at " + p.pos + " might not hold.")}), "precondition") :::
+    // havoc formal outs
+    (for (v <- formalOuts) yield Havoc(v)) :::
+    // havoc lockchanges
+    LockHavoc(for (e <- LockChanges(c.m.spec) map (p => SubstThisAndVars(p, formalThis, c.m.ins, formalIns))) yield etran.Tr(e), postEtran) :::
+    // inhale postconditions (using the state before the call as the "old" state)
+    postEtran.Inhale(Postconditions(c.m.spec) map
+                     (p => SubstThisAndVars(p, formalThis, c.m.ins ++ c.m.outs, formalIns ++ formalOuts)) , "postcondition", false) :::
+    // assign formal outs to actual outs
+    (for ((v,e) <- lhs zip formalOuts) yield (v :=e))
+  }
+
+  def translateWhile(w: WhileStmt): List[Stmt] = {
+    val guard = w.guard;
+    val invs = w.invs;
+    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,
+                                             for (v <- saveLocalsV) yield new VariableExpr(v)))
+    val lkchIterStart = lkch map (e => SubstVars(e, w.LoopTargetsList,
+                                                   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))
+    val newLocks = lkch map (e => loopEtran.Tr(e));
+    Comment("while") ::
+    // save globals
+    (for (v <- preLoopGlobals) yield BLocal(v)) :::
+    (loopEtran.oldEtran.Heap := loopEtran.Heap) ::
+    (loopEtran.oldEtran.Mask := loopEtran.Mask) ::  // oldMask is not actually used below
+    // 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") :::
+    // 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))) :::
+    // havoc local-variable loop targets
+    (w.LoopTargets :\ List[Boogie.Stmt]()) ( (v,vars) => (v match {
+      case v: ImmutableVariable => Boogie.Havoc(Boogie.VarExpr("assigned$" + v.id))
+      case _ => Boogie.Havoc(Boogie.VarExpr(v.UniqueName)) }) :: vars) :::
+    Boogie.If(null,
+    // 1. CHECK  DEFINEDNESS OF INVARIANT
+      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) ::
+      InhaleWithChecking(invs, "loop invariant definedness") :::
+      bassume(false)
+    , Boogie.If(null,
+    // 2. CHECK LOOP BODY
+      // Renew Heap and Mask: set Mask to ZeroMask, and havoc Heap everywhere except
+      // at {old(local),local}.{held,rdheld}
+      Havoc(etran.Heap) :: (etran.Mask := ZeroMask) ::
+      Inhale(invs, "loop invariant, body") :::
+      // this is the state at the beginning of the loop iteration; save these values
+      (for (v <- iterStartGlobals) yield BLocal(v)) :::
+      (iterStartEtran.oldEtran.Heap := iterStartEtran.Heap) ::
+      (iterStartEtran.oldEtran.Mask := iterStartEtran.Mask) ::  // oldMask is not actually used below
+      (for (isv <- iterStartLocalsV) yield BLocal(Variable2BVarWhere(isv))) :::
+      (for ((v,isv) <- w.LoopTargetsList 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") :::
+      isLeaking(w.pos, "The loop might leak refereces.") :::
+      // enforce lockchange
+      (NumberOfLocksHeldIsInvariant(iterStartLocks, newLocks, iterStartEtran) map { e: Boogie.Expr => bassert(e, w.pos, "The loop might lock/unlock more than the changelock clause allows.") }) :::
+      bassume(false),
+   // 3. AFTER LOOP
+     LockHavoc(oldLocks ++ newLocks, loopEtran) :::
+     (NumberOfLocksHeldIsInvariant(oldLocks, newLocks, loopEtran) map bassume) :::
+     Inhale(invs, "loop invariant, after loop") :::
+     bassume(!guard)))
+  }
+
+  def UpdateMu(o: Expr, allowOnlyFromBottom: boolean,
+               lowerBounds: List[Expression], upperBounds: List[Expression], error: ErrorMessage): List[Stmt] = {
+    def BoundIsNullObject(b: Expression): Boogie.Expr = {
+      if (b.typ.IsMu) false else b ==@ bnull
+    }
+    def MuValue(b: Expression): Expr = {
+      if (b.typ.IsMu) b else etran.Heap.select(b, "mu")
+    }
+    def Below(a: Expr, b: Expr) = {
+      new FunctionApp("MuBelow", a, b)
+    }
+    val (muV, mu) = Boogie.NewBVar("mu", Boogie.NamedType("Mu"), true)
+    // check that bounds are well-defined
+    ((lowerBounds ++ upperBounds) flatMap { bound => isDefined(bound)}) :::
+    // check that we have full access to mu
+    bassert(CanWrite(o, "mu"), error.pos, error.message + " The mu field of the target might not be writable.") ::
+    // ...and that mu starts off as lockbottom, if desired
+    (if (allowOnlyFromBottom)
+      List(bassert(etran.Heap.select(o,"mu") ==@ bLockBottom,
+                   error.pos, error.message + " The object may already be shared (i.e., mu may not be LockBottom)"))
+     else
+      List()) :::
+    // check for each bound that if it is a non-null object, then its mu field is readable
+    (for (bound <- lowerBounds ++ upperBounds if !bound.typ.IsMu) yield
+      bassert((bound ==@ bnull) || CanRead(bound, "mu"), bound.pos, "The mu field of bound at " + bound.pos + " might not be readable." )) :::
+    // check that each lower bound is smaller than each upper bound
+    (for (lb <- lowerBounds; ub <- upperBounds) yield
+      bassert( (etran.ShaveOffOld(lb), etran.ShaveOffOld(ub)) match {
+        case ((MaxLockLiteral(),o0), (MaxLockLiteral(),o1)) =>
+          if (o0 == o1)
+            false
+          else
+            etran.TemporalMaxLockComparison(etran.ChooseEtran(o0), etran.ChooseEtran(o1))
+        case ((MaxLockLiteral(),o), _) => etran.ChooseEtran(o).MaxLockIsBelowX(MuValue(ub))
+        case (_, (MaxLockLiteral(),o)) => etran.ChooseEtran(o).MaxLockIsAboveX(MuValue(lb))
+        case _ => BoundIsNullObject(lb) ||
+                  BoundIsNullObject(ub) ||
+                  Below(MuValue(lb), MuValue(ub)) }, lb.pos, "The lower bound at " + lb.pos + " might not be smaller than the upper bound at " + ub.pos + ".")) :::
+    // havoc o.mu
+    BLocal(muV) :: Havoc(mu) :: bassume(mu !=@ bLockBottom) ::
+    // assume that o.mu is between the given bounds (or above maxlock if no bounds are given)
+    (if (lowerBounds == Nil && upperBounds == Nil) {
+      // assume maxlock << o.mu
+      List(bassume(etran.MaxLockIsBelowX(mu)))
+    } else {
+      (for (lb <- lowerBounds) yield
+        // assume lb << o.mu
+        bassume(
+          if (etran.IsMaxLockLit(lb)) {
+            val (f,o) = etran.ShaveOffOld(lb)
+            etran.ChooseEtran(o).MaxLockIsBelowX(mu)
+          } else
+            (BoundIsNullObject(lb) || Below(MuValue(lb), mu)))) :::
+      (for (ub <- upperBounds) yield
+        // assume o.mu << ub
+        bassume(
+          if (etran.IsMaxLockLit(ub)) {
+            val (f,o) = etran.ShaveOffOld(ub)
+            etran.ChooseEtran(o).MaxLockIsAboveX(mu)
+          } else
+            (BoundIsNullObject(ub) || Below(mu, MuValue(ub)))))
+    }) :::
+    // store the mu field
+    etran.Heap.store(o, "mu", mu)
+  }
+
+  def isLeaking(pos: Position, msg: String): List[Boogie.Stmt] = {
+    if(checkLeaks) {
+      var o = Boogie.VarExpr("$o");
+      var f = "$f";
+      val (ttV,tt) = Boogie.NewTVar("T")
+      List(
+        bassert(new Boogie.Forall(
+          List(ttV),
+          List(Boogie.BVar("$o", tref), Boogie.BVar("$f", FieldType(tt))),
+          Nil,
+          (o ==@ bnull) || ((new MapSelect(etran.Mask, o, f, "perm$R") ==@ 0) && (new MapSelect(etran.Mask, o, f, "perm$N") ==@ 0))
+        ), pos, msg)
+      )
+    } else {
+      Nil
+    }
+  }
+
+  def LockFrame(lkch: List[Expression], etran: ExpressionTranslator) =
+    LocksUnchanged(for (l <- lkch) yield etran.Tr(l), etran)
+  def LocksUnchanged(exceptions: List[Boogie.Expr], etran: ExpressionTranslator) = {
+    val (lkV, lk) = Boogie.NewBVar("lk", tref, true)
+    val b: Boogie.Expr = false
+    new Boogie.Forall(List(lkV),
+                  List(etran.Heap.select(lk, "held"), etran.Heap.select(lk, "rdheld")),
+                  (((0 < Boogie.MapSelect(etran.Heap, lk, "held")) ==@
+                    (0 < Boogie.MapSelect(etran.oldEtran.Heap, lk, "held"))) &&
+                   (Boogie.MapSelect(etran.Heap, lk, "rdheld") ==@
+                    Boogie.MapSelect(etran.oldEtran.Heap, lk, "rdheld"))) ||
+                  ((exceptions :\ b) ((e,ll) => ll || (lk ==@ e))))
+  }
+  def LockHavoc(locks: List[Boogie.Expr], etran: ExpressionTranslator) = {
+    val (heldV, held) = NewBVar("isHeld", Boogie.ClassType(IntClass), true)
+    val (rdheldV, rdheld) = NewBVar("isRdHeld", Boogie.ClassType(BoolClass), true)
+    BLocal(heldV) :: BLocal(rdheldV) ::
+    List.flatten (for (o <- locks) yield {  // todo: somewhere we should worry about Df(l)
+      Havoc(held) :: Havoc(rdheld) ::
+      bassume(rdheld ==> (0 < held)) ::
+      MapUpdate(etran.Heap, o, "held", held) ::
+      MapUpdate(etran.Heap, o, "rdheld", rdheld) })
+  }
+  def NumberOfLocksHeldIsInvariant(oldLocks: List[Boogie.Expr], newLocks: List[Boogie.Expr],
+                                   etran: ExpressionTranslator) = {
+    List.flatten (for ((o,n) <- oldLocks zip newLocks) yield {
+      // oo.held == nn.held && oo.rdheld == nn.rdheld
+      (((0 < Boogie.MapSelect(etran.oldEtran.Heap, o, "held")) ==@
+        (0 < Boogie.MapSelect(etran.Heap, n, "held"))) &&
+       (Boogie.MapSelect(etran.oldEtran.Heap, o, "rdheld") ==@
+        Boogie.MapSelect(etran.Heap, n, "rdheld"))) ::
+      // no.held == on.held && no.rdheld == on.rdheld
+      (((0 < Boogie.MapSelect(etran.Heap, o, "held")) ==@
+        (0 < Boogie.MapSelect(etran.oldEtran.Heap, n, "held"))) &&
+       (Boogie.MapSelect(etran.Heap, o, "rdheld") ==@
+        Boogie.MapSelect(etran.oldEtran.Heap, n, "rdheld"))) ::
+      // o == n || (oo.held != no.held && (!oo.rdheld || !no.rdheld))
+      ((o ==@ n) ||
+       (((0 < Boogie.MapSelect(etran.oldEtran.Heap, o, "held")) !=@ (0 < Boogie.MapSelect(etran.Heap, o, "held"))) &&
+        ((! Boogie.MapSelect(etran.oldEtran.Heap, o, "rdheld")) ||
+         (! Boogie.MapSelect(etran.Heap, o, "rdheld"))))) ::
+      Nil
+    })
+  }
+
+  implicit def lift(s: Stmt): List[Stmt] = List(s)
+  def isDefined(e: Expression) = etran.isDefined(e)(true)
+  def TrExpr(e: Expression) = etran.Tr(e)
+
+  def InhaleInvariants(obj: Expression, readonly: boolean, tran: ExpressionTranslator) = {
+    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
+           (inv => SubstThis(inv.e, sh)) map
+           (inv => (if (readonly) SubstRd(inv) else inv)), "monitor invariant", false)
+  }
+  def ExhaleInvariants(obj: Expression, readonly: boolean, msg: ErrorMessage, tran: ExpressionTranslator) = {
+    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
+           (inv => SubstThis(inv.e, sh)) map
+           (inv => (if (readonly) SubstRd(inv) else inv, msg)), "monitor invariant", false)
+  }
+  def InhaleInvariants(obj: Expression, readonly: boolean) = {
+    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
+           (inv => SubstThis(inv.e, sh)) map
+           (inv => (if (readonly) SubstRd(inv) else inv)), "monitor invariant")
+  }
+  def ExhaleInvariants(obj: Expression, readonly: boolean, msg: ErrorMessage) = {
+    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
+           (inv => SubstThis(inv.e, sh)) map
+           (inv => (if (readonly) SubstRd(inv) else inv, msg)), "monitor invariant")
+  }
+
+  def Inhale(predicates: List[Expression], occasion: String): List[Boogie.Stmt] = etran.Inhale(predicates, occasion, false)
+  def Exhale(predicates: List[(Expression, ErrorMessage)], occasion: String): List[Boogie.Stmt] = etran.Exhale(predicates, occasion, false)
+  def InhaleWithChecking(predicates: List[Expression], occasion: String): List[Boogie.Stmt] = etran.Inhale(predicates, occasion, true)
+  def ExhaleWithChecking(predicates: List[(Expression, ErrorMessage)], occasion: String): List[Boogie.Stmt] = etran.Exhale(predicates, occasion, true)
+
+  def CanRead(obj: Boogie.Expr, field: Boogie.Expr): Boogie.Expr = etran.CanRead(obj, field)
+  def CanWrite(obj: Boogie.Expr, field: Boogie.Expr): Boogie.Expr = etran.CanWrite(obj, field)
+
+
+  /**********************************************************************
+  *****************          EXPRESSIONS                *****************
+  **********************************************************************/
+
+class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.Expr], currentClass: Class) {
+  import TranslationHelper._
+  import TranslationOptions._
+
+  val Heap = globals(0);
+  val Mask = globals(1);
+  lazy val oldEtran = new ExpressionTranslator(preGlobals, preGlobals, currentClass)
+  var checkTermination = false; // check that heap required by callee is strictly smaller than heap required by caller
+
+  def this(globals: List[Boogie.Expr], cl: Class) = this(globals, globals map (g => Boogie.Old(g)), cl)
+  def this(cl: Class) = this(for ((id,t) <- S_ExpressionTranslator.Globals) yield Boogie.VarExpr(id), cl)
+
+  def Globals = List(Heap, Mask)
+  def ChooseEtran(chooseOld: boolean) = if (chooseOld) oldEtran else this
+  // Create a list of fresh global variables
+  def FreshGlobals(prefix: String) = {
+    new Boogie.BVar(prefix + "Heap", theap, true) ::
+    new Boogie.BVar(prefix + "Mask", tmask, true) ::
+    Nil
+  }
+
+  // Create a new ExpressionTranslator that is a copy of the receiver, but with
+  // preGlobals as the old global variables 
+  def FromPreGlobals(preGlobals: List[Boogie.BVar]) = {
+    val g = for ((id,t) <- S_ExpressionTranslator.Globals) yield VarExpr(id)
+    val pg = preGlobals map (g => new VarExpr(g))
+    new ExpressionTranslator(g, pg, currentClass)
+  }
+
+  def UseCurrentAsOld() = {
+    new ExpressionTranslator(globals, globals, currentClass);
+  }
+
+  def WhereOldIs(h: Boogie.Expr, m: Boogie.Expr) = {
+    new ExpressionTranslator(globals, List(h, m), currentClass);
+  }
+
+  /**********************************************************************
+  *****************              TR/DF                  *****************
+  **********************************************************************/
+ 
+  def isDefined(e: Expression)(implicit assumption: Expr): List[Boogie.Stmt] = {
+    def prove(goal: Expr, pos: Position, msg: String)(implicit assumption: Expr): Boogie.Assert = {
+      bassert(assumption ==> goal, pos, msg)
+    }
+    e match {
+      case IntLiteral(n) => Nil
+      case BoolLiteral(b) => Nil
+      case NullLiteral() => Nil
+      case MaxLockLiteral() => Nil
+      case LockBottomLiteral() => Nil
+      case _:ThisExpr => Nil
+      case _:Result => Nil
+      case _:VariableExpr => Nil
+      case fs @ MemberAccess(e, f) =>       
+        assert(!fs.isPredicate);
+        isDefined(e) ::: 
+        prove(nonNull(Tr(e)), e.pos, "Receiver might be null.") ::
+        prove(CanRead(Tr(e), fs.f.FullName), fs.pos, "Location might not be readable.")
+      case _:Access => throw new Exception("acc expression unexpected here")
+      case _:RdAccess => throw new Exception("rd expression unexpected here")
+      case _:AccessAll => throw new Exception("acc expression unexpected here")
+      case _:RdAccessAll => throw new Exception("rd expression unexpected here")
+      case Holds(e) =>
+        isDefined(e)
+      case RdHolds(e) =>
+        isDefined(e)
+      case _: Assigned => Nil
+      case Old(e) =>
+        oldEtran.isDefined(e)
+      case IfThenElse(con, then, els) =>
+        isDefined(con) ::: Boogie.If(Tr(con), isDefined(then), isDefined(els))
+      case Not(e) =>
+        isDefined(e)
+      case func@FunctionApplication(obj, id, args) =>
+        val newGlobals = FreshGlobals("checkPre");
+        val (tmpHeapV, tmpHeap) = Boogie.NewBVar("Heap", theap, true);
+        val (tmpMaskV, tmpMask) = Boogie.NewBVar("Mask", tmask, true); 
+        val tmpTranslator = new ExpressionTranslator(List(tmpHeap,tmpMask), currentClass);
+        // check definedness of receiver + arguments
+        (obj :: args flatMap { arg => isDefined(arg) }) :::
+        // check that receiver is not null
+        List(prove(nonNull(Tr(obj)), obj.pos, "Receiver might be null.")) :::
+        // check precondition of the function by exhaling the precondition in tmpHeap/tmpMask
+        Comment("check precondition of call") ::
+        bassume(assumption) ::
+        BLocal(tmpHeapV) :: (tmpHeap := Heap) ::
+        BLocal(tmpMaskV) :: (tmpMask := Mask) :::
+        tmpTranslator.Exhale(Preconditions(func.f.spec) map { pre=> (SubstThisAndVars(pre, obj, func.f.ins, args), ErrorMessage(func.pos, "Precondition at " + pre.pos + " might not hold."))},
+                             "function call",
+                             false) :::
+        // size of the heap of callee must be strictly smaller than size of the heap of the caller
+        (if(checkTermination) { List(prove(NonEmptyMask(tmpMask), func.pos, "The heap of the callee might not be strictly smaller than the heap of the caller.")) } else Nil)
+      case unfolding@Unfolding(access, e) =>
+        val (checks, predicate, definition, from) = access match {
+          case acc@Access(pred@MemberAccess(obj, f), perm) => 
+           val receiverOk = isDefined(obj) ::: prove(nonNull(Tr(obj)), obj.pos, "Receiver might be null.");
+           val body = SubstThis(DefinitionOf(pred.predicate), obj);
+            perm match {           
+              case None => (receiverOk, acc, body, Heap.select(Tr(obj), pred.predicate.FullName))
+              case Some(fraction) => (receiverOk ::: isDefined(fraction) ::: prove(0 <= Tr(fraction), fraction.pos, "Fraction might be negative") :: prove(Tr(fraction) <= 100, fraction.pos, "Fraction might exceed 100."), acc, FractionOf(body, fraction), Heap.select(Tr(obj), pred.predicate.FullName))
+            }
+          case acc@RdAccess(pred@MemberAccess(obj, f), perm) =>
+            val receiverOk = isDefined(obj) ::: prove(nonNull(Tr(obj)), obj.pos, "Receiver might be null.");
+            val body = SubstThis(DefinitionOf(pred.predicate), obj);
+            perm match {
+              case None => (receiverOk, acc, EpsilonsOf(body, IntLiteral(1)), Heap.select(Tr(obj), pred.predicate.FullName))
+              case Some(None) => assert(false); (null, null, null, Heap.select(Tr(obj), pred.predicate.FullName))
+              case Some(Some(epsilons)) => (receiverOk ::: isDefined(epsilons) ::: prove(0 <= Tr(epsilons), epsilons.pos, "Number of epsilons might be negative"), acc, EpsilonsOf(body, epsilons), Heap.select(Tr(obj), pred.predicate.FullName))
+            }
+        }
+        val newGlobals = FreshGlobals("checkPre");
+        val (tmpHeapV, tmpHeap) = Boogie.NewBVar("Heap", theap, true);
+        val (tmpMaskV, tmpMask) = Boogie.NewBVar("Mask", tmask, true); 
+        val tmpTranslator = new ExpressionTranslator(List(tmpHeap, tmpMask), currentClass);
+        Comment("unfolding") ::
+        // check definedness
+        checks :::
+        // copy state into temporary variables
+        BLocal(tmpHeapV) :: Boogie.Assign(tmpHeap, Heap) ::
+        BLocal(tmpMaskV) :: Boogie.Assign(tmpMask, Mask) ::
+        // exhale the predicate
+        tmpTranslator.Exhale(List((predicate, ErrorMessage(unfolding.pos, "Unfolding might fail."))), "unfolding", false) :::
+        // inhale the definition of the predicate
+        tmpTranslator.InhaleFrom(List(definition), "unfolding", false, from) :::
+        // check definedness of e in state where the predicate is unfolded
+        tmpTranslator.isDefined(e)
+      case Iff(e0,e1) =>
+        isDefined(e0) ::: isDefined(e1)
+      case Implies(e0,e1) =>
+        isDefined(e0) ::: isDefined(e1)(assumption && Tr(e0))
+      case And(e0,e1) =>
+        isDefined(e0) ::: isDefined(e1)(assumption && Tr(e0))
+      case Or(e0,e1) =>
+        isDefined(e0) ::: isDefined(e1)(assumption && Boogie.UnaryExpr("!", Tr(e0)))
+      case LockBelow(e0,e1) =>
+        var df = isDefined(e0) ::: isDefined(e1);
+        if (e0.typ.IsRef) {
+          df = df ::: List(prove(nonNull(Tr(e0)), e0.pos, "Receiver might be null."), prove(CanRead(Tr(e0),"mu"), e0.pos, "The mu field might not be readable."));
+        }
+         if (e1.typ.IsRef) {
+          df = df ::: List(prove(nonNull(Tr(e1)), e1.pos, "Receiver might be null."), prove(CanRead(Tr(e1),"mu"), e1.pos, "The mu field might not be readable."));
+        }
+        df
+      case e: CompareExpr =>
+        isDefined(e.E0) ::: isDefined(e.E1)
+      case Div(e0,e1) =>
+        isDefined(e0) ::: isDefined(e1) :::
+        List(prove(Tr(e1) !=@ 0, e1.pos, "Denominator might be zero."))
+      case Mod(e0,e1) =>
+        isDefined(e0) ::: isDefined(e1) ::: List(prove(Tr(e1) !=@ 0, e1.pos, "Denominator might be zero."))
+      case e: ArithmeticExpr =>
+        isDefined(e.E0) ::: isDefined(e.E1)
+      case q@Forall(i, Range(min, max), e) =>
+        // optimize for range
+        isDefinedForall(q.variables, min, max, e)
+      case q@Forall(i, seq, e) =>
+      var newVars = Nil : List[Variable];
+        for(i <- q.variables) {
+          newVars = newVars + new Variable(i.UniqueName, new Type(IntClass))
+        }
+        isDefinedForall(newVars, IntLiteral(0), Length(seq), SubstVars(e, q.variables, newVars map {newVar => At(seq, new VariableExpr(newVar)) }))
+      case EmptySeq(t) => Nil
+      case ExplicitSeq(es) =>
+        es flatMap { e => isDefined(e) }
+      case Range(min, max) =>
+        isDefined(min) ::: isDefined(max)
+      case Append(e0, e1) =>
+        isDefined(e0) ::: isDefined(e1)
+      case at@At(e0, e1) =>
+        isDefined(e0) ::: isDefined(e1) ::: List(prove(0 <= Tr(e1), at.pos, "Sequence index might be negative."), prove(Tr(e1) < Boogie.FunctionApp("Seq#Length", List(Tr(e0))), at.pos, "Sequence index might be larger than or equal to the length of the sequence."))
+      case Drop(e0, e1) => 
+        isDefined(e0) ::: isDefined(e1) ::: List(prove(0 <= Tr(e1), e.pos, "Cannot drop less than zero elements."), prove(Tr(e1) <= Boogie.FunctionApp("Seq#Length", List(Tr(e0))), e.pos, "Cannot drop more than elements than the length of the sequence."))
+      case Take(e0, e1) => 
+        isDefined(e0) ::: isDefined(e1) ::: List(prove(0 <= Tr(e1), e.pos, "Cannot take less than zero elements."), prove(Tr(e1) <= Boogie.FunctionApp("Seq#Length", List(Tr(e0))), e.pos, "Cannot take more than elements than the length of the sequence."))
+      case Length(e) =>
+        isDefined(e)
+      case Eval(h, e) =>
+        val (evalHeap, evalMask, checks, assumptions) = fromEvalState(h);
+        val evalEtran = new ExpressionTranslator(List(evalHeap, evalMask), currentClass);
+        evalEtran.isDefined(e)
+    }
+  }
+
+  def isDefinedForall(is: List[Variable], min: Expression, max: Expression, e: Expression)(implicit assumption: Expr): List[Stmt] = {
+    var iTmps = Nil: List[Variable];
+    var assumption2 = assumption;
+    for(i <- is) { 
+      val iTmp = new Variable(i.UniqueName, new Type(IntClass));
+      iTmps = iTmps + iTmp; 
+      assumption2 = assumption2 && (Tr(min)<=VarExpr(iTmp.UniqueName)) && (VarExpr(iTmp.UniqueName) < Tr(max))
+    }
+    // check definedness of the bounds
+    isDefined(min) ::: isDefined(max) :::
+    // introduce a new local iTmp with an arbitrary value
+    (iTmps map { iTmp =>
+      BLocal(Boogie.BVar(iTmp.UniqueName, Boogie.NamedType("int")))
+    }) :::
+    // prove that the body is well-defined for iTmp, provided iTmp lies betweeen min and max 
+    isDefined(SubstVars(e, is, iTmps map { iTmp => new VariableExpr(iTmp)}))(assumption2)
+  }
+
+  def Tr(e: Expression): Boogie.Expr = e match {
+    case IntLiteral(n) => n
+    case BoolLiteral(b) => b
+    case NullLiteral() => bnull
+    case MaxLockLiteral() => throw new Exception("maxlock case should be handled in << and == and !=")
+    case LockBottomLiteral() => bLockBottom
+    case _:ThisExpr => VarExpr("this")
+    case _:Result => VarExpr("result")
+    case ve : VariableExpr => VarExpr(ve.v.UniqueName)
+    case fs @ MemberAccess(e,_) =>
+      assert(! fs.isPredicate);
+      var r = Heap.select(Tr(e), fs.f.FullName);
+      if (fs.f.isInstanceOf[SpecialField] && fs.f.id == "joinable")
+        r !=@ 0 // joinable is encoded as an integer
+      else
+        r
+    case _:Access => throw new Exception("acc expression unexpected here")
+    case _:RdAccess => throw new Exception("rd expression unexpected here")
+    case _:AccessAll => throw new Exception("acc expression unexpected here")
+    case _:RdAccessAll => throw new Exception("rd expression unexpected here")
+    case Holds(e) =>
+      (0 < Heap.select(Tr(e), "held")) &&
+      !Heap.select(Tr(e), "rdheld")
+    case RdHolds(e) =>
+      Heap.select(Tr(e), "rdheld")
+    case a: Assigned =>
+      VarExpr("assigned$" + a.v.UniqueName)
+    case Old(e) =>
+      oldEtran.Tr(e)
+    case IfThenElse(con, then, els) =>
+      Boogie.Ite(Tr(con), Tr(then), Tr(els))  // of type: VarExpr(TrClass(then.typ))
+    case Not(e) =>
+      ! Tr(e)
+    case func@FunctionApplication(obj, id, args) =>
+      FunctionApp("#" + func.f.Parent.id + "." + id, Heap :: Mask :: (obj :: args map { arg => Tr(arg)}))
+    case uf@Unfolding(_, e) =>
+      Tr(e)
+    case Iff(e0,e1) =>
+      Tr(e0) <==> Tr(e1)
+    case Implies(e0,e1) =>
+      Tr(e0) ==> Tr(e1)
+    case And(e0,e1) =>
+      Tr(e0) && Tr(e1)
+    case Or(e0,e1) =>
+      Tr(e0) || Tr(e1)
+    case Eq(e0,e1) =>
+      (ShaveOffOld(e0), ShaveOffOld(e1)) match {
+        case ((MaxLockLiteral(),o0), (MaxLockLiteral(),o1)) =>
+          if (o0 == o1)
+            true
+          else
+            MaxLockPreserved
+        case ((MaxLockLiteral(),o), (fs@MemberAccess(q, "mu"), useOld)) => isHeldInHeap(Tr(q), ChooseEtran(useOld).Heap) && ChooseEtran(o).MaxLockEqualsX(Tr(fs))
+        case ((MaxLockLiteral(),o), _) => ChooseEtran(o).MaxLockEqualsX(Tr(e1))
+        case (_, (MaxLockLiteral(),o)) => ChooseEtran(o).MaxLockEqualsX(Tr(e0))
+        case _ => if(e0.typ.IsSeq) FunctionApp("Seq#Equal", List(Tr(e0), Tr(e1))) else (Tr(e0) ==@ Tr(e1))
+      }
+    case Neq(e0,e1) =>
+      if (IsMaxLockLit(e0) || IsMaxLockLit(e1))
+        Tr(Not(Eq(e0,e1)))
+      else
+        (Tr(e0) !=@ Tr(e1))
+    case Less(e0,e1) =>
+      Tr(e0) < Tr(e1)
+    case AtMost(e0,e1) =>
+      Tr(e0) <= Tr(e1)
+    case AtLeast(e0,e1) =>
+      Tr(e0) >= Tr(e1)
+    case Greater(e0,e1) =>
+      Tr(e0) > Tr(e1)
+    case LockBelow(e0,e1) => {
+      def MuValue(b: Expression): Boogie.Expr =
+        if (b.typ.IsRef) Boogie.MapSelect(Heap, Tr(b), "mu") else Tr(b)
+      (ShaveOffOld(e0), ShaveOffOld(e1)) match {
+        case ((MaxLockLiteral(),o0), (MaxLockLiteral(),o1)) =>
+          if (o0 == o1)
+            false
+          else
+            TemporalMaxLockComparison(ChooseEtran(o0), ChooseEtran(o1))
+        case ((MaxLockLiteral(),o), _) => ChooseEtran(o).MaxLockIsBelowX(MuValue(e1))
+        case (_, (MaxLockLiteral(),o)) => ChooseEtran(o).MaxLockIsAboveX(MuValue(e0))
+        case _ => new FunctionApp("MuBelow", MuValue(e0), MuValue(e1)) }
+    }
+    case Plus(e0,e1) =>
+      Tr(e0) + Tr(e1)
+    case Minus(e0,e1) =>
+      Tr(e0) - Tr(e1)
+    case Times(e0,e1) =>
+      Tr(e0) * Tr(e1)
+    case Div(e0,e1) =>
+      Tr(e0) / Tr(e1)
+    case Mod(e0,e1) =>
+      Tr(e0) % Tr(e1)
+    case q@Forall(is, Range(min, max), e) =>
+      // optimize translation for range expressions
+      translateForall(q.variables, min, max, e)
+    case q@Forall(is, seq, e) =>
+      var newVars = Nil : List[Variable];
+      for(i <- q.variables) {
+        newVars = newVars + new Variable(i.UniqueName, new Type(IntClass))
+      }
+      translateForall(newVars, IntLiteral(0), Length(seq), SubstVars(e, q.variables, newVars map {newVar => At(seq, new VariableExpr(newVar)) }))
+    case EmptySeq(t) =>
+      createEmptySeq
+    case ExplicitSeq(es) =>
+      es match {
+        case Nil => createEmptySeq
+        case h :: Nil => createSingletonSeq(Tr(h))
+        case h :: t => createAppendSeq(createSingletonSeq(Tr(h)), Tr(ExplicitSeq(t)))
+      }
+    case Range(min, max) =>
+      createRange(Tr(min), Tr(max))
+    case Append(e0, e1) =>
+      createAppendSeq(Tr(e0), Tr(e1))
+    case at@At(e0, e1) =>
+      FunctionApp("Seq#Index", List(Tr(e0), Tr(e1)))  // of type: VarExpr(TrClass(e0.typ.parameters(0)))
+    case Drop(e0, e1) =>
+      Boogie.FunctionApp("Seq#Drop", List(Tr(e0), Tr(e1)))
+    case Take(e0, e1) =>
+      Boogie.FunctionApp("Seq#Take", List(Tr(e0), Tr(e1)))
+    case Length(e) =>
+      Boogie.FunctionApp("Seq#Length", List(Tr(e)))
+    case Eval(h, e) =>
+      val (evalHeap, evalMask, checks, assumptions) = fromEvalState(h);
+      val evalEtran = new ExpressionTranslator(List(evalHeap, evalMask), currentClass);
+      evalEtran.Tr(e)
+  }
+ 
+  def translateForall(is: List[Variable], min: Expression, max: Expression, e: Expression): Expr = {
+    var assumption = true: Expr;
+    for(i <- is) {
+      assumption = assumption && (Tr(min) <= VarExpr(i.UniqueName) && VarExpr(i.UniqueName) < Tr(max));
+    }
+    new Boogie.Forall(is map { i=> Variable2BVar(i)}, Nil, assumption ==> Tr(e))
+  }
+
+  def ShaveOffOld(e: Expression): (Expression, boolean) = e match {
+    case Old(e) =>
+      val (f,o) = ShaveOffOld(e)
+      (f,true)
+    case _ => (e,false)
+  }
+  def IsMaxLockLit(e: Expression) = {
+    val (f,o) = ShaveOffOld(e)
+    f.isInstanceOf[MaxLockLiteral]
+  }
+
+  /**********************************************************************
+  *****************          INHALE/EXHALE              *****************
+  **********************************************************************/
+
+  def Inhale(predicates: List[Expression], occasion: String, check: Boolean): List[Boogie.Stmt] = {
+    val (ihV, ih) = Boogie.NewBVar("inhaleHeap", theap, true)
+    Comment("inhale (" + occasion + ")") ::
+    BLocal(ihV) :: Boogie.Havoc(ih) ::
+    bassume(IsGoodInhaleState(ih, Heap, Mask)) ::
+    List.flatten (for (p <- predicates) yield Inhale(p,ih, check)) :::
+    bassume(IsGoodMask(Mask)) ::
+    bassume(wf(Heap, Mask)) ::
+    Comment("end inhale")
+  }
+
+  def InhaleFrom(predicates: List[Expression], occasion: String, check: Boolean, useHeap: Boogie.Expr): List[Boogie.Stmt] = {
+    val (ihV, ih) = Boogie.NewBVar("inhaleHeap", theap, true)
+    Comment("inhale (" + occasion + ")") ::
+    BLocal(ihV) :: Boogie.Assign(ih, useHeap) ::
+    bassume(IsGoodInhaleState(ih, Heap, Mask)) ::
+    List.flatten (for (p <- predicates) yield Inhale(p,ih, check)) :::
+    bassume(IsGoodMask(Mask)) ::
+    bassume(wf(Heap, Mask)) ::
+    Comment("end inhale")
+  }
+
+  def Inhale(p: Expression, ih: Boogie.Expr, check: Boolean): List[Boogie.Stmt] = p match {
+    case pred@MemberAccess(e, p) if pred.isPredicate => 
+      val tmp = Access(pred, None);
+      tmp.pos = pred.pos;
+      Inhale(tmp, ih, check)
+    case acc@AccessAll(obj, perm) =>
+      obj.typ.Fields flatMap { f => 
+        val ma = MemberAccess(obj, f.id);
+        ma.f = f;
+        ma.pos = acc.pos;
+        val inhalee = Access(ma, perm);
+        inhalee.pos = acc.pos;
+        Inhale(inhalee, ih, check) }
+    case acc@RdAccessAll(obj, perm) =>
+      obj.typ.Fields flatMap { f => 
+        val ma = MemberAccess(obj, f.id);
+        ma.f = f;
+        ma.pos = acc.pos;
+        val inhalee = RdAccess(ma, perm);
+        inhalee.pos = acc.pos;
+        Inhale(inhalee, ih, check) }
+    case acc@Access(e,perm) =>
+      val trE = Tr(e.e)
+      val module = currentClass.module;
+      val memberName = if(e.isPredicate) e.predicate.FullName else e.f.FullName;
+      (if(check) isDefined(e.e)(true)
+        // List(bassert(nonNull(trE), acc.pos, "The target of the acc predicate might be null."))
+       else Nil) :::
+      (perm match { 
+        case None => List() 
+        case Some(perm) =>
+          (if(check) isDefined(perm)(true) ::: bassert(Boogie.IntLiteral(0)<=Tr(perm), perm.pos, "Fraction might be negative.") ::  
+          (if(! e.isPredicate) bassert(Tr(perm) <= Boogie.IntLiteral(100), perm.pos, "Fraction might exceed 100.") :: Nil else Nil) else Nil)
+      }) :::
+      bassume(nonNull(trE)) ::
+      MapUpdate(Heap, trE, memberName, Boogie.MapSelect(ih, trE, memberName)) ::
+      bassume(wf(Heap, Mask)) ::
+      (if(e.isPredicate && e.predicate.Parent.module.equals(currentClass.module)) List(bassume(Boogie.MapSelect(ih, trE, memberName) ==@ Heap)) else Nil) :::
+      (if(e.isPredicate) Nil else List(bassume(TypeInformation(Boogie.MapSelect(Heap, trE, memberName), e.f.typ)))) :::
+      (perm match {
+        case None => IncPermission(trE, memberName, 100)
+        case Some(perm) => IncPermission(trE, memberName, Tr(perm))
+      }) ::
+      bassume(IsGoodMask(Mask)) ::
+      bassume(IsGoodState(Boogie.MapSelect(ih, trE, memberName))) ::
+      bassume(wf(Heap, Mask)) ::
+      bassume(wf(ih, Mask))
+    case rdacc@RdAccess(e,perm) =>
+      val memberName = if(e.isPredicate) e.predicate.FullName else e.f.FullName;
+      val trE = Tr(e.e)
+      val (dfP,p) = perm match {
+        case None => (List(), Boogie.IntLiteral(1))
+        case Some(None) => (List(), null)
+        case Some(Some(p)) => (isDefined(p)(true) ::: bassert(Boogie.IntLiteral(0)<=Tr(p), p.pos, "Number of epsilons might be negative."), Tr(p))
+      }
+      (if(check) { isDefined(e.e)(true) :::
+        // bassert(nonNull(trE), rdacc.pos, "The target of the rd predicate might be null.")
+        dfP } else Nil) :::
+      bassume(nonNull(trE)) ::
+      Boogie.MapUpdate(Heap, trE, memberName,
+                       Boogie.MapSelect(ih, trE, memberName)) ::
+      bassume(Boogie.FunctionApp("wf", List(Heap, Mask))) ::
+      (if(e.isPredicate && e.predicate.Parent.module.equals(currentClass.module)) List(bassume(Boogie.MapSelect(ih, trE, memberName) ==@ Heap)) else Nil) :::
+      (if(e.isPredicate) Nil else List(bassume(TypeInformation(Boogie.MapSelect(Heap, trE, memberName), e.f.typ)))) :::
+      IncPermissionEpsilon(trE, memberName, p) ::
+      bassume(IsGoodMask(Mask)) ::
+      bassume(IsGoodState(Boogie.MapSelect(ih, trE, memberName))) ::
+      bassume(wf(Heap, Mask)) ::
+      bassume(wf(ih, Mask))
+    case Implies(e0,e1) =>
+      (if(check) isDefined(e0)(true) else Nil) :::
+      Boogie.If(Tr(e0), Inhale(e1, ih, check), Nil)
+    case IfThenElse(con, then, els) =>
+      (if(check) isDefined(con)(true) else Nil) :::
+      Boogie.If(Tr(con), Inhale(then, ih, check), Inhale(els, ih, check))
+    case And(e0,e1) =>
+      Inhale(e0, ih, check) ::: Inhale(e1, ih, check)
+    case holds@Holds(e) =>
+      val trE = Tr(e);
+      (if(check) isDefined(e)(true) :::
+      List(bassert(nonNull(trE), holds.pos, "The target of the holds predicate might be null.")) else Nil) :::
+      IncPermission(trE, "held", 100) :::
+      bassume(IsGoodMask(Mask)) ::
+      bassume(IsGoodState(Boogie.MapSelect(ih, trE, "held"))) ::
+      bassume(wf(Heap, Mask)) ::
+      bassume(wf(ih, Mask)) ::
+      Boogie.MapUpdate(Heap, trE, "held",
+                      Boogie.MapSelect(ih, trE, "held")) ::
+      bassume(0 < Boogie.MapSelect(ih, trE, "held")) ::
+      bassume(! Boogie.MapSelect(ih, trE, "rdheld")) ::
+      bassume(wf(Heap, Mask)) ::
+      bassume(IsGoodMask(Mask)) ::
+      bassume(IsGoodState(Boogie.MapSelect(ih, trE, "held"))) ::
+      bassume(wf(Heap, Mask)) ::
+      bassume(wf(ih, Mask))
+    case Eval(h, e) => 
+      val (evalHeap, evalMask, checks, proofOrAssume) = fromEvalState(h);
+      val preGlobals = etran.FreshGlobals("eval")
+      val preEtran = new ExpressionTranslator(preGlobals map (v => new Boogie.VarExpr(v)), currentClass)
+      BLocal(preGlobals(0)) :: BLocal(preGlobals(1)) ::
+      (new VarExpr(preGlobals(1)) := ZeroMask) ::
+      // Should we start from ZeroMask instead of an arbitrary mask? In that case, assume submask(preEtran.Mask, evalMask); at the end!
+      (if(check) checks else Nil) :::
+      // havoc the held field when inhaling eval(o.release, ...)
+      (if(h.isInstanceOf[ReleaseState]) {
+        val (freshHeldV, freshHeld) = NewBVar("freshHeld", tint, true);
+        val obj = Tr(h.target());
+        List(BLocal(freshHeldV), bassume((0<Heap.select(obj, "held")) <==> (0<freshHeld)), (Heap.select(obj, "held") := freshHeld))
+      } else Nil) :::
+      bassume(IsGoodMask(preEtran.Mask)) ::
+      bassume(wf(preEtran.Heap, preEtran.Mask)) ::
+      bassume(proofOrAssume) ::
+      preEtran.Inhale(e, ih, check) :::
+      bassume(preEtran.Heap ==@ evalHeap) ::
+      bassume(submask(preEtran.Mask, evalMask))
+    case e => (if(check) isDefined(e)(true) else Nil) ::: bassume(Tr(e))
+  }
+
+  def Exhale(predicates: List[(Expression, ErrorMessage)], occasion: String, check: Boolean): List[Boogie.Stmt] = {
+    val (emV, em) = NewBVar("exhaleMask", tmask, true)
+    Comment("begin exhale (" + occasion + ")") ::
+    BLocal(emV) :: (em := Mask) ::
+    (List.flatten (for (p <- predicates) yield Exhale(p._1, em, null, p._2, check))) :::
+    (Mask := em) ::
+    bassume(wf(Heap, Mask)) ::
+    Comment("end exhale")
+  }
+
+  def Exhale(p: Expression, em: Boogie.Expr, eh: Boogie.Expr, error: ErrorMessage, check: Boolean): List[Boogie.Stmt] = p match {
+    case pred@MemberAccess(e, p) if pred.isPredicate =>
+      val tmp = Access(pred, None);
+      tmp.pos = pred.pos;
+      Exhale(tmp, em , eh, error, check)
+    case acc@AccessAll(obj, perm) =>
+      obj.typ.Fields flatMap { f => 
+        val ma = MemberAccess(obj, f.id);
+        ma.f = f;
+        ma.pos = acc.pos;
+        val exhalee = Access(ma, perm);
+        exhalee.pos = acc.pos;
+        Exhale(exhalee, em, eh, error, check) }
+    case acc@RdAccessAll(obj, perm) =>
+      obj.typ.Fields flatMap { f => 
+        val ma = MemberAccess(obj, f.id);
+        ma.f = f;
+        ma.pos = acc.pos;
+        val exhalee = RdAccess(ma, perm);
+        exhalee.pos = acc.pos;
+        Exhale(exhalee, em, eh, error, check) }
+    case acc@Access(e,perm) =>
+      val memberName = if(e.isPredicate) e.predicate.FullName else e.f.FullName;
+      // look up the fraction
+      val (fraction, checkFraction) = perm match {
+        case None => (IntLiteral(100), Nil)
+        case Some(fr) => (fr, bassert(0<=Tr(fr), fr.pos, "Fraction might be negative.") :: (if(! e.isPredicate) bassert(Tr(fr)<=100, fr.pos, "Fraction might exceed 100.") :: Nil else Nil) ::: Nil)
+      }
+      val (fractionV, frac) = NewBVar("fraction", tint, true);
+      // check definedness
+      (if(check) isDefined(e.e)(true) :::
+                 checkFraction :::
+                 bassert(nonNull(Tr(e.e)), error.pos, error.message + " The target of the acc predicate at " + acc.pos + " might be null.") else Nil) :::
+      BLocal(fractionV) :: (frac := Tr(fraction)) ::
+      // if the mask does not contain sufficient permissions, try folding acc(e, fraction)
+      (if(e.isPredicate && autoFold && (!perm.isDefined || canTakeFractionOf(DefinitionOf(e.predicate)))) {
+         val inhaleTran = new ExpressionTranslator(List(Heap, em), currentClass);
+         val sourceVar = new Variable("fraction", new Type(IntClass));
+         val bplVar = Variable2BVar(sourceVar);
+         BLocal(bplVar) :: (VarExpr(sourceVar.UniqueName) := frac) ::
+         If(new MapSelect(em, Tr(e.e), memberName, "perm$R") < frac,
+           Exhale(if(perm.isDefined) FractionOf(SubstThis(DefinitionOf(e.predicate), e.e), new VariableExpr(sourceVar)) else SubstThis(DefinitionOf(e.predicate), e.e), em, eh, ErrorMessage(error.pos, error.message + " Automatic fold might fail."), false) :::
+           inhaleTran.Inhale(List(if(! perm.isDefined) Access(e, None) else Access(e, Some(new VariableExpr(sourceVar)))), "automatic fold", false)
+         , Nil) :: Nil}
+       else Nil) :::
+      // check that the necessary permissions are there and remove them from the mask
+      DecPermission(Tr(e.e), memberName, frac, em, error, acc.pos) :::
+      bassume(IsGoodMask(Mask)) ::
+      bassume(wf(Heap, Mask)) ::
+      bassume(wf(Heap, em))
+    case rd@RdAccess(e,perm) =>
+      val memberName = if(e.isPredicate) e.predicate.FullName else e.f.FullName;
+      val (epsilonsV, eps) = NewBVar("epsilons", tint, true);
+      val (dfP, epsilons) = perm match {
+        case None => (List(), IntLiteral(1))
+        case Some(None) => (List(), null)
+        case Some(Some(p)) => (isDefined(p)(true) ::: List(bassert(0 <= Tr(p), error.pos, error.message + " The number of epsilons at " + rd.pos + " might be negative.")) , p)
+      }
+      // check definedness
+      (if(check) isDefined(e.e)(true) :::
+        bassert(nonNull(Tr(e.e)), error.pos, error.message + " The target of the rd predicate at " + rd.pos + " might be null.") ::
+        dfP else Nil) :::
+      BLocal(epsilonsV) :: (if(epsilons!=null) (eps := Tr(epsilons)) :: Nil else Nil) :::
+      // if the mask does not contain sufficient permissions, try folding rdacc(e, epsilons)
+      (if(e.isPredicate && autoFold && canTakeEpsilonsOf(DefinitionOf(e.predicate)) && epsilons!=null) {
+          val inhaleTran = new ExpressionTranslator(List(Heap, em), currentClass);
+          val sourceVar = new Variable("epsilons", new Type(IntClass));
+          val bplVar = Variable2BVar(sourceVar);
+          BLocal(bplVar) :: (VarExpr(sourceVar.UniqueName) := eps) ::
+          If(new MapSelect(em, Tr(e.e), memberName, "perm$N") < eps,
+            Exhale(EpsilonsOf(SubstThis(DefinitionOf(e.predicate), e.e), new VariableExpr(sourceVar)), em, eh, ErrorMessage(error.pos, error.message + " Automatic fold might fail."), false) :::
+            inhaleTran.Inhale(List(RdAccess(e, Some(Some(new VariableExpr(sourceVar))))), "automatic fold", false)
+          , Nil) :: Nil}
+       else Nil) :::
+      // check that the necessary permissions are there and remove them from the mask
+      DecPermissionEpsilon(Tr(e.e), memberName, if(epsilons != null) eps else null, em, error, rd.pos) :::
+      bassume(IsGoodMask(Mask)) ::
+      bassume(wf(Heap, Mask)) ::
+      bassume(wf(Heap, em))
+    case Implies(e0,e1) =>
+      (if(check) isDefined(e0)(true) else Nil) :::
+      Boogie.If(Tr(e0), Exhale(e1, em, eh, error, check), Nil)
+    case IfThenElse(con, then, els) =>
+      (if(check) isDefined(con)(true) else Nil) :::
+      Boogie.If(Tr(con), Exhale(then, em, eh, error, check), Exhale(els, em, eh, error, check))
+    case And(e0,e1) =>
+      Exhale(e0, em, eh, error, check) ::: Exhale(e1, em, eh, error, check)
+    case holds@Holds(e) => 
+      (if(check) isDefined(e)(true) :::
+      bassert(nonNull(Tr(e)), error.pos, error.message + " The target of the holds predicate at " + holds.pos + " might be null.") :: Nil else Nil) :::
+      bassert(HasFullPermission(Tr(e), "held", em), error.pos, error.message + " The current thread might not have full permission to the held field at " + holds.pos + ".") ::
+      bassert(0 < Boogie.MapSelect(Heap, Tr(e), "held"), error.pos, error.message + " The current thread might not hold lock at " + holds.pos + ".") ::
+      bassert(! Boogie.MapSelect(Heap, Tr(e), "rdheld"), error.pos, error.message + " The current thread might hold the read lock at " + holds.pos + ".") ::
+      SetNoPermission(Tr(e), "held", em) ::
+      bassume(IsGoodMask(Mask)) ::
+      bassume(wf(Heap, Mask)) ::
+      bassume(wf(Heap, em))
+    case Eval(h, e) =>
+      val (evalHeap, evalMask, checks, proofOrAssume) = fromEvalState(h);
+      val preGlobals = etran.FreshGlobals("eval")
+      val preEtran = new ExpressionTranslator(List(Boogie.VarExpr(preGlobals(0).id), Boogie.VarExpr(preGlobals(1).id)), currentClass);
+      BLocal(preGlobals(0)) :: (VarExpr(preGlobals(0).id) := evalHeap) ::
+      BLocal(preGlobals(1)) :: (VarExpr(preGlobals(1).id) := evalMask) ::
+      (if(check) checks else Nil) :::
+      bassume(IsGoodMask(preEtran.Mask)) ::
+      bassume(wf(preEtran.Heap, preEtran.Mask)) ::
+      bassert(proofOrAssume, p.pos, "Arguments for joinable might not match up.") ::
+      preEtran.Exhale(List((e, error)), "eval", check)
+    case e => (if(check) isDefined(e)(true) else Nil) ::: List(bassert(Tr(e), error.pos, error.message + " The expression at " + e.pos + " might not evaluate to true."))
+  }
+
+  def fromEvalState(h: EvalState): (Expr, Expr, List[Stmt], Expr) = {
+    h match {
+      case AcquireState(obj) => 
+        (AcquireHeap(Heap.select(Tr(obj), "held")), AcquireMask(Heap.select(Tr(obj), "held")), isDefined(obj)(true), true)
+      case ReleaseState(obj) => 
+        (LastSeenHeap(Heap.select(Tr(obj), "mu"), Heap.select(Tr(obj), "held")), LastSeenMask(Heap.select(Tr(obj), "mu"), Heap.select(Tr(obj), "held")), isDefined(obj)(true), true)
+      case CallState(token, obj, id, args) =>
+        val argsSeq = CallArgs(Heap.select(Tr(token), "joinable"));
+        
+        var i : int = 0;
+        (CallHeap(Heap.select(Tr(token), "joinable")), 
+         CallMask(Heap.select(Tr(token), "joinable")),
+         isDefined(token)(true) :::
+         isDefined(obj)(true) :::
+         (args flatMap { a => isDefined(a)(true)}) :::
+         bassert(CanRead(Tr(token), "joinable"), obj.pos, "Joinable field of the token might not be readable.") ::
+         bassert(Heap.select(Tr(token), "joinable") !=@ 0, obj.pos, "Token might not be active."),
+         (new MapSelect(argsSeq, 0) ==@ Tr(obj) ) &&
+         (((args zip (1 until args.length+1).toList) map { a => new MapSelect(argsSeq, a._2) ==@ Tr(a._1)}).foldLeft(true: Expr){ (a: Expr, b: Expr) => a && b})
+        )
+    }
+  }
+ 
+  // permissions
+
+  def CanRead(obj: Boogie.Expr, field: Boogie.Expr): Boogie.Expr = new Boogie.FunctionApp("CanRead", Mask, obj, field)
+  def CanRead(obj: Boogie.Expr, field: String): Boogie.Expr = CanRead(obj, new Boogie.VarExpr(field))
+  def CanWrite(obj: Boogie.Expr, field: Boogie.Expr): Boogie.Expr = new Boogie.FunctionApp("CanWrite", Mask, obj, field)
+  def CanWrite(obj: Boogie.Expr, field: String): Boogie.Expr = CanWrite(obj, new Boogie.VarExpr(field))
+  def HasNoPermission(obj: Boogie.Expr, field: String) =
+    (new Boogie.MapSelect(Mask, obj, field, "perm$R") ==@ Boogie.IntLiteral(0)) &&
+    (new Boogie.MapSelect(Mask, obj, field, "perm$N") ==@ Boogie.IntLiteral(0))
+  def SetNoPermission(obj: Boogie.Expr, field: String, mask: Boogie.Expr) =
+    Boogie.Assign(Boogie.MapSelect(mask, obj, field), Boogie.VarExpr("Permission$Zero"))
+  def HasFullPermission(obj: Boogie.Expr, field: String, mask: Boogie.Expr) =
+    (new Boogie.MapSelect(mask, obj, field, "perm$R") ==@ Boogie.IntLiteral(100)) &&
+    (new Boogie.MapSelect(mask, obj, field, "perm$N") ==@ Boogie.IntLiteral(0))
+  def SetFullPermission(obj: Boogie.Expr, field: String) =
+    Boogie.Assign(Boogie.MapSelect(Mask, obj, field), Boogie.VarExpr("Permission$Full"))
+
+  def IncPermission(obj: Boogie.Expr, field: String, howMuch: Boogie.Expr) =
+    MapUpdate3(Mask, obj, field, "perm$R", new Boogie.MapSelect(Mask, obj, field, "perm$R") + howMuch)
+  def IncPermissionEpsilon(obj: Boogie.Expr, field: String, epsilons: Boogie.Expr) =
+    if (epsilons != null) {
+      val g = (new Boogie.MapSelect(Mask, obj, field, "perm$N") !=@ Boogie.VarExpr("Permission$MinusInfinity")) &&
+              (new Boogie.MapSelect(Mask, obj, field, "perm$N") !=@ Boogie.VarExpr("Permission$PlusInfinity"))
+      Boogie.If(g, 
+        MapUpdate3(Mask, obj, field, "perm$N", new Boogie.MapSelect(Mask, obj, field, "perm$N") + epsilons) ::
+          bassume(Boogie.FunctionApp("wf", List(Heap, Mask))) :: Nil
+        , Nil)
+    } else {
+      val g = (new Boogie.MapSelect(Mask, obj, field, "perm$N") !=@ Boogie.VarExpr("Permission$MinusInfinity"))
+      Boogie.If(g, MapUpdate3(Mask, obj, field, "perm$N", Boogie.VarExpr("Permission$PlusInfinity")), Nil)
+    }
+
+  def DecPermission(obj: Boogie.Expr, field: String, howMuch: Boogie.Expr, mask: Boogie.Expr, error: ErrorMessage, pos: Position) = {
+    val xyz: Boogie.Expr = new Boogie.MapSelect(mask, obj, field, "perm$R")
+    bassert(howMuch <= xyz, error.pos, error.message + " Insufficient fraction at " + pos + " for " + field + ".") ::
+    MapUpdate3(mask, obj, field, "perm$R", new Boogie.MapSelect(mask, obj, field, "perm$R") - howMuch)
+  }
+  def DecPermissionEpsilon(obj: Boogie.Expr, field: String, epsilons: Boogie.Expr, mask: Boogie.Expr, error: ErrorMessage, pos: Position) =
+    if (epsilons != null) {
+      val g = (new Boogie.MapSelect(mask, obj, field, "perm$N") !=@ Boogie.VarExpr("Permission$MinusInfinity")) &&
+              (new Boogie.MapSelect(mask, obj, field, "perm$N") !=@ Boogie.VarExpr("Permission$PlusInfinity"))
+      val xyz = new Boogie.MapSelect(mask, obj, field, "perm$N")
+      bassert((new Boogie.MapSelect(mask, obj, field, "perm$R") ==@ Boogie.IntLiteral(0)) ==> (epsilons <= xyz), error.pos, error.message + " Insufficient epsilons at " + pos + "  for " + field + ".") ::
+      Boogie.If(g,
+         MapUpdate3(mask, obj, field, "perm$N", new Boogie.MapSelect(mask, obj, field, "perm$N") - epsilons) ::
+           bassume(Boogie.FunctionApp("wf", List(Heap, Mask))) :: Nil
+        , Nil)
+    } else {
+      val g = (new Boogie.MapSelect(mask, obj, field, "perm$N") !=@ Boogie.VarExpr("Permission$PlusInfinity"))
+      bassert((new Boogie.MapSelect(mask, obj, field, "perm$R") ==@ Boogie.IntLiteral(0)) ==>
+                    (new Boogie.MapSelect(mask, obj, field, "perm$N") ==@ Boogie.VarExpr("Permission$PlusInfinity")),  error.pos, error.message + " Insufficient epsilons at " + pos + " for " + field + ".") ::
+      Boogie.If(g, MapUpdate3(mask, obj, field, "perm$N", Boogie.VarExpr("Permission$MinusInfinity")), Nil)
+    }
+  var uniqueInt = 0;
+
+  def MapUpdate3(m: Boogie.Expr, arg0: Boogie.Expr, arg1: String, arg2: String, rhs: Boogie.Expr) = {
+    // m[a,b,c] := rhs
+    // m[a,b][c] := rhs
+    // m[a,b] := map[a,b][c := rhs]
+    val m01 = Boogie.MapSelect(m, arg0, arg1)
+    Boogie.Assign(m01, Boogie.MapStore(m01, arg2, rhs))
+  }
+
+  def DecPerm(m: Expr, e: Expr, f: Expr, i: Expr) = FunctionApp("DecPerm", List(m, e, f, i))
+  def DecEpsilons(m: Expr, e: Expr, f: Expr, i: Expr) = FunctionApp("DecEpsilons", List(m, e, f, i))
+  def IncPerm(m: Expr, e: Expr, f: Expr, i: Expr) = FunctionApp("IncPerm", List(m, e, f, i))
+  def IncEpsilons(m: Expr, e: Expr, f: Expr, i: Expr) = FunctionApp("IncEpsilons", List(m, e, f, i))
+
+  
+  def MaxLockIsBelowX(x: Boogie.Expr) = {  // maxlock << x
+    val (oV, o) = Boogie.NewBVar("o", tref, false)
+    new Boogie.Forall(oV,
+                      (isHeldInHeap(o, Heap)) ==>
+                      new Boogie.FunctionApp("MuBelow", Boogie.MapSelect(Heap, o, "mu"), x))
+  }
+  def MaxLockIsAboveX(x: Boogie.Expr) = {  // x << maxlock
+    val (oV, o) = Boogie.NewBVar("o", tref, false)
+    new Boogie.Exists(oV,
+                      (isHeldInHeap(o, Heap)) &&
+                      new Boogie.FunctionApp("MuBelow", x, Boogie.MapSelect(Heap, o, "mu")))
+  }
+  def MaxLockEqualsX(x: Boogie.Expr) = {  // maxlock == o.mu
+    // Note: Instead of the existential below, we could generate a nicer expression if we knew that
+    // x has the form y.mu--then, we'd replace the existential with y.held.  Another possibility
+    // would be if we had an inverse of .mu (such an inverse exists, but we're not encoding it).
+//    val (oV, o) = Boogie.NewBVar("o", tref, false)
+    //new Boogie.Exists(oV,
+    //                  (isHeldInHeap(o, Heap)) && (Boogie.MapSelect(Heap, o, "mu") ==@ x)) &&  
+    /*isHeldInHeap(x, Heap) &&*/ IsHighestLock(x)
+  }
+  def IsHighestLock(x: Boogie.Expr) = {
+    // (forall r :: r.held ==> r.mu << x || r.mu == x)
+    val (rV, r) = Boogie.NewBVar("r", tref, false)
+    new Boogie.Forall(rV,
+                      (isHeldInHeap(r, Heap)) ==>
+                      (new Boogie.FunctionApp("MuBelow", MapSelect(Heap, r, "mu"), x) ||
+                       (Boogie.MapSelect(Heap, r, "mu") ==@ x)))
+  }
+  def MaxLockPreserved = {  // old(maxlock) == maxlock
+    // I don't know what the best encoding of this conding is, so I'll try a disjunction.
+    // Disjunct b0 is easier to prove, but it is stronger than b1.
+
+    // (forall r: ref ::
+    //     old(Heap)[r,held] == Heap[r,held] &&
+    //     (Heap[r,held] ==> old(Heap)[r,mu] == Heap[r,mu]))
+    val (rV, r) = Boogie.NewBVar("r", tref, false)
+    val b0 = new Boogie.Forall(rV,
+                      ((0 < Boogie.MapSelect(oldEtran.Heap, r, "held")) ==@
+                       (0 < Boogie.MapSelect(Heap, r, "held"))) &&
+                      ((0 < Boogie.MapSelect(Heap, r, "held")) ==>
+                        (Boogie.MapSelect(oldEtran.Heap, r, "mu") ==@
+                         Boogie.MapSelect(Heap, r, "mu"))))
+
+    // (forall o, p ::
+    //     old(o.held) && (forall r :: old(r.held) ==> old(r.mu) << old(o.mu) || old(r.mu)==old(o.mu)) &&
+    //         p.held  && (forall r ::     r.held  ==>     r.mu  <<     p.mu  ||     r.mu ==    p.mu )
+    //     ==>
+    //     old(o.mu) == p.mu)
+    val (oV, o) = Boogie.NewBVar("o", tref, false)
+    val (pV, p) = Boogie.NewBVar("p", tref, false)
+    val b1 = new Boogie.Forall(List(oV,pV), List(),
+                  ((0 < Boogie.MapSelect(oldEtran.Heap, o, "held")) &&
+                   oldEtran.IsHighestLock(Boogie.MapSelect(oldEtran.Heap, o, "mu")) &&
+                   (0 < Boogie.MapSelect(Heap, p, "held")) &&
+                   IsHighestLock(Boogie.MapSelect(Heap, p, "mu")))
+                  ==>
+                  (Boogie.MapSelect(oldEtran.Heap, o, "mu") ==@ Boogie.MapSelect(Heap, p, "mu")))
+    b0 || b1
+  }
+  def TemporalMaxLockComparison(e0: ExpressionTranslator, e1: ExpressionTranslator) = {  // e0(maxlock) << e1(maxlock)
+    // (exists o ::
+    //     e1(o.held) &&
+    //     (forall r :: e0(r.held) ==> e0(r.mu) << e1(o.mu)))
+    val (oV, o) = Boogie.NewBVar("o", tref, false)
+    new Boogie.Exists(oV,
+                      (0 < Boogie.MapSelect(e0.Heap, o, "held")) &&
+                      e0.MaxLockIsBelowX(Boogie.MapSelect(e1.Heap, o, "mu")))
+  }
+
+  def fractionOk(expr: Expression) = {
+    bassert(0<=Tr(expr), expr.pos, "Fraction might be negative.") :: 
+    bassert(Tr(expr) <= 100, expr.pos, "Fraction might exceed 100.")
+  }
+}
+object S_ExpressionTranslator {
+  val Globals = {
+    ("Heap", theap) ::
+    ("Mask", tmask) ::
+    Nil
+  }
+}
+
+
+  // implicit 
+  implicit def string2VarExpr(s: String) = VarExpr(s)
+  implicit def expression2Expr(e: Expression) = etran.Tr(e)
+  implicit def field2Expr(f: Field) = VarExpr(f.FullName)
+
+  // prelude
+
+  def ModuleType = NamedType("ModuleName");
+  def ModuleName(cl: Class) = "module#" + cl.module.id;
+  def TypeName = NamedType("TypeName");
+  def FieldType(tp: BType) = IndexedType("Field", tp);
+  def bassert(e: Expr, pos: Position, msg: String) = {
+    val result = Boogie.Assert(e); result.pos = pos; result.message = msg; result
+  }
+  def bassume(e: Expr) = Boogie.Assume(e)
+  def BLocal(id: String, tp: BType) = new Boogie.LocalVar(id, tp)
+  def BLocal(x: Boogie.BVar) = Boogie.LocalVar(x)
+  def tArgSeq = NamedType("ArgSeq");
+  def tref = NamedType("ref");
+  def tbool = NamedType("bool");
+  def tmu  = NamedType("Mu");
+  def tint = NamedType("int");
+  def tseq(arg: BType) = IndexedType("Seq", arg)
+  def theap = NamedType("HeapType");
+  def tmask = NamedType("MaskType");
+  def ZeroMask = VarExpr("ZeroMask");
+  def HeapName = "Heap";
+  def MaskName = "Mask";
+  def Heap = VarExpr(HeapName);
+  def Mask = VarExpr(MaskName);
+  def GlobalNames = List(HeapName, MaskName);
+  def CanAssumeFunctionDefs = VarExpr("CanAssumeFunctionDefs");
+  def CurrentModule = VarExpr("CurrentModule");
+  def IsGoodState(e: Expr) = FunctionApp("IsGoodState", List(e));
+  def dtype(e: Expr) = FunctionApp("dtype", List(e))
+  def functionName(f: Function) = "#" + f.FullName;
+  def bnull = Boogie.Null();
+  def bLockBottom = VarExpr("$LockBottom")
+  def nonNull(e: Expr): Expr = e !=@ bnull
+  def isHeld(e: Expr): Expr = (0 < etran.Heap.select(e, "held"))
+  def isRdHeld(e: Expr): Expr = etran.Heap.select(e, "rdheld")
+  def isShared(e: Expr): Expr = etran.Heap.select(e, "mu") !=@ bLockBottom
+  def LastSeenHeap(sharedBit: Expr, heldBit: Expr) = FunctionApp("LastSeen$Heap", List(sharedBit, heldBit))
+  def LastSeenMask(sharedBit: Expr, heldBit: Expr) = FunctionApp("LastSeen$Mask", List(sharedBit, heldBit))
+  def AcquireHeap(heldBit: Expr) = FunctionApp("Acquire$Heap", List(heldBit))
+  def AcquireMask(heldBit: Expr) = FunctionApp("Acquire$Mask", List(heldBit))
+  def CallHeap(joinableBit: Expr) = FunctionApp("Call$Heap", List(joinableBit))
+  def CallMask(joinableBit: Expr) = FunctionApp("Call$Mask", List(joinableBit))
+  def CallArgs(joinableBit: Expr) = FunctionApp("Call$Args", List(joinableBit))
+  def submask(m1: Expr, m2: Expr) = FunctionApp("submask", List(m1, m2))
+
+object TranslationHelper {
+  def wf(h: Expr, m: Expr) = FunctionApp("wf", List(h, m));
+  def IsGoodMask(m: Expr) = FunctionApp("IsGoodMask", List(m))
+  def IsGoodInhaleState(a: Expr, b: Expr, c: Expr) = FunctionApp("IsGoodInhaleState", List(a, b, c))
+  def isHeldInHeap(e: Expr, h: Expr) = 0 < h.select(e, "held")
+  def NonEmptyMask(m: Expr) = ! FunctionApp("EmptyMask", List(m))
+  def NonPredicateField(f: String) = FunctionApp("NonPredicateField", List(VarExpr(f)))
+  def PredicateField(f: String) = FunctionApp("PredicateField", List(VarExpr(f)))
+  def createEmptySeq = FunctionApp("Seq#Empty", List())
+  def createSingletonSeq(e: Expr) = FunctionApp("Seq#Singleton", List(e)) 
+  def createAppendSeq(a: Expr, b: Expr) = FunctionApp("Seq#Append", List(a, b)) 
+  def createRange(min: Expr, max: Expr) = FunctionApp("Seq#Range", List(min, max))
+  def cast(a: Expr, b: Expr) = FunctionApp("cast", List(a, b))
+
+  // implicit conversions
+  implicit def bool2Bool(b: Boolean): Boogie.BoolLiteral = Boogie.BoolLiteral(b)
+  implicit def int2Int(n: int): Boogie.IntLiteral = Boogie.IntLiteral(n)
+  implicit def lift(s: Boogie.Stmt): List[Boogie.Stmt] = List(s)
+  implicit def type2BType(tp: Type): BType = {
+    val cl = tp.typ;
+    if(cl.IsRef) {
+      tref
+    } else if(cl.IsBool) {
+      tbool
+    } else if(cl.IsMu) {
+      tmu
+    } else if(cl.IsInt) {
+      tint
+    } else if(cl.IsSeq) {
+      tseq(type2BType(new Type(cl.asInstanceOf[SeqClass].parameter)))
+    } else {
+      assert(false); null
+    }
+  }
+  implicit def decl2DeclList(decl: Decl): List[Decl] = List(decl)
+  implicit def function2RichFunction(f: Function) = RichFunction(f);
+
+  case class RichFunction(f: Function) {
+    def apply(args: List[Expr]) = {
+      FunctionApp(functionName(f), args)
+    }
+  }
+
+  def Variable2BVar(v: Variable) = new Boogie.BVar(v.UniqueName, Boogie.ClassType(v.t.typ))
+  def Variable2BVarWhere(v: Variable) = NewBVarWhere(v.UniqueName, v.t)
+  def NewBVarWhere(id: String, tp: Type) = {
+    new Boogie.BVar(id, Boogie.ClassType(tp.typ)){
+      override val where = TypeInformation(new Boogie.VarExpr(id), tp) }
+  }
+
+  // scale an expression by a fraction
+  def FractionOf(expr: Expression, fraction: Expression) : Expression = {
+    val result = expr match {
+      case Access(e, None) => Access(e, Some(fraction))
+      case And(lhs, rhs) => And(FractionOf(lhs, fraction), FractionOf(rhs, fraction))
+      case _ if ! expr.isInstanceOf[PermissionExpr] => expr
+      case _ => throw new Exception("  " + expr.pos + ": Scaling non-full permissions is not supported yet." + expr);
+    }
+    result.pos = expr.pos;
+    result
+  }
+
+  def canTakeFractionOf(expr: Expression): Boolean = {
+    expr match {
+      case Access(e, None) => true
+      case And(lhs, rhs) => canTakeFractionOf(lhs) && canTakeFractionOf(rhs)
+      case _ if ! expr.isInstanceOf[PermissionExpr] => true
+      case _ => false
+    }
+  }
+
+  // scale an expression by a number of epsilons
+  def EpsilonsOf(expr: Expression, nbEpsilons: Expression) : Expression = {
+    val result = expr match {
+      case Access(e, _) => RdAccess(e, Some(Some(nbEpsilons)))
+      case And(lhs, rhs) => And(FractionOf(lhs, nbEpsilons), FractionOf(rhs, nbEpsilons))
+      case _ if ! expr.isInstanceOf[PermissionExpr] => expr
+      case _ => throw new Exception("  " + expr.pos + ": Scaling non-full permissions is not supported yet." + expr);
+    }
+    result.pos = expr.pos;
+    result
+  }
+
+  def canTakeEpsilonsOf(expr: Expression): Boolean = {
+    expr match {
+      case Access(e, _) => true
+      case And(lhs, rhs) => canTakeEpsilonsOf(lhs) && canTakeEpsilonsOf(rhs)
+      case _ if ! expr.isInstanceOf[PermissionExpr] => true
+      case _ => false
+    }
+  }
+
+  def TrType(cl: Class) = Boogie.VarExpr(cl.id + "#t")
+
+  def TypeInformation(e: Boogie.Expr, t: Type): Boogie.Expr = {
+    if (t.typ.IsRef) {
+      (e ==@ Boogie.Null()) || (new Boogie.FunctionApp("dtype", e) ==@ TrType(t.typ))
+    } else {
+      true
+    }
+  }
+  
+  def Version(expr: Expression, etran: ExpressionTranslator): Boogie.Expr =  
+  { 
+    expr match{
+      case pred@MemberAccess(e, p) if pred.isPredicate =>
+        Version(Access(pred, None), etran)
+      case acc@Access(e,perm) =>
+        val memberName = if(e.isPredicate) e.predicate.FullName else e.f.FullName;
+        Boogie.MapSelect(etran.Heap, etran.Tr(e.e), memberName)
+      case rd@RdAccess(e,perm) =>
+        val memberName = if(e.isPredicate) e.predicate.FullName else e.f.FullName;
+        Boogie.MapSelect(etran.Heap, etran.Tr(e.e), memberName)
+      case Implies(e0,e1) =>
+        Boogie.Ite(etran.Tr(e0), Version(e1, etran), 0)
+      case And(e0,e1) =>
+        Boogie.FunctionApp("combine", List(Version(e0, etran), Version(e1, etran)))
+      case IfThenElse(con, then, els) =>
+        Boogie.Ite(etran.Tr(con), Version(then, etran), Version(els, etran))
+      case e => Boogie.VarExpr("nostate")
+    }
+  }
+  def FieldTp(f: Field): String = {
+    f match {
+      case SpecialField("mu", _) => "Mu"
+      case SpecialField("held", _) => "int"
+      case SpecialField("rdheld", _) => "bool"
+      case SpecialField("joinable", _) => "int"
+      case f: Field => TrClass(f.typ.typ)
+    }
+  }
+
+  def TrClass(tp: Class): String = {
+    tp.id match {
+      case "int" => "int"
+      case "bool" => "bool"
+      case "$Mu" => "Mu"
+      case _ => if(tp.IsSeq) "seq" else "ref"
+    }
+  }
+  def Preconditions(spec: List[Specification]): List[Expression] = {
+    val result = spec flatMap ( s => s match {
+      case Precondition(e) => List(e)
+      case _ => Nil });
+    if(autoMagic) {
+     automagic(result.foldLeft(BoolLiteral(true): Expression)({ (a, b) => And(a, b)}), Nil)._1 ::: result
+    } else {
+      result
+    }
+  }
+  def Postconditions(spec: List[Specification]): List[Expression] = {
+    val result = spec flatMap ( s => s match {
+      case Postcondition(e) => List(e)
+      case _ => Nil })
+    if(autoMagic) {
+      automagic(result.foldLeft(BoolLiteral(true): Expression)({ (a, b) => And(a, b)}), Nil)._1 ::: result
+    } else {
+      result
+    }
+  }
+
+  def automagic(expr: Expression, handled: List[Expression]): (/*assumptions*/ List[Expression], /*newHandled*/List[Expression]) = {
+    def isHandled(e: Expression) = handled exists { ex => ex.equals(e) }
+    expr match {
+      case ma@MemberAccess(obj, f) =>
+        val (assumptions, handled1) = automagic(obj, handled);
+        if(isHandled(ma)) {
+          (assumptions, handled1)
+        } else {
+          if(ma.isPredicate){
+            // assumption: obj!=null
+            (assumptions ::: Neq(obj, NullLiteral()) :: Nil, handled1 + ma)
+          } else {
+            // assumption: obj!=null && acc(obj, f)
+            (assumptions ::: Neq(obj, NullLiteral()) :: Access(ma, None) :: Nil, handled1 + ma)
+          }
+        }
+      case Access(ma@MemberAccess(obj, f), perm) => 
+        val (assumptions, handled1) = automagic(obj, handled + ma);
+        perm match {
+          case None => (assumptions, handled1);
+          case Some(fraction) => val result = automagic(fraction, handled1); (assumptions ::: result._1, result._2)
+        }
+      case RdAccess(ma@MemberAccess(obj, f), perm) =>
+        val (assumptions, handled1) = automagic(obj, handled + ma);
+        perm match {
+          case None => (assumptions, handled1);
+          case Some(None) => (assumptions, handled1);
+          case Some(Some(epsilon)) => val result = automagic(epsilon, handled1); (assumptions ::: result._1, result._2)
+        }
+      case AccessAll(obj, perm) => 
+        automagic(obj, handled)
+      case RdAccessAll(obj, perm) => 
+        automagic(obj, handled)
+      case Holds(e) =>
+        automagic(e, handled)
+      case RdHolds(e) =>
+        automagic(e, handled)
+      case a: Assigned =>
+       (Nil, handled)
+      case Old(e) =>
+       (Nil, handled) // ??
+      case IfThenElse(con, then, els) =>
+        val (assumptions, handled1) = automagic(con, handled);
+        val (assumptions2, handled2) = automagic(then, handled1);
+        val result = automagic(els, handled2); 
+        (assumptions ::: assumptions2 ::: result._1, result._2)
+      case Not(e) =>
+        automagic(e, handled)
+      case func@FunctionApplication(obj, id, args) =>
+        var assumption = Nil: List[Expression];
+        var newHandled = handled;
+        for(a <- obj :: args) {
+          val (ass, hd) = automagic(a, handled);
+          assumption = assumption ::: ass;
+          newHandled = hd;
+        }
+        (assumption, newHandled)
+      case uf@Unfolding(_, e) =>
+        (Nil, handled)
+      case bin: BinaryExpr =>
+        val (assumptions, handled1) = automagic(bin.E0, handled);
+        val result = automagic(bin.E1, handled1); 
+        (assumptions ::: result._1, result._2)
+      case q@Forall(is, Range(min, max), e) =>
+        (Nil, handled)
+      case q@Forall(is, seq, e) =>
+        (Nil, handled)
+      case EmptySeq(t) =>
+        (Nil, handled)
+      case ExplicitSeq(es) =>
+        var assumption = Nil: List[Expression];
+        var newHandled = handled;
+        for(a <- es) {
+          val (ass, hd) = automagic(a, handled);
+          assumption = assumption ::: ass;
+          newHandled = hd;
+        }
+        (assumption, newHandled)
+      case Range(min, max) =>
+        val (assumptions, handled1) = automagic(min, handled);
+        val result = automagic(max, handled1); 
+        (assumptions ::: result._1, result._2)
+      case Length(e) =>
+        automagic(e, handled)
+      case Eval(h, e) =>
+        (Nil, handled)
+      case _ => (Nil, handled)
+    }
+  }
+
+  def DefinitionOf(predicate: Predicate): Expression = {
+    if(autoMagic) {
+      And(automagic(predicate.definition, Nil)._1.foldLeft(BoolLiteral(true): Expression)({ (a, b) => And(a, b)}), predicate.definition)
+    } else {
+      predicate.definition
+    }
+  }
+
+  def LockChanges(spec: List[Specification]): List[Expression] = {
+    spec flatMap ( s => s match {
+      case LockChange(ee) => ee
+      case _ => Nil })
+  }
+
+  def SubstRd(e: Expression): Expression = e match {
+    case Access(e,_) =>
+      val r = RdAccess(e,None); r.typ = BoolClass; r
+    case e: RdAccess => e
+    case Implies(e0,e1) =>
+      val r = Implies(e0, SubstRd(e1)); r.typ = BoolClass; r
+    case And(e0,e1) =>
+      val r = And(SubstRd(e0), SubstRd(e1)); r.typ = BoolClass; r
+    case e => e
+   }
+ }
+
+  def UnfoldPredicatesWithReceiverThis(expr: Expression): Expression = {
+    def unfoldPred(e: Expression): Expression = {
+      e match {
+        case pred@MemberAccess(o, f) if pred.isPredicate && o.isInstanceOf[ThisExpr] =>
+          SubstThis(DefinitionOf(pred.predicate), o)
+        case Access(pred@MemberAccess(o, f), p) if pred.isPredicate && o.isInstanceOf[ThisExpr] =>
+          p match {
+            case None => SubstThis(DefinitionOf(pred.predicate), o)
+            case Some(p) => FractionOf(SubstThis(DefinitionOf(pred.predicate), o), p)
+          }
+        case RdAccess(pred@MemberAccess(o, f), p) if pred.isPredicate && o.isInstanceOf[ThisExpr] =>
+          p match {
+            case None => EpsilonsOf(SubstThis(DefinitionOf(pred.predicate), o), IntLiteral(1))
+            case Some(None) => throw new Exception("not supported yet")
+            case Some(Some(p)) => EpsilonsOf(SubstThis(DefinitionOf(pred.predicate), o), p)
+          }
+        case func@FunctionApplication(obj: ThisExpr, name, args) if 2<=TranslationOptions.defaults =>
+          SubstThisAndVars(func.f.definition, obj, func.f.ins, args) 
+        case _ => manipulate(e, {ex => unfoldPred(ex)})
+      }
+    }
+    unfoldPred(expr)
+  }
+
+  // needed to do a _simultaneous_ substitution!
+  def SubstThisAndVars(expr: Expression, thisReplacement: Expression, vs: List[Variable], xs: List[Expression]): Expression = {
+    def replace(e: Expression): Expression = {
+      e match {
+        case _: ThisExpr => thisReplacement
+        case e: VariableExpr => 
+          for ((v,x) <- vs zip xs if v == e.v) { return x }
+          e
+        case q@Forall(is, seq, e) => 
+          val sub = vs zip xs filter { xv => is forall { variable => ! variable.id.equals(xv._1)}};
+          val result = Forall(is, SubstThisAndVars(seq, thisReplacement, vs, xs), SubstThisAndVars(e, thisReplacement, sub map { x => x._1}, sub map { x => x._2}));
+          result.variables = q.variables;
+          result
+        case _ => manipulate(e, {ex => replace(ex)})
+      }
+    }
+    replace(expr)
+  }
+
+  def SubstThis(expr: Expression, x: Expression): Expression = {
+    def replaceThis(e: Expression): Expression = {
+      e match {
+        case _: ThisExpr => x
+        case _ => manipulate(e, {ex => replaceThis(ex)})
+      }
+    }
+    replaceThis(expr)
+  }
+
+  def SubstResult(expr: Expression, x: Expression): Expression = {
+    def replaceThis(e: Expression): Expression = {
+      e match {
+        case _: Result => x
+        case _ => manipulate(e, {ex => replaceThis(ex)})
+      }
+    }
+    replaceThis(expr)
+  }
+
+  def SubstVars(expr: Expression, vs: List[Variable], xs: List[Expression]): Expression = {
+    def replaceThis(e: Expression): Expression = {
+      e match {
+        case e: VariableExpr => 
+          for ((v,x) <- vs zip xs if v == e.v) { return x }
+          e
+        case q@Forall(is, seq, e) => 
+          val sub = vs zip xs filter { xv => is forall { variable => ! variable.id.equals(xv._1)}};
+          val result = Forall(is, SubstVars(seq, vs, xs), SubstVars(e, sub map { x => x._1}, sub map { x => x._2}));
+          result.variables = q.variables;
+          result
+        case _ => manipulate(e, {ex => replaceThis(ex)})
+      }
+    }
+    replaceThis(expr)
+  }
+  
+  def manipulate(expr: Expression, func: Expression => Expression): Expression = {
+    val result = expr match {
+      case e: Literal => expr
+      case _:ThisExpr => expr
+      case _:Result => expr
+      case e:VariableExpr => expr
+      case acc@MemberAccess(e,f) =>
+        val g = MemberAccess(func(e), f); g.f = acc.f; g.predicate = acc.predicate; g.isPredicate = acc.isPredicate; g
+      case Access(e, perm) =>
+        Access(func(e).asInstanceOf[MemberAccess],
+             perm match { case None => perm case Some(perm) => Some(func(perm)) })
+      case RdAccess(e, perm) =>
+        RdAccess(func(e).asInstanceOf[MemberAccess],
+               perm match { case Some(Some(p)) => Some(Some(func(p))) case _ => perm })
+      case AccessAll(obj, perm) =>
+        AccessAll(func(obj),
+             perm match { case None => perm case Some(perm) => Some(func(perm)) })
+      case RdAccessAll(obj, perm) =>
+        RdAccessAll(func(obj),
+               perm match { case Some(Some(p)) => Some(Some(func(p))) case _ => perm })
+      case Holds(e) => Holds(func(e))
+      case RdHolds(e) => RdHolds(func(e))
+      case e: Assigned => e
+      case Old(e) => Old(func(e))
+      case IfThenElse(con, then, els) => IfThenElse(func(con), func(then), func(els))
+      case Not(e) => Not(func(e))
+      case funapp@FunctionApplication(obj, id, args) =>
+        val appl = FunctionApplication(func(obj), id, args map { arg => func(arg)}); appl.f = funapp.f; appl
+      case Unfolding(pred, e) =>
+        Unfolding(func(pred).asInstanceOf[PermissionExpr], func(e))
+      case Iff(e0,e1) => Iff(func(e0), func(e1))
+      case Implies(e0,e1) => Implies(func(e0), func(e1))
+      case And(e0,e1) => And(func(e0), func(e1))
+      case Or(e0,e1) => Or(func(e0), func(e1))
+      case Eq(e0,e1) => Eq(func(e0), func(e1))
+      case Neq(e0,e1) => Neq(func(e0), func(e1))
+      case Less(e0,e1) => Less(func(e0), func(e1))
+      case AtMost(e0,e1) => AtMost(func(e0), func(e1))
+      case AtLeast(e0,e1) => AtLeast(func(e0), func(e1))
+      case Greater(e0,e1) => Greater(func(e0), func(e1))
+      case LockBelow(e0,e1) => LockBelow(func(e0), func(e1))
+      case Plus(e0,e1) => Plus(func(e0), func(e1))
+      case Minus(e0,e1) => Minus(func(e0), func(e1))
+      case Times(e0,e1) => Times(func(e0), func(e1))
+      case Div(e0,e1) => Div(func(e0), func(e1))
+      case Mod(e0,e1) => Mod(func(e0), func(e1))
+      case forall@Forall(i, seq, e) => val result = Forall(i, func(seq), func(e)); result.variables = forall.variables; result
+      case ExplicitSeq(es) =>
+        ExplicitSeq(es map { e => func(e) })
+      case Range(min, max)=>
+        Range(func(min), func(max))
+      case Append(e0, e1) =>
+        Append(func(e0), func(e1))
+      case At(e0, e1) =>
+        At(func(e0), func(e1))
+      case Drop(e0, e1) =>
+        Drop(func(e0), func(e1))
+      case Take(e0, e1) =>
+        Take(func(e0), func(e1))
+      case Length(e) =>
+        Length(func(e))
+      case Eval(h, e) =>
+        Eval(h match { 
+          case AcquireState(obj) => AcquireState(func(obj)) 
+          case ReleaseState(obj) => ReleaseState(func(obj)) 
+          case CallState(token, obj, i, args) => CallState(func(token), func(obj), i, args map { a => func(a)})
+        }, func(e)) 
+    }
+    if(result.typ == null) {
+      result.typ = expr.typ;
+    }
+    result.pos = expr.pos
+    result
+  }
+
+}