No commit message

No commit message

src/funcheck/AnalysisComponent.scala

@@ -43,6 +43,9 @@ class AnalysisComponent(val global: Global, val pluginInstance: FunCheckPlugin)
       println("Extracted program for " + unit + ": ")
       println(prog)
 
+      println("Starting analysis.")
+      purescala.Analysis.analyze(prog)
+
       // Mirco your component can do its job here, as I leave the trees
       // unmodified.
       // val (genDef, arbDef) = createGeneratorDefDefs(unit)

src/purescala/Analysis.scala

+package purescala
+
+import Definitions._
+import Trees._
+
+object Analysis {
+    // Analysis should check that:
+    //  - all the postconditions are implied by preconds. + body
+    //  - all callsites satisfy the preconditions
+    //  - all matches are exhaustive
+    // In the future:
+    //  - catamorphisms are catamorphisms (poss. with surjectivity conds.)
+    //  - injective functions are injective
+    //  - all global invariants are satisfied 
+    def analyze(program: Program) : Unit = {
+        program.mainObject.defs.filter(_.isInstanceOf[FunDef]).foreach(df => {
+            val funDef = df.asInstanceOf[FunDef]
+            val vc = postconditionVC(funDef)
+            if(vc != BooleanLiteral(true)) {
+                println("Verification condition for " + funDef.id + ":")
+                println(vc)
+            }
+        }) 
+    }
+
+    def postconditionVC(functionDefinition: FunDef) : Expr = {
+        val prec = functionDefinition.precondition
+        val post = functionDefinition.postcondition
+
+        if(post.isEmpty) {
+            BooleanLiteral(true)
+        } else {
+            BooleanLiteral(false)
+        }
+    }
+}

src/purescala/PrettyPrinter.scala

@@ -98,10 +98,10 @@ object PrettyPrinter {
     case GreaterThan(l,r) => ppBinary(sb, l, r, " > ", lvl)
     case LessEquals(l,r) => ppBinary(sb, l, r, " \u2264 ", lvl)      // \leq
     case GreaterEquals(l,r) => ppBinary(sb, l, r, " \u2265 ", lvl)   // \geq
-    case EmptySet(_) => sb.append("Ø")
-    case SetUnion(l,r) => ppBinary(sb, l, r, " U ", lvl)
-    case SetDifference(l,r) => ppBinary(sb, l, r, " \\ ", lvl)
-    case SetIntersection(l,r) => ppBinary(sb, l, r, " INT ", lvl)
+    case EmptySet(_) => sb.append("\u2205")                          // Ø
+    case SetUnion(l,r) => ppBinary(sb, l, r, " \u222A ", lvl)        // \cup
+    case SetDifference(l,r) => ppBinary(sb, l, r, " \\ ", lvl)       
+    case SetIntersection(l,r) => ppBinary(sb, l, r, " \u2229 ", lvl) // \cap
     
     case IfExpr(c, t, e) => {
       var nsb = sb

testcases/BinarySearchTree.scala

+import scala.collection.immutable.Set
+
+object BinarySearchTree {
+    sealed abstract class Tree
+    case class Node(left: Tree, value: Int, right: Tree) extends Tree
+    case class Leaf() extends Tree
+
+    def emptySet() : Tree = Leaf()
+
+    def insert(tree: Tree, value: Int) : Tree = (tree match {
+        case Leaf() => Node(Leaf(), value, Leaf())
+        case n @ Node(_, v, _) if v == value => n
+        case Node(l, v, r) if v < value => Node(l, v, insert(r, value))
+        case Node(l, v, r) if v > value => Node(insert(l, value), v, r)
+    }) ensuring(_ != Leaf())
+
+    def contains(tree: Tree, value: Int) : Boolean = tree match {
+        case Leaf() => false
+        case Node(_, v, _) if v == value => true 
+        case Node(l, v, r) if v < value => contains(r, value)
+        case Node(l, v, r) if v > value => contains(l, value)
+    }
+
+    def contents(tree: Tree) : Set[Int] = tree match {
+        case Leaf() => Set.empty[Int]
+        case Node(l, v, r) => contents(l) /*++ Set(v)*/ ++ contents(r)
+    }
+}
+