Chalice: added sequence containment surface syntax ("in" comparison operator); cleaned up some deprecation warnings; resolved ambiguity with "unfolding ... in" expression

6 files changed, 87 insertions, 67 deletions

diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala
index 9ca324d7..065c03ff 100644
--- a/Chalice/src/Ast.scala
+++ b/Chalice/src/Ast.scala
@@ -23,15 +23,15 @@ sealed case class Class(classId: String, parameters: List[Class], module: String
     } 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 IsChannel: boolean = false

-  def IsState: boolean = false

+  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 IsChannel: Boolean = false

+  def IsState: Boolean = false

   def IsNormalClass = true;

   var IsExternal = false;  // says whether or not to compile the class (compilation ignores external classes)

 

@@ -115,7 +115,7 @@ sealed case class TokenType(C: Type, m: String) extends Type("token", Nil) {  //
 // members

 

 sealed abstract class Member extends ASTNode {

-  val Hidden: boolean = false  // hidden means not mentionable in source

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

@@ -124,7 +124,7 @@ sealed abstract class NamedMember(id: String) extends Member {
   def FullName = Parent.id + "." + Id

 }

 case class Field(id: String, typ: Type) extends NamedMember(id) {

-  val IsGhost: boolean = false

+  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

@@ -142,8 +142,8 @@ case class Condition(id: String, where: Option[Expression]) extends NamedMember(
 class Variable(name: String, typ: Type) extends ASTNode {

   val id = name

   val t = typ

-  val IsGhost: boolean = false

-  val IsImmutable: boolean = false

+  val IsGhost: Boolean = false

+  val IsImmutable: Boolean = false

   val UniqueName = {

     val n = S_Variable.VariableCount

     S_Variable.VariableCount = S_Variable.VariableCount + 1

@@ -152,7 +152,7 @@ class Variable(name: String, typ: Type) extends ASTNode {
 }

 object S_Variable { var VariableCount = 0 }

 class ImmutableVariable(id: String, t: Type) extends Variable(id, t) {

-  override val IsImmutable: boolean = true

+  override val IsImmutable: Boolean = true

 }

 class SpecialVariable(name: String, typ: Type) extends Variable(name, typ) {

   override val UniqueName = name

@@ -182,14 +182,14 @@ case class WhileStmt(guard: Expression,
 }

 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 {

+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(declaresLocal: List[boolean], lhs: List[VariableExpr], obj: Expression, id: String, args: List[Expression]) extends Statement {

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

   var locals = List[Variable]()

   var m: Method = null

 }

@@ -201,9 +201,9 @@ 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 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 {

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

   var local: Variable = null

   var m: Method = null

 }

@@ -213,12 +213,12 @@ case class JoinAsync(lhs: List[VariableExpr], token: Expression) extends Stateme
 case class Wait(obj: Expression, id: String) extends Statement {

   var c: Condition = null

 }

-case class Signal(obj: Expression, id: String, all: boolean) extends Statement {

+case class Signal(obj: Expression, id: String, all: Boolean) extends Statement {

   var c: Condition = null

 }

 case class Send(ch: Expression, args: List[Expression]) extends Statement {

 }

-case class Receive(declaresLocal: List[boolean], ch: Expression, outs: List[VariableExpr]) extends Statement {

+case class Receive(declaresLocal: List[Boolean], ch: Expression, outs: List[VariableExpr]) extends Statement {

   var locals = List[Variable]()

 }

 case class Fold(pred: PermissionExpr) extends Statement

@@ -235,25 +235,25 @@ case class Init(id: String, e: Expression) extends ASTNode {
 }

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

   def Resolve(vr: Variable) = { v = vr; typ = vr.t.typ }

 }

-case class Result extends Expression

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

@@ -394,6 +394,9 @@ case class Drop(s: Expression, n: Expression) extends SeqAccess(s, n) {
 case class Take(s: Expression, n: Expression) extends SeqAccess(s, n) {

   override val OpName = ""

 }

+case class Contains(s: Expression, n: Expression) extends SeqAccess(s, n) {

+  override val OpName = "in"

+}

 

 

 // eval

diff --git a/Chalice/src/Boogie.scala b/Chalice/src/Boogie.scala
index f889609f..9d290aa5 100644
--- a/Chalice/src/Boogie.scala
+++ b/Chalice/src/Boogie.scala
@@ -9,7 +9,7 @@ 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 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

@@ -69,7 +69,7 @@ object Boogie {
    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 BoolLiteral(b: Boolean) extends Expr

  case class Null extends Expr

  case class VarExpr(id: String) extends Expr {

    def this(v: BVar) = this(v.id)

@@ -99,7 +99,7 @@ object Boogie {
  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) =

+   def this(id: String, t: BType, uniquifyName: Boolean) =

      this(if (uniquifyName) {

             val n = S_BVar.VariableCount

             S_BVar.VariableCount = S_BVar.VariableCount + 1

@@ -110,13 +110,13 @@ object Boogie {
    val where: Expr = null

  }

  object S_BVar { var VariableCount = 0 }

- def NewBVar(id: String, t: BType, uniquifyName: boolean) = {

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

+   def this(id: String, uniquifyName: Boolean) =

      this(if (uniquifyName) {

             val n = S_TVar.VariableCount

             S_TVar.VariableCount = S_TVar.VariableCount + 1

@@ -233,7 +233,7 @@ object Boogie {
  def PrintExpr(e: Expr): String = {

    PrintExpr(e, false)

  }

- def PrintExpr(e: Expr, useParens: boolean): String = e match {

+ def PrintExpr(e: Expr, useParens: Boolean): String = e match {

    case IntLiteral(n) => n.toString

    case BoolLiteral(b) => b.toString

    case Null() => "null"

diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala
index 12a989d7..097526b0 100644
--- a/Chalice/src/Parser.scala
+++ b/Chalice/src/Parser.scala
@@ -32,13 +32,13 @@ class Parser extends StandardTokenParsers {
                        "int", "bool", "false", "true", "null", "waitlevel", "lockbottom",

                        "module", "external",

                        "predicate", "function", "free", "send", "receive",

-                       "ite", "fold", "unfold", "unfolding", "in", "forall", "exists", 

+                       "ite", "fold", "unfold", "unfolding", "in", "forall", "exists",

                        "seq", "nil", "result", "eval", "token",

                        "wait", "signal")

   // todo: can we remove "nil"?

   lexical.delimiters += ("(", ")", "{", "}", "[[", "]]",

                          "<==>", "==>", "&&", "||",

-                         "==", "!=", "<", "<=", ">=", ">", "<<",

+                         "==", "!=", "<", "<=", ">=", ">", "<<", "in", "!in",

                          "+", "-", "*", "/", "%", "!", ".", "..",

                          ";", ":", ":=", ",", "?", "|", "[", "]", "++", "::")

 

@@ -95,11 +95,11 @@ class Parser extends StandardTokenParsers {
     ("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) =

+  def formalParameters(immutable: Boolean) =

     "(" ~> (formalList(immutable) ?) <~ ")" ^^ {

       case None => Nil

       case Some(ids) => ids }

-  def formalList(immutable: boolean) = {

+  def formalList(immutable: Boolean) = {

     def MVar(id: String, t: Type) = {

       currentLocalVariables = currentLocalVariables + id

       if (immutable) new ImmutableVariable(id,t) else new Variable(id,t)

@@ -220,7 +220,7 @@ class Parser extends StandardTokenParsers {
           val lhs = ExtractList(outs)

           Receive(declareImplicitLocals(lhs), e, lhs) }

     )

-  def localVarStmt(const: boolean, ghost: boolean) =

+  def localVarStmt(const: Boolean, ghost: Boolean) =

       idTypeOpt ~ (":=" ~> Rhs ?) <~ Semi ^^ {

         case (id,optT) ~ rhs =>

           currentLocalVariables = currentLocalVariables + id

@@ -345,8 +345,10 @@ class Parser extends StandardTokenParsers {
           case e0 ~ Some(">=" ~ e1) => AtLeast(e0,e1)

           case e0 ~ Some(">" ~ e1) => Greater(e0,e1)

           case e0 ~ Some("<<" ~ e1) => LockBelow(e0,e1)

+          case e0 ~ Some("in" ~ e1) => Contains(e0, e1)

+          case e0 ~ Some("!in" ~ e1) => Not(Contains(e0, e1))

         })

-  def CompareOp = "==" | "!=" | "<" | "<=" | ">=" | ">" | "<<"

+  def CompareOp = "==" | "!=" | "<" | "<=" | ">=" | ">" | "<<" | "in" | "!in"

   def concatExpr =

     positioned(addExpr ~ ("++" ~> addExpr *) ^^ {

           case e0 ~ rest => (rest foldLeft e0) {

@@ -450,7 +452,7 @@ class Parser extends StandardTokenParsers {
     | "holds" ~> "(" ~> expression <~ ")" ^^ Holds

     | "assigned" ~> "(" ~> ident <~ ")" ^^ Assigned

     | "old" ~> "(" ~> expression <~ ")" ^^ Old

-    | ("unfolding" ~> expression <~ "in") ~ expression ^? { 

+    | ("unfolding" ~> suffixExpr <~ "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) 

       }

diff --git a/Chalice/src/PrettyPrinter.scala b/Chalice/src/PrettyPrinter.scala
index bcf51826..84d4df31 100644
--- a/Chalice/src/PrettyPrinter.scala
+++ b/Chalice/src/PrettyPrinter.scala
@@ -195,7 +195,7 @@ object PrintProgram {
     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 {

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

@@ -284,6 +284,7 @@ object PrintProgram {
       Expr(s); print("["); Expr(n); print(" ..]");

     case Take(s, n) =>

       Expr(s); print("[.. "); Expr(n); print("]");

+    case e:Contains => BinExpr(e, e.OpName, 0x40, true, true, contextBindingPower, fragileContext)      

     case Eval(h, e) =>

       print("eval("); (h match 

         { 

@@ -292,17 +293,17 @@ object PrintProgram {
           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 {

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

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

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

diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala
index 4b702a8e..73b248e3 100644
--- a/Chalice/src/Resolver.scala
+++ b/Chalice/src/Resolver.scala
@@ -8,7 +8,7 @@ import scala.util.parsing.input.Positional
 

 object Resolver {

  sealed abstract class ResolverOutcome

- case class Success extends ResolverOutcome

+ case class Success() extends ResolverOutcome

  case class Errors(ss: List[(Position,String)]) extends ResolverOutcome

 

  var seqClasses = Map[String, SeqClass]();

@@ -26,14 +26,14 @@ object Resolver {
      new LProgramContext(v, this);

    }

    def LookupVariable(id: String): Option[Variable] = None

-   def IsVariablePresent(vr: Variable): boolean = false

+   def IsVariablePresent(vr: Variable): Boolean = false

 

    private class LProgramContext(v: Variable, parent: ProgramContext) extends ProgramContext(parent.Decls, 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 = {

+     override def IsVariablePresent(vr: Variable): Boolean = {

        if (vr == v) true else parent.IsVariablePresent(vr)

      }

      override def CurrentMember() = {

@@ -163,7 +163,7 @@ object Resolver {
    }

  }

 

- def ResolveType(t: Type, context: ProgramContext): unit = {

+ def ResolveType(t: Type, context: ProgramContext): Unit = {

      for(p <- t.params){

        ResolveType(p, context);

      }

@@ -209,7 +209,7 @@ object Resolver {
    }

  }

 

- def ResolveStmt(s: Statement, context: ProgramContext): unit = s match {

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

@@ -490,7 +490,7 @@ object Resolver {
      }

  }

 

- def ResolveLHS(declaresLocal: List[boolean], actuals: List[VariableExpr], formals: List[Variable], context: ProgramContext): List[Variable] = {

+ def ResolveLHS(declaresLocal: List[Boolean], actuals: List[VariableExpr], formals: List[Variable], context: ProgramContext): List[Variable] = {

    var locals = List[Variable]()

    var vars = Set[Variable]()

    var ctx = context

@@ -557,7 +557,7 @@ object Resolver {
 

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

+                 twoStateContext: Boolean, specContext: Boolean)(implicit inPredicate: Boolean): Unit = e match {

    case e @ NewRhs(id, initialization, lower, upper) =>

      if (context.Decls contains id) {

        context.Decls(id) match {

@@ -766,6 +766,12 @@ object Resolver {
      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 contains@Contains(e0, e1) =>

+     ResolveExpr(e0, context, twoStateContext, false);

+     ResolveExpr(e1, context, twoStateContext, false);

+     if(! e1.typ.IsSeq) context.Error(contains.pos, "RHS operand of 'in' must be sequence. (found: " + e1.typ.FullName + ").");

+     if(e0.typ ne e1.typ.parameters(0)) context.Error(contains.pos, "LHS operand's type must be element type of sequence. (found: " + e0.typ.FullName + ", expected: " + e1.typ.parameters(0).FullName + ").");

+     contains.typ = BoolClass;

    case bin: BinaryExpr =>

      ResolveExpr(bin.E0, context, twoStateContext, specContext && bin.isInstanceOf[And])

      ResolveExpr(bin.E1, context, twoStateContext, specContext && (bin.isInstanceOf[And] || bin.isInstanceOf[Implies]))

@@ -919,7 +925,7 @@ object Resolver {
    specOk(expr)

  }

 

- def CheckRunSpecification(e: Expression, context: ProgramContext, allowMaxLock: boolean): unit = e match {

+ 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 waitlevel here")

    case _:Literal =>

diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index 5039395b..1983b034 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -906,7 +906,7 @@ class Translator {
      bassume(!guard)))

   }

 

-  def UpdateMu(o: Expr, allowOnlyFromBottom: boolean, justAssumeValue: boolean,

+  def UpdateMu(o: Expr, allowOnlyFromBottom: Boolean, justAssumeValue: 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

@@ -1045,7 +1045,7 @@ class Translator {
   def isDefined(e: Expression) = etran.isDefined(e)(true)

   def TrExpr(e: Expression) = etran.Tr(e)

 

-  def InhaleInvariants(obj: Expression, readonly: boolean, tran: ExpressionTranslator) = {

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

@@ -1053,7 +1053,7 @@ class Translator {
            (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) = {

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

@@ -1061,7 +1061,7 @@ class Translator {
            (inv => SubstThis(inv.e, sh)) map

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

   }

-  def InhaleInvariants(obj: Expression, readonly: boolean) = {

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

@@ -1069,7 +1069,7 @@ class Translator {
            (inv => SubstThis(inv.e, sh)) map

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

   }

-  def ExhaleInvariants(obj: Expression, readonly: boolean, msg: ErrorMessage) = {

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

@@ -1105,7 +1105,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
   def this(cl: Class) = this(for ((id,t) <- S_ExpressionTranslator.Globals) yield Boogie.VarExpr(id), cl)

 

   def Globals = List(Heap, Mask, Credits)

-  def ChooseEtran(chooseOld: boolean) = if (chooseOld) oldEtran else this

+  def ChooseEtran(chooseOld: Boolean) = if (chooseOld) oldEtran else this

   // Create a list of fresh global variables

   def FreshGlobals(prefix: String) = {

     new Boogie.BVar(prefix + HeapName, theap, true) ::

@@ -1271,13 +1271,21 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
       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."))

+        isDefined(e0) ::: isDefined(e1) :::

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

+        isDefined(e0) ::: isDefined(e1) :::

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

+        isDefined(e0) ::: isDefined(e1) :::

+        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 Contains(e0, e1) =>

+        isDefined(e0) ::: isDefined(e1)

       case Eval(h, e) =>

         val (evalHeap, evalMask, evalCredits, checks, assumptions) = fromEvalState(h);

         val evalEtran = new ExpressionTranslator(List(evalHeap, evalMask, evalCredits), currentClass);

@@ -1396,9 +1404,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
       Tr(e0) / Tr(e1)

     case Mod(e0,e1) =>

       Tr(e0) % Tr(e1)

-    case q: Forall =>

-      translateQuantification(q)

-    case q: Exists =>

+    case q: Quantification =>

       translateQuantification(q)

     case EmptySeq(t) =>

       createEmptySeq

@@ -1420,6 +1426,8 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
       Boogie.FunctionApp("Seq#Take", List(Tr(e0), Tr(e1)))

     case Length(e) =>

       Boogie.FunctionApp("Seq#Length", List(Tr(e)))

+    case Contains(e0, e1) =>

+      Boogie.FunctionApp("Seq#Contains", List(Tr(e1), Tr(e0)))

     case Eval(h, e) =>

       val (evalHeap, evalMask, evalCredits, checks, assumptions) = fromEvalState(h);

       val evalEtran = new ExpressionTranslator(List(evalHeap, evalMask, evalCredits), currentClass);

@@ -1450,7 +1458,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
     }

   }

 

-  def ShaveOffOld(e: Expression): (Expression, boolean) = e match {

+  def ShaveOffOld(e: Expression): (Expression, Boolean) = e match {

     case Old(e) =>

       val (f,o) = ShaveOffOld(e)

       (f,true)