From 7e36b3e13c08b216d6e059737fa707853c4a3533 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Mon, 4 Jan 2016 17:41:38 +0100
Subject: [PATCH] bank transfer example with internal transfers
---
.../verification/xlang/BankTransfer.scala | 31 +++++++++++++++++++
1 file changed, 31 insertions(+)
diff --git a/testcases/verification/xlang/BankTransfer.scala b/testcases/verification/xlang/BankTransfer.scala
index 05b27dbc5..c533b4e08 100644
--- a/testcases/verification/xlang/BankTransfer.scala
+++ b/testcases/verification/xlang/BankTransfer.scala
@@ -39,4 +39,35 @@ object BankTransfer {
deposit(35)
withdrawal(40)
}
+
+
+ def internalTransfer(): Unit = {
+ var checking: BigInt = 0
+ var saving: BigInt = 0
+
+ def balance = checking + saving
+
+ def balanceInvariant: Boolean = balance >= 0
+
+ def deposit(x: BigInt): Unit = {
+ require(balanceInvariant && x >= 0)
+ checking += x
+ } ensuring(_ => checking == old(checking) + x && balanceInvariant)
+
+ def withdrawal(x: BigInt): Unit = {
+ require(balanceInvariant && x >= 0 && x <= checking)
+ checking -= x
+ } ensuring(_ => checking == old(checking) - x && balanceInvariant)
+
+ def checkingToSaving(x: BigInt): Unit = {
+ require(balanceInvariant && x >= 0 && checking >= x)
+ checking -= x
+ saving += x
+ } ensuring(_ => checking + saving == old(checking) + old(saving) && balanceInvariant)
+
+ deposit(50)
+ withdrawal(30)
+ checkingToSaving(10)
+ }
+
}
--
GitLab