System Requirements

• The banking system should be able to furnish the current balance and overdraft limit of any account and allow alterations to the overdraft limit.
• It should be possible to open new accounts at the bank and to close existing accounts.
• It should be possible to record deposits and withdrawals.
• The system should be able to identify accounts with balances below a specified amount.

[ACC_NO]

Initialise the system

ÚÄInitAccountÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ Account
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ balance = í
³ od_limit = í
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

ÚÄœAccountÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ Account
³ Account'
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

ÚÄOpenÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ œAccount
³ new? : ACC_NO
³ odl? : Ÿ
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ new? ç dom balance
³ odl? ò 0
³ balance' = balance µ {new? šŽ 0}
³ od_limit' = od_limit µ {new? šŽ -odl?}
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

The following schema is normally not included

ÚÄ�AccountÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ œAccount
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ balance' = balance
³ od_limit' = od_limit
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

ÚÄQueryBalanceÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ �Account
³ acc? : ACC_NO
³ acc_balance! : Ÿ
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ acc? î dom balance
³ acc_balance! = balance acc?
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

ÚÄQueryOdLimitÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ �Account
³ acc? : ACC_NO
³ acc_od_limit! : Ÿ
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ acc? î dom od_limit
³ acc_od_limit! = -(od_limit acc?)
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

ÚÄCloseÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ œAccount
³ acc? : ACC_NO
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ acc? î dom balance
³ balance acc? = 0
³ balance' = {acc?} ° balance
³ od_limit' = {acc?} ° od_limit
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

ÚÄCloseÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ œAccount
³ acc? : ACC_NO
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ acc? î dom balance
³ balance acc? = 0
³ balance' = balance \ {acc? šŽ balance acc?}
³ od_limit' = od_limit \ {acc? šŽ od_limit acc?}
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

ÚÄQueryForAccountÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ �Account
³ amount? : Ÿ
³ accounts! : ˆacc_no
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ accounts! = dom (balance © { x : Ÿ | x < amount? })
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

REPORT ::= ok | already_exists | neg_od_limit | no_such_account | not_pos_amnt | over_od_limit | bal_not_zero | bal_below_od_lim

ÚÄSuccessÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ result! : REPORT
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ result! = ok
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

RInitAccount ¡ InitAccount ™ Success

ÚÄRInitAccountÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ Account
³ result! : REPORT
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ balance = í
³ od_limit = í
³ result! = ok
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

ÚÄAlreadyExistsÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ �Account
³ new? : ACC_NO
³ result! : REPORT
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ new? î dom balance
³ result! = already_exists
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

ÚÄNegOdLimitÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ �Account
³ new? : ACC_NO
³ odl? : Ÿ
³ result! : REPORT
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ new? ç dom balance
³ odl? < 0
³ result! = neg_od_limit
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

ROpen ¡ (Open ™ Success) ˜ AlreadyExists ˜ NegOdLimit

ÚÄNoSuchAccountÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ �Account
³ acc? : ACC_NO
³ result! : REPORT
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ acc? ç dom balance
³ result! = no_such_account
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

ÚÄNotPosAmntÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ �Account
³ acc? : ACC_NO
³ amount? : Ÿ
³ result! : REPORT
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ acc? î dom balance
³ amount? ó 0
³ result! = not_pos_amnt
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

RDeposit ¡ (Deposit ™ Success) ˜ NoSuchAccount ˜ NotPosAmnt

ÚÄOverOdLimitÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ �Account
³ acc? : ACC_NO
³ amount? : Ÿ
³ result! : REPORT
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ acc? î dom balance
³ amount? > 0
³ balance acc? - amount? < od_limit acc?
³ result! = over_od_limit
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

RWithdraw ¡ (Withdraw ™ Success) ˜ NoSuchAccount ˜ NotPosAmnt ˜ OverOdLimit

RQueryBalance ¡ (QueryBalance ™ Success) ˜ NoSuchAccount

RQueryOdLimit ¡ (QueryOdLimit ™ Success) ˜ NoSuchAccount

RQueryForAccount ¡ QueryForAccount ™ Success

ÚÄNegOdLimit2ÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ �Account
³ acc? : ACC_NO
³ odl? : Ÿ
³ result! : REPORT
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ acc? î dom od_limit
³ odl? < 0
³ balance acc? ò -odl?
³ result! = neg_od_limit
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

ÚÄTooSmallOdLimitÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ �Account
³ acc? : ACC_NO
³ odl? : Ÿ
³ result! : REPORT
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ acc? î dom od_limit
³ odl? ò 0
³ balance acc? < -odl?
³ result! = bal_below_od_lim
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

RAlterOdLimit ¡ (AlterOdLimit ™ Success) ˜ NoSuchAccount ˜ NegOdLimit2 ˜ TooSmallOdLimit

ÚÄBalNotZeroÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ �Account
³ acc? : ACC_NO
³ result! : REPORT
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ acc? î dom balance
³ balance acc? ² 0
³ result! = bal_not_zero
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

RClose ¡ (Close ™ Success) ˜ NoSuchAccount ˜ BalNotZero