From ed824282b5a4a5073e0fd1d212a8120f3c4b6e9a Mon Sep 17 00:00:00 2001
From: Mirco Dotta <mirco.dotta@gmail.com>
Date: Fri, 10 Jul 2009 14:08:34 +0000
Subject: [PATCH] Added pre/post condition to mk example
---
tests/plugin/kawaguchi/MiniBDD.scala | 10 +++++++---
1 file changed, 7 insertions(+), 3 deletions(-)
diff --git a/tests/plugin/kawaguchi/MiniBDD.scala b/tests/plugin/kawaguchi/MiniBDD.scala
index 0678bf4b2..26ed18d24 100644
--- a/tests/plugin/kawaguchi/MiniBDD.scala
+++ b/tests/plugin/kawaguchi/MiniBDD.scala
@@ -67,8 +67,8 @@ object MiniBDD {
def empty2 = Map.empty[(BDD,BDD),BDD]
def mk_not(x: BDD): BDD = {
+ require(check(x))
val cache = empty
- assert(check(x))
def mk_not_rec(cache: Map[BDD,BDD], x: BDD): (Map[BDD,BDD],BDD) = {
cache.get(x) match {
@@ -92,9 +92,8 @@ object MiniBDD {
}
val (_,rv) = mk_not_rec(cache, x)
- assert(check(rv))
rv
- }
+ } ensuring { res => check(res)}
def apply_op(op: Op, b1: Boolean, b2: Boolean): Boolean = op match {
case And() => b1 && b2
@@ -174,4 +173,9 @@ object MiniBDD {
}
}
+
+
+ def main(args: Array[String]) = {
+
+ }
}
--
GitLab