diff --git a/testcases/verification/xlang/BankTransfer.scala b/testcases/verification/xlang/BankTransfer.scala index 05b27dbc5c3b1aec5fef575ea20b0d689f1f24e8..c533b4e08a6297446aad36d7a31fd04e148ccc37 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) + } + }