Question: Use VDM method to specify an automated transaction machine (ATM)

- Problem description

An automatic transaction machine provides fast banking services for depositing and withdrawing cash. Each user of the ATM has a card that is coded with a unique password of the user.

To initiate a transaction, machine is accessed with a card and password. If the password coded in the card matches the password entered by the user, the user is permitted to execute the transaction; otherwise, the transaction is terminated. It is assumed that only one account can be accessed with one card. The machine allows only two types of transactions withdraw, and deposit.

- Additional requirements o Each account in the bank is uniquely identified by an account number.

o A user can have several accounts with the bank; however, the user needs one card for each account.

o The machine has a reserve that can hold a fixed amount of cash.

o If there is a request to withdraw an amount exceeding the balance in that account or in the machine's reserve, the withdraw1 request will not be completed. No partial withdraw1 is permitted. The machine's reserve can be modified only by an employee of the bank. Each employee of the bank has a distinct card to access a special account.

An employee can update the reserve of the machine using the distinct card.

o The machine's reserve can be modified only by an employee of bank. Each employ of the bank has a distinct card to access a special account to update the reserve of the machine using the distinct card.

o Error messages should be given to user stating why a certain operation is not successful.

- Assumptions

o All account holders have equal privileges.

o Sufficient funds are deposited into the machine's reserve on regular basis.

- Operations Your specification should include three operations: (1) withdraw, (2) update reserve, and (3) deposit