banking testcases

testcases/verification/xlang/BankSimpleTransactions.scala

+import leon.lang._
+
+object BankSimpleTransactions {
+
+  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)
+  }
+
+
+  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)
+  }
+
+}

testcases/verification/xlang/BankTransfer.scala

@@ -2,72 +2,39 @@ import leon.lang._
 
 object BankTransfer {
 
-  def okTransaction(): Unit = {
-    var balance: BigInt = 0
+  case class BankAccount(var checking: BigInt, var saving: BigInt) {
+    require(checking >= 0 && saving >= 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 balance: BigInt = checking + saving
   }
 
-  def invalidTransaction(): Unit = {
-    var balance: BigInt = 0
+  //TODO: support for map references to mutable items
+  //case class Bank(accounts: Map[BigInt, BankAccount])
 
-    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)
-  }
+  def deposit(x: BigInt, account: BankAccount): Unit = {
+    require(x > 0)
+    account.checking = account.checking + x
+  } ensuring(_ => account.balance == old(account).balance + x)
 
+  def withdrawal(x: BigInt, account: BankAccount): Unit = {
+    require(x > 0 && account.checking >= x)
+    account.checking = account.checking - x
+  } ensuring(_ => account.balance == old(account).balance - x)
 
-  def internalTransfer(): Unit = {
-    var checking: BigInt = 0
-    var saving: BigInt = 0
+  def transfer(x: BigInt, a1: BankAccount, a2: BankAccount): Unit = {
+    require(x > 0 && a1.checking >= x)
+    withdrawal(x, a1)
+    deposit(x, a2)
+  } ensuring(_ => a1.balance + a2.balance == old(a1).balance + old(a2).balance &&
+                  a1.balance == old(a1).balance - x &&
+                  a2.balance == old(a2).balance + x)
 
-    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)
-  }
+  def save(x: BigInt, account: BankAccount): Unit = {
+    require(x > 0 && account.checking >= x)
+    account.checking = account.checking - x
+    account.saving = account.saving + x
+  } ensuring(_ => account.balance == old(account).balance)
 
 }