From 0c45517318adf65d422d6680b098ad9db8ebac69 Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Wed, 9 Jun 2010 22:22:52 +0000
Subject: [PATCH]
---
src/funcheck/AnalysisComponent.scala | 3 +++
src/purescala/Analysis.scala | 36 ++++++++++++++++++++++++++++
src/purescala/PrettyPrinter.scala | 8 +++----
testcases/BinarySearchTree.scala | 29 ++++++++++++++++++++++
4 files changed, 72 insertions(+), 4 deletions(-)
create mode 100644 src/purescala/Analysis.scala
create mode 100644 testcases/BinarySearchTree.scala
diff --git a/src/funcheck/AnalysisComponent.scala b/src/funcheck/AnalysisComponent.scala
index 332c4629b..0497946ec 100644
--- a/src/funcheck/AnalysisComponent.scala
+++ b/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)
diff --git a/src/purescala/Analysis.scala b/src/purescala/Analysis.scala
new file mode 100644
index 000000000..1f9809ad9
--- /dev/null
+++ b/src/purescala/Analysis.scala
@@ -0,0 +1,36 @@
+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)
+ }
+ }
+}
diff --git a/src/purescala/PrettyPrinter.scala b/src/purescala/PrettyPrinter.scala
index 8a835a896..c96723707 100644
--- a/src/purescala/PrettyPrinter.scala
+++ b/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
diff --git a/testcases/BinarySearchTree.scala b/testcases/BinarySearchTree.scala
new file mode 100644
index 000000000..329878053
--- /dev/null
+++ b/testcases/BinarySearchTree.scala
@@ -0,0 +1,29 @@
+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)
+ }
+}
+
--
GitLab