Aim

The aim of this practical is to develop Event-B models. In all cases the resulting machines should be introduced into the Rodin Toolkit, analyzed, proof obligations generated, the autoprover run and any remaining undischarged proof obligations inspected carefully. In many cases it would be a good idea to animate the machine.

A Simple Bank Machine

Produce a model, consisting of context SimpleBank_ctx and machine SimpleBank, of a very simple bank with the following requirements. Follow the English very carefully.

accounts: the bank customers are represented by accounts. Having obtained an account a customer may use the other operations supported by the bank.

balance: the bank needs to maintain a balance for all accounts.

NewAccount: an operation by which a customer obtains an account identifier. Account identifiers are allocated from a pool (set) of identifiers maintained by the bank.

Deposit: an operation to add an amount to an account balance.

WithDraw: an operation to withdraw an amount from an account. Customers cannot withdraw more than the balance in their account.

Transfer: an operation that transfers an amount of money from one bank account to another.

Note that the balance and all other money amounts can be represented by natural numbers.