diff --git a/examples/parsable/IntSets.scala b/examples/parsable/IntSets.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e9a703c3688c4fd825b573915c847049485066c2
--- /dev/null
+++ b/examples/parsable/IntSets.scala
@@ -0,0 +1,14 @@
+package intsets
+
+object IntSets {
+  import scala.collection.immutable.Set
+
+  def union(s1: Set[Int], s2: Set[Int]): Set[Int] = {
+    require(!s1.isEmpty && !s2.isEmpty)
+    s1 ++ s2
+  } ensuring((res: Set[Int]) => res.size > s1.size && res.size > s2.size && res.size <= s1.size + s2.size)
+
+  def main(args: Array[String]): Unit = {
+    println(union(Set(1, 2, 3), Set(2, 3, 4)))
+  }
+}
diff --git a/src/funcheck/Extractors.scala b/src/funcheck/Extractors.scala
index 609b4475b3f7dfc6a58c3fb3da183a3de6200240..838442b8a90f3b3a855271fc9669b13334060b15 100644
--- a/src/funcheck/Extractors.scala
+++ b/src/funcheck/Extractors.scala
@@ -50,16 +50,19 @@ trait Extractors {
     }
 
     object ObjectDefn {
-      def unapply(tree: Tree): Option[String] = tree match {
-        case c @ ClassDef(_, name, tparams, impl) => {
-          println(name.toString + " is being traversed.")
-          println(c.symbol)
-          if(c.symbol.isModuleClass) {
-            Some(name.toString)
-          } else {
-            None
-          }
-        }
+      /** Matches an object with no type parameters, and regardless of its
+       * visibility. */
+      def unapply(cd: ClassDef): Option[(String,Template)] = cd match {
+        case ClassDef(_, name, tparams, impl) if (cd.symbol.isModuleClass && tparams.isEmpty) => Some((name.toString, impl))
+        case _ => None
+      }
+    }
+
+    object FunctionDefn {
+      /** Matches a function with a single list of arguments, no type
+       * parameters and regardless of its visibility. */
+      def unapply(dd: DefDef): Option[(String,Seq[ValDef],Tree,Tree)] = dd match {
+        case DefDef(_, name, tparams, vparamss, tpt, rhs) if(tparams.isEmpty && vparamss.size == 1) => Some((name.toString, vparamss(0), tpt, rhs))
         case _ => None
       }
     }
diff --git a/src/funcheck/purescala/Definitions.scala b/src/funcheck/purescala/Definitions.scala
index f7b638f5fe982ff5ead748925c4d4a7f969fec5d..f2ad9e0b482e44be962becdcf0b2991db9924c23 100644
--- a/src/funcheck/purescala/Definitions.scala
+++ b/src/funcheck/purescala/Definitions.scala
@@ -5,7 +5,23 @@ object Definitions {
   import Trees._
   import TypeTrees._
 
-  sealed abstract class Definition {
+  /** Scopes add new definitions to the surrounding scope. */
+  trait Scope {
+    import scala.collection.immutable.Map
+
+    val parentScope: Option[Scope] = None
+    def lookupObject(id: Identifier): Option[ObjectDef] = None
+    def lookupClassType(id: Identifier): Option[ClassTypeDef] = None
+    def lookupAbstractClass(id: Identifier): Option[AbstractClassDef] = None
+    def lookupCaseClass(id: Identifier): Option[CaseClassDef] = None
+    def lookupClass(id: Identifier): Option[ClassDef] = None
+    def lookupVal(id: Identifier): Option[ValDef] = None
+    def lookupFun(id: Identifier): Option[FunDef] = None
+  }
+
+  /** A definition is anything "structural", ie. anything that's part of the
+   * syntax of a program but not in an expression. */
+  sealed abstract class Definition extends Scope {
     val id: Identifier
     override def toString: String = PrettyPrinter(this)
   }
@@ -15,7 +31,7 @@ object Definitions {
 
   /** Objects work as containers for class definitions, functions (def's) and
    * val's. */
-  case class ObjectDef(id: Identifier, defs : Seq[Definition]) extends Definition
+  case class ObjectDef(id: Identifier, defs : Seq[Definition], invariants: Seq[Expr]) extends Definition
 
   /** Useful because case classes and classes are somewhat unified in some
    * patterns (of pattern-matching, that is) */
@@ -42,7 +58,7 @@ object Definitions {
   case class ValDef(id: Identifier, value: Expr) extends Definition
 
   /** Functions (= 'methods' of objects) */
-  case class FunDef(id: Identifier, args: VarDecls, body: Expr) extends Definition {
+  case class FunDef(id: Identifier, args: VarDecls, body: Expr, precondition: Option[Expr], postcondition: Option[Expr]) extends Definition {
     lazy val argTypes : Seq[TypeTree] = args.map(_.tpe) 
     lazy val returnType : TypeTree = body.getType
   }
diff --git a/src/funcheck/purescala/PrettyPrinter.scala b/src/funcheck/purescala/PrettyPrinter.scala
index dcde2788a5b9b82a9213cedcdce69ac0abc20dfa..9338f6b8477f1247be306a63a538e79884ce24e0 100644
--- a/src/funcheck/purescala/PrettyPrinter.scala
+++ b/src/funcheck/purescala/PrettyPrinter.scala
@@ -68,6 +68,17 @@ object PrettyPrinter {
     case Equals(l,r) => ppBinary(sb, l, r, " = ")
     case IntLiteral(v) => sb.append(v)
     case BooleanLiteral(v) => sb.append(v)
+    case IfExpr(c, t, e) => {
+      var nsb = sb
+      nsb.append("if (")
+      nsb = pp(c, nsb)
+      nsb.append(") { ")
+      nsb.append(t)
+      nsb.append(" } else { ")
+      nsb.append(e)
+      nsb.append(" }")
+      nsb
+    }
 
     case _ => sb.append("Expr?")
   }
diff --git a/src/funcheck/purescala/Trees.scala b/src/funcheck/purescala/Trees.scala
index beeebc0f19c61aa621948624976d2c68697c4bbb..c2086f23696f83ad0d67a98cc9bee9b1cd8e3c4c 100644
--- a/src/funcheck/purescala/Trees.scala
+++ b/src/funcheck/purescala/Trees.scala
@@ -15,6 +15,14 @@ object Trees {
    * node, and each node is then responsible for communicating its type. */
   sealed abstract class Expr extends Typed {
     override def toString: String = PrettyPrinter(this)
+
+    var _scope: Scope = null
+
+    def scope: Scope =
+      if(_scope == null)
+        throw new Exception("Undefined scope.")
+      else
+        _scope
   }
 
   /** 
@@ -36,7 +44,7 @@ see examples in:
     lazy val getType = funDef.returnType
   }
 
-  case class IfExpr(cond : Expr, then : Expr, elze : Expr) extends Expr {
+  case class IfExpr(cond: Expr, then: Expr, elze: Expr) extends Expr {
     assert(cond.getType == BooleanType)
     assert(then.getType == elze.getType)
     def getType = then.getType