From fe8a64df2cf8de79703c5b1732761d65b57429ba Mon Sep 17 00:00:00 2001
From: Viktor Kuncak <vkuncak@gmail.com>
Date: Tue, 6 Jul 2010 17:47:09 +0000
Subject: [PATCH] another example, which should fail
---
testcases/Account2.scala | 22 ++++++++++++++++++++++
1 file changed, 22 insertions(+)
create mode 100644 testcases/Account2.scala
diff --git a/testcases/Account2.scala b/testcases/Account2.scala
new file mode 100644
index 000000000..e6fb25ce8
--- /dev/null
+++ b/testcases/Account2.scala
@@ -0,0 +1,22 @@
+object Account2 {
+ sealed abstract class AccLike
+ case class Acc(checking : Int, savings : Int) extends AccLike
+
+ def sameTotal(a1 : Acc, a2 : Acc) : Boolean = {
+ a1.checking + a1.savings == a2.checking + a2.savings
+ }
+ def notRed(a : Acc) : Boolean = {
+ a.checking >= 0 && a.savings >= 0
+ }
+
+ def toSavingsOk(x : Int, a : Acc) : Acc = {
+ require (notRed(a) && x >= 0 && a.checking >= x)
+ Acc(a.checking - x, a.savings + x)
+ } ensuring (res => (notRed(res) && sameTotal(a, res)))
+
+ def toSavingsBroken(x : Int, a : Acc) : Acc = {
+ require (notRed(a) && a.checking >= x)
+ Acc(a.checking - x, a.savings + x)
+ } ensuring (res => (notRed(res) && sameTotal(a, res)))
+
+}
--
GitLab