# The Symphony IDE

Formal Modelling for Systems of Systems

Go to our GitHub Profile ## AccountSys

Author: Quentin Charatan and Aaron Kans

This example comes from the book “Formal Software Development: From VDM to Java” written by Quentin Charatan and Aaron Kans. This example illustrate how to model bank accounts and transactions made on these as a series of deposits and withdrawals. The CML model has been made by Peter Gorm Larsen. This example illustrate the use of records with invariants and a state with the bank accounts indexed over the account number. All the operations are defined implicitly. However the reactive part is not defined so that is left as an exercise for the reader.

### AccountSys.cml

``````process AccountSys =
begin

types

AccNum = token

Date = token

Details = token

TransactionType = <Withdrawal> | <Deposit>

Transaction ::
date             : Date
amount           : real
transaction_type : TransactionType
inv mk_Transaction(-,a,-) == a > 0

Account ::
number  : AccNum
details : Details
balance : real
limit   : real
transactions : seq of Transaction
inv mk_Account(-,-,b,l,t) == l >= 0 and b >= l and balanceOf(t) = b

state
accounts : map AccNum to Account
inv forall num in set dom accounts @ num = accounts(num).number

functions

balanceOf: seq of Transaction -> real
balanceOf(transln) ==
let dep = [transln(i).amount | i in set inds transln
@ transln(i).transaction_type = <Deposit>],
withd = [transln(i).amount | i in set inds transln
@ transln(i).transaction_type = <Withdrawal>]
in
sum(dep) - sum(withd)

sum: seq of real -> real
sum(seqln) ==
if seqln = []
then 0
else hd seqln + sum(tl seqln)
measure Len

Len: seq of real -> nat
Len(l) == len l

operations

addAccount(numberIn: AccNum, detailsIn: Details, limitIn: real)
frame wr accounts: map AccNum to Account
pre numberIn not in set dom accounts and limitIn >= 0
post accounts = accounts~ munion {numberIn |-> mk_Account(numberIn, detailsIn, 0, limitIn,[])}

removeAccount(numberIn: AccNum)
frame wr accounts: map AccNum to Account
pre numberIn in set dom accounts
post accounts = {numberIn} <-: accounts~

deposit(numberIn: AccNum, dateIn: Date, amountIn: real)
frame wr accounts: map AccNum to Account
pre numberIn in set dom accounts and amountIn >= 0
post let bal = accounts~(numberIn).balance,
trans = accounts~(numberIn).transactions
in
let newTrans = mk_Transaction(dateIn, amountIn, <Deposit>)
in
accounts = accounts~ ++ {numberIn |-> mk_Account(numberIn,
accounts~(numberIn).details,
bal + amountIn,
accounts~(numberIn).limit,
trans ^ [newTrans])}

withdraw(numberIn: AccNum, dateIn: Date, amountIn: real)
frame wr accounts: map AccNum to Account
pre numberIn in set dom accounts and amountIn >= 0 and
accounts(numberIn).balance -amountIn >= accounts(numberIn).limit
post let bal = accounts~(numberIn).balance,
trans = accounts~(numberIn).transactions
in
let newTrans = mk_Transaction(dateIn, amountIn, <Withdrawal>)
in
accounts = accounts~ ++ {numberIn |-> mk_Account(numberIn,
accounts~(numberIn).details,
bal - amountIn,
accounts~(numberIn).limit,
trans ^ [newTrans])}

changeDetails(numberIn: AccNum, detailsIn: Details)
frame wr accounts: map AccNum to Account
pre numberIn in set dom accounts
post accounts = accounts~ ++ {numberIn |-> mk_Account(numberIn,
detailsIn,
accounts~(numberIn).balance,
accounts~(numberIn).limit,
accounts~(numberIn).transactions)}

changeLimits(numberIn: AccNum, limitIn: real)
frame wr accounts: map AccNum to Account
pre numberIn in set dom accounts and limitIn >= 0 and
accounts(numberIn).balance >= limitIn
post accounts = accounts~ ++ {numberIn |-> mk_Account(numberIn,
accounts~(numberIn).details,
accounts~(numberIn).balance,
limitIn,
accounts~(numberIn).transactions)}

getDetails(numberIn: AccNum) detailsOut: Details
frame rd accounts: map AccNum to Account
pre numberIn in set dom accounts
post detailsOut = accounts(numberIn).details

getBalance(numberIn: AccNum) balanceOut: real
frame rd accounts: map AccNum to Account
pre numberIn in set dom accounts
post balanceOut = accounts(numberIn).balance

getLimit(numberIn: AccNum) limitOut: real
frame rd accounts: map AccNum to Account
pre numberIn in set dom accounts
post limitOut = accounts(numberIn).limit

getAllTransactions(numberIn: AccNum) transactionsOut: seq of Transaction
frame rd accounts: map AccNum to Account
pre numberIn in set dom accounts
post transactionsOut = accounts(numberIn).transactions

contains(numberIn: AccNum) query: bool
frame rd accounts: map AccNum to Account
post query <=> numberIn in set dom accounts

isEmpty() query: bool
frame rd accounts: map AccNum to Account
post query <=> accounts = {|->}

getTotal() totalOut: nat
frame rd accounts: map AccNum to Account
post totalOut = card dom accounts

@ Skip

end
``````