From abe378341a00ce4166e41edbf033f1654146b259 Mon Sep 17 00:00:00 2001
From: Viktor Kuncak <vkuncak@gmail.com>
Date: Tue, 13 Jul 2010 10:25:41 +0000
Subject: [PATCH] ExprCompr soundness
---
testcases/ExprComp.scala | 11 ++++++++++-
1 file changed, 10 insertions(+), 1 deletion(-)
diff --git a/testcases/ExprComp.scala b/testcases/ExprComp.scala
index 3154bd460..945e78642 100644
--- a/testcases/ExprComp.scala
+++ b/testcases/ExprComp.scala
@@ -58,7 +58,7 @@ object ExprComp {
case EStack() => Fail()
case NStack(v1,vs1) => vs1 match {
case EStack() => Fail()
- case NStack(v2,vs2) => run(rest, NStack(evalOp(v1,op,v2),vs2))
+ case NStack(v2,vs2) => Fail() // should be: run(rest, NStack(evalOp(v1,op,v2),vs2))
}
}
}
@@ -77,4 +77,13 @@ object ExprComp {
def property(e : Expr, acc : Program, vs : ValueStack) : Boolean = {
run(compile(e, acc), vs) == Ok(NStack(eval(e), vs))
} ensuring (res => res)
+
+ def main(args : Array[String]) = {
+ val e = Binary(Constant(Value(3)), Plus(), Constant(Value(5)))
+ val vs = EStack()
+ val acc = EProgram()
+ println(run(compile(e, acc), vs))
+ println(Ok(NStack(eval(e), vs)))
+ println(property(e,acc,vs))
+ }
}
--
GitLab