From 5984b82c9e755f41ecf143cfd1ea16b0e9a1a26d Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Mon, 28 Dec 2015 20:16:44 +0100
Subject: [PATCH] bank transfer example with variables
---
.../verification/xlang/BankTransfer.scala | 42 +++++++++++++++++++
1 file changed, 42 insertions(+)
create mode 100644 testcases/verification/xlang/BankTransfer.scala
diff --git a/testcases/verification/xlang/BankTransfer.scala b/testcases/verification/xlang/BankTransfer.scala
new file mode 100644
index 000000000..05b27dbc5
--- /dev/null
+++ b/testcases/verification/xlang/BankTransfer.scala
@@ -0,0 +1,42 @@
+import leon.lang._
+
+object BankTransfer {
+
+ def okTransaction(): Unit = {
+ var balance: BigInt = 0
+
+ def balanceInvariant: Boolean = balance >= 0
+
+ def deposit(x: BigInt): Unit = {
+ require(balanceInvariant && x >= 0)
+ balance += x
+ } ensuring(_ => balance == old(balance) + x && balanceInvariant)
+
+ def withdrawal(x: BigInt): Unit = {
+ require(balanceInvariant && x >= 0 && x <= balance)
+ balance -= x
+ } ensuring(_ => balance == old(balance) - x && balanceInvariant)
+
+ deposit(35)
+ withdrawal(30)
+ }
+
+ def invalidTransaction(): Unit = {
+ var balance: BigInt = 0
+
+ def balanceInvariant: Boolean = balance >= 0
+
+ def deposit(x: BigInt): Unit = {
+ require(balanceInvariant && x >= 0)
+ balance += x
+ } ensuring(_ => balance == old(balance) + x && balanceInvariant)
+
+ def withdrawal(x: BigInt): Unit = {
+ require(balanceInvariant && x >= 0 && x <= balance)
+ balance -= x
+ } ensuring(_ => balance == old(balance) - x && balanceInvariant)
+
+ deposit(35)
+ withdrawal(40)
+ }
+}
--
GitLab