Simple Bank

This document was generated from the URDAD model Simple Bank. It specifies what the business requires, independently of any technology.

It is written to be read without knowledge of URDAD or of its diagrams, as every diagram is followed by a description of what it shows, in words. The specification is organised by responsibility domain. For each, it describes the services the domain provides, i.e. what each requires and guarantees, the information exchanged with it, how the work is allocated to other domains and the business process which provides it. It then describes the entities the domain maintains, the services it depends on from other domains, and finally its lower-level responsibility domains, each in a part of its own. The first part is the model itself, specified as the responsibility domain which contains all the others. It gives the model’s scope and the top-level responsibility domains it decomposes into.

1. Simple Bank

This part specifies the model Simple Bank as a whole. The model is the responsibility domain which contains all the others. It decomposes into top-level responsibility domains, each of which provides services to others and may in turn rely on services of other domains.

A minimal bank, modelled in URDAD as a reference and teaching model.

Customers register, open accounts, deposit, withdraw, transfer, pay salaries, move large amounts, ask for a balance and close accounts — nine use cases over three entities. Between them the processes use every construct of the method: alternate and concurrent flows, for-each and while loops, and exceptions both handled and raised.

Read it top-down, as the method works: start at a use case — a service published to Customer, in the department that answers for it — look at its functional requirements (its pre- and post-conditions), see which lower-level service each requirement is allocated to, and then how the process orchestrates them. Every requirement is formal, most of them in URDAD-OCL, and the post-conditions use @pre to say how a service changes the bank's state.

Generated by models/simpleBank/generate.py.

The scope diagram below shows what Simple Bank is responsible for, i.e. the top-level responsibility domains it decomposes into.

Figure 1. The scope of Simple Bank.

1.1. Lower-level responsibilities

Simple Bank decomposes into the following top-level responsibility domains, each specified in the same way:

Customer: A customer of the bank, to whom the bank’s services are offered.
Bank: The bank: its shared vocabulary and the departments that answer for its services.

2. Customer

This part specifies the Customer responsibility domain. A responsibility domain is an area of responsibility, e.g. a business unit, a role or a system, which provides services to others and may in turn rely on services of other domains.

A customer of the bank, to whom the bank’s services are offered.

A role, owning nothing in this model: a person plays the role of a customer. Every use case is published to it, which is what makes the service callable from outside the bank, and every advice is sent to it.

The scope diagram below shows what Customer is responsible for, i.e. the services it provides and the lower-level responsibility domains it contains.

Figure 2. The scope of Customer.

Nothing has been specified within this responsibility domain yet.

3. Bank

This part specifies the Bank responsibility domain. A responsibility domain is an area of responsibility, e.g. a business unit, a role or a system, which provides services to others and may in turn rely on services of other domains.

The bank: its shared vocabulary and the departments that answer for its services.

Responsibility is divided by what each department can guarantee: Customer Register knows who the customers are, Accounts keeps the accounts, and Ledger is the only thing that moves money. Each offers the customer the use cases whose outcome it answers for, and requests of the others what only they can do.

The scope diagram below shows what Bank is responsible for, i.e. the services it provides and the lower-level responsibility domains it contains.

Figure 3. The scope of Bank.

3.1. Lower-level responsibilities

Bank delegates part of its responsibility to the following lower-level responsibility domains, each specified in the same way:

Customer Register: Who the bank’s customers are.
Accounts: The bank’s accounts: opening, looking up and closing them.
Ledger: The only thing that moves money, and the record of every movement.

4. Bank / Customer Register

This part specifies the Customer Register responsibility domain. A responsibility domain is an area of responsibility, e.g. a business unit, a role or a system, which provides services to others and may in turn rely on services of other domains.

Who the bank’s customers are.

Offers Register as customer, which puts a person on its record.

The scope diagram below shows what Customer Register is responsible for, i.e. the services it provides and the lower-level responsibility domains it contains.

Figure 4. The scope of Customer Register.

4.1. Services

Customer Register is responsible for providing the following services. Each is described in its own section below: what it requires and what it guarantees (its service requirements), the information exchanged with it, how the work is allocated to the responsibility domains taking part, and the business process providing it.

Register as customer: A person becomes a customer of the bank.
Record customer: Records a new customer and issues their customer number.
getCustomer: Gives the customer with the customer number asked for, as its owning domain holds it. Generated from the entity; generate again rather than editing it.
findCustomerByIdentityNumber: Gives the customer with the identity number asked for, as its owning domain holds it. Generated from the entity; generate again rather than editing it.
findCustomerByLogin: Gives the customer with the login asked for, as its owning domain holds it. Generated from the entity; generate again rather than editing it.

4.1.1. Service: Register as customer

Customer Register provides the Register as customer service.

A person becomes a customer of the bank.

The login the customer registers with is not in the request: it is caller, the identity that asked. The post-condition says so, which is how a model ties a login identity to a business entity.

Service requirements

The functional requirements diagram below shows who has an interest in the Register as customer service, i.e. its stakeholders, and what each requires of it. A pre-condition is a condition which must hold for the service to be provided at all. When one does not, the request is refused with an exception. A post-condition is what must be true once the service has been provided, i.e. what it must have achieved.

Figure 5. Functional requirements of the Register as customer service.

Its stakeholders, and what each requires of it, are:

Bank: The bank: its shared vocabulary and the departments that answer for its services.

Bank requires the pre-condition Identity not yet registered.
Customer: A customer of the bank, to whom the bank’s services are offered.

Customer requires the post-condition Customer registered.

It is provided only when:

Identity not yet registered: Each person is registered once.

Required by Bank. Formally: findCustomerByIdentityNumber(Tuple{identityNumber = request.identityNumber}) = null

Once it has been provided:

Customer registered: The person is a customer, under the login they asked with.

Required by Customer. Formally: Customer.allInstances()->exists(c | c.customerNumber = response.customerNumber and c.name = request.name and c.login = caller)

Exceptions

When a pre-condition does not hold, the Register as customer service is not provided. Instead, it raises the exception belonging to that pre-condition, which the requester may handle. These are the ways in which the service can fail:

Identity not yet registered not met, raised when Identity not yet registered does not hold: Raised when 'Register as customer' is requested while 'Identity not yet registered' does not hold.

Request data structure

The information a requester provides when asking for the service is a Bank::Customer Register::Request.

What is supplied when requesting 'Register as customer'.

Figure 6. The Bank::Customer Register::Request data structure, fully expanded.

A Bank::Customer Register::Request has:

one name, a Bank::Text: The person’s name.
one identityNumber, a Bank::Text: The number on their identity document.

Response data structure

The information the service returns once provided is a Bank::Customer Register::Response.

What 'Register as customer' yields once rendered.

Figure 7. The Bank::Customer Register::Response data structure, fully expanded.

A Bank::Customer Register::Response has:

one customerNumber, an Bank::Identifier: Their new customer number.

Responsibility allocation

The responsibility allocation diagram below shows how the Register as customer process takes care of each requirement of the Register as customer service. It shows which of its steps addresses each pre- and post-condition, and which services it uses from other responsibility domains to do so.

Figure 8. Responsibility allocation for the Register as customer process.

Requirement by requirement:

Identity not yet registered (pre-condition) is addressed by checking it before anything else is done.
Customer registered (post-condition) is addressed by requesting the Record customer service from Customer Register.

To do so the process uses the following services:

From Customer Register:
- Record customer: Records a new customer and issues their customer number.

Business process

Records the person as a customer under the login they asked with.

The Register as customer business process provides the Register as customer service. The diagram below shows its flow. The numbered steps after it describe the same flow in words, with each choice, loop and parallel flow holding its own steps beneath it.

Figure 9. The business process Register as customer.

Step by step:

Check that Identity not yet registered holds. If it does not, stop and raise Identity not yet registered not met.

Formally: findCustomerByIdentityNumber(Tuple{identityNumber = request.identityNumber}) = null
Request the Record customer service from Customer Register.

This step addresses Customer registered.

The request is populated as follows:
- name: providerRequest.name = request.name
- identityNumber: providerRequest.identityNumber = request.identityNumber
- login: providerRequest.login = caller
  
  The answer is kept as recorded, one Bank::Customer Register::Response.
- If the service is provided:
  1. Populate the response.
    
    customerNumber: response.customerNumber = recorded.customerNumber

4.1.2. Service: Record customer

Customer Register provides the Record customer service.

Records a new customer and issues their customer number.

Service requirements

The functional requirements diagram below shows who has an interest in the Record customer service, i.e. its stakeholders, and what each requires of it. A pre-condition is a condition which must hold for the service to be provided at all. When one does not, the request is refused with an exception. A post-condition is what must be true once the service has been provided, i.e. what it must have achieved.

Figure 10. Functional requirements of the Record customer service.

Its stakeholders, and what each requires of it, are:

Bank: The bank: its shared vocabulary and the departments that answer for its services.

Bank requires the pre-condition Identity not yet registered.
Customer Register: Who the bank’s customers are.

Customer Register requires the post-conditions Customer recorded and Customer number is new.

It is provided only when:

Identity not yet registered: Each person is registered once, by their identity document.

Required by Bank. Formally: Customer.allInstances()->forAll(c | c.identityNumber <> request.identityNumber)

Once it has been provided:

Customer recorded: The customer is on record with the details given.

Required by Customer Register. Formally: Customer.allInstances()->exists(c | c.customerNumber = response.customerNumber and c.name = request.name and c.identityNumber = request.identityNumber and c.login = request.login)
Customer number is new: The number issued belonged to no customer before.

Required by Customer Register. Formally: Customer.allInstances@pre()->forAll(c | c.customerNumber <> response.customerNumber)

Exceptions

When a pre-condition does not hold, the Record customer service is not provided. Instead, it raises the exception belonging to that pre-condition, which the requester may handle. These are the ways in which the service can fail:

Identity not yet registered not met, raised when Identity not yet registered does not hold: Raised when 'Record customer' is requested while 'Identity not yet registered' does not hold.

Request data structure

The information a requester provides when asking for the service is a Bank::Customer Register::Request.

What is supplied when requesting 'Record customer'.

Figure 11. The Bank::Customer Register::Request data structure, fully expanded.

A Bank::Customer Register::Request has:

one name, a Bank::Text: The customer’s name.
one identityNumber, a Bank::Text: The number on their identity document.
one login, a Bank::Text: The login identity they will use.

Response data structure

The information the service returns once provided is a Bank::Customer Register::Response.

What 'Record customer' yields once rendered.

Figure 12. The Bank::Customer Register::Response data structure, fully expanded.

A Bank::Customer Register::Response has:

one customerNumber, an Bank::Identifier: The number issued.

Business process

No business process is needed. The service’s post-conditions say exactly what it records, i.e. it creates a Customer. It is thus provided by making that one change.

4.1.3. Service: getCustomer

Customer Register provides the getCustomer service. It is a query, i.e. it answers from information already held and changes nothing.

Gives the customer with the customer number asked for, as its owning domain holds it. Generated from the entity; generate again rather than editing it.

Service requirements

The functional requirements diagram below shows who has an interest in the getCustomer service, i.e. its stakeholders, and what each requires of it. A pre-condition is a condition which must hold for the service to be provided at all. When one does not, the request is refused with an exception. A post-condition is what must be true once the service has been provided, i.e. what it must have achieved.

Figure 13. Functional requirements of the getCustomer service.

It is provided only when:

Customer exists: There is a customer with that customer number.

Formally: Customer.allInstances()->exists(e | e.customerNumber = request.customerNumber)

Once it has been provided:

Customer given: Every stored field of the customer with that customer number, an association as its target’s identity.

Formally: response.customerNumber = Customer.allInstances()->any(e | e.customerNumber = request.customerNumber).customerNumber and response.identityNumber = Customer.allInstances()->any(e | e.customerNumber = request.customerNumber).identityNumber and response.login = Customer.allInstances()->any(e | e.customerNumber = request.customerNumber).login and response.name = Customer.allInstances()->any(e | e.customerNumber = request.customerNumber).name

Exceptions

When a pre-condition does not hold, the getCustomer service is not provided. Instead, it raises the exception belonging to that pre-condition, which the requester may handle. These are the ways in which the service can fail:

Customer exists not met, raised when Customer exists does not hold: Raised when 'getCustomer' is requested while 'Customer exists' does not hold.

Request data structure

The information a requester provides when asking for the service is a Bank::Customer Register::Request.

What is supplied when requesting 'getCustomer'.

Figure 14. The Bank::Customer Register::Request data structure, fully expanded.

A Bank::Customer Register::Request has:

one customerNumber, an Bank::Identifier: The customer number of the customer asked for.

Response data structure

The information the service returns once provided is a Bank::Customer Register::Response.

What 'getCustomer' yields once rendered.

Figure 15. The Bank::Customer Register::Response data structure, fully expanded.

A Bank::Customer Register::Response has:

one customerNumber, an Bank::Identifier: The customer’s customer number.
one identityNumber, a Bank::Text: The customer’s identity number.
one login, a Bank::Text: The customer’s login.
one name, a Bank::Text: The customer’s name.

Business process

No business process providing this service has been specified yet.

4.1.4. Service: findCustomerByIdentityNumber

Customer Register provides the findCustomerByIdentityNumber service. It is a query, i.e. it answers from information already held and changes nothing.

Gives the customer with the identity number asked for, as its owning domain holds it. Generated from the entity; generate again rather than editing it.

Service requirements

The functional requirements diagram below shows who has an interest in the findCustomerByIdentityNumber service, i.e. its stakeholders, and what each requires of it. A pre-condition is a condition which must hold for the service to be provided at all. When one does not, the request is refused with an exception. A post-condition is what must be true once the service has been provided, i.e. what it must have achieved.

Figure 16. Functional requirements of the findCustomerByIdentityNumber service.

It is provided only when:

Customer with that identity number exists: There is a customer with that identity number.

Formally: Customer.allInstances()->exists(e | e.identityNumber = request.identityNumber)

Once it has been provided:

Customer given: Every stored field of the customer with that identity number, an association as its target’s identity.

Formally: response.customerNumber = Customer.allInstances()->any(e | e.identityNumber = request.identityNumber).customerNumber and response.identityNumber = Customer.allInstances()->any(e | e.identityNumber = request.identityNumber).identityNumber and response.login = Customer.allInstances()->any(e | e.identityNumber = request.identityNumber).login and response.name = Customer.allInstances()->any(e | e.identityNumber = request.identityNumber).name

Exceptions

When a pre-condition does not hold, the findCustomerByIdentityNumber service is not provided. Instead, it raises the exception belonging to that pre-condition, which the requester may handle. These are the ways in which the service can fail:

Customer with that identity number exists not met, raised when Customer with that identity number exists does not hold: Raised when 'findCustomerByIdentityNumber' is requested while 'Customer with that identity number exists' does not hold.

Request data structure

The information a requester provides when asking for the service is a Bank::Customer Register::Request.

What is supplied when requesting 'findCustomerByIdentityNumber'.

Figure 17. The Bank::Customer Register::Request data structure, fully expanded.

A Bank::Customer Register::Request has:

one identityNumber, a Bank::Text: The identity number of the customer asked for.

Response data structure

The information the service returns once provided is a Bank::Customer Register::Response.

What 'findCustomerByIdentityNumber' yields once rendered.

Figure 18. The Bank::Customer Register::Response data structure, fully expanded.

A Bank::Customer Register::Response has:

one customerNumber, an Bank::Identifier: The customer’s customer number.
one identityNumber, a Bank::Text: The customer’s identity number.
one login, a Bank::Text: The customer’s login.
one name, a Bank::Text: The customer’s name.

Business process

No business process providing this service has been specified yet.

4.1.5. Service: findCustomerByLogin

Customer Register provides the findCustomerByLogin service. It is a query, i.e. it answers from information already held and changes nothing.

Gives the customer with the login asked for, as its owning domain holds it. Generated from the entity; generate again rather than editing it.

Service requirements

The functional requirements diagram below shows who has an interest in the findCustomerByLogin service, i.e. its stakeholders, and what each requires of it. A pre-condition is a condition which must hold for the service to be provided at all. When one does not, the request is refused with an exception. A post-condition is what must be true once the service has been provided, i.e. what it must have achieved.

Figure 19. Functional requirements of the findCustomerByLogin service.

It is provided only when:

Customer with that login exists: There is a customer with that login.

Formally: Customer.allInstances()->exists(e | e.login = request.login)

Once it has been provided:

Customer given: Every stored field of the customer with that login, an association as its target’s identity.

Formally: response.customerNumber = Customer.allInstances()->any(e | e.login = request.login).customerNumber and response.identityNumber = Customer.allInstances()->any(e | e.login = request.login).identityNumber and response.login = Customer.allInstances()->any(e | e.login = request.login).login and response.name = Customer.allInstances()->any(e | e.login = request.login).name

Exceptions

When a pre-condition does not hold, the findCustomerByLogin service is not provided. Instead, it raises the exception belonging to that pre-condition, which the requester may handle. These are the ways in which the service can fail:

Customer with that login exists not met, raised when Customer with that login exists does not hold: Raised when 'findCustomerByLogin' is requested while 'Customer with that login exists' does not hold.

Request data structure

The information a requester provides when asking for the service is a Bank::Customer Register::Request.

What is supplied when requesting 'findCustomerByLogin'.

Figure 20. The Bank::Customer Register::Request data structure, fully expanded.

A Bank::Customer Register::Request has:

one login, a Bank::Text: The login of the customer asked for.

Response data structure

The information the service returns once provided is a Bank::Customer Register::Response.

What 'findCustomerByLogin' yields once rendered.

Figure 21. The Bank::Customer Register::Response data structure, fully expanded.

A Bank::Customer Register::Response has:

one customerNumber, an Bank::Identifier: The customer’s customer number.
one identityNumber, a Bank::Text: The customer’s identity number.
one login, a Bank::Text: The customer’s login.
one name, a Bank::Text: The customer’s name.

Business process

No business process providing this service has been specified yet.

4.2. Entities

An entity is information which Customer Register keeps over time. It is a record which outlives any one request, and which its services create, change and read. Customer Register maintains the following entities:

Customer: A person the bank has registered as a customer.

The entity map below shows each entity together with its facets, i.e. the data structures whose fields make up what it stores.

Figure 22. The entities maintained by Customer Register.

4.2.1. Entity: Customer

A person the bank has registered as a customer.

An entity: a business object with an identity, whose state the bank keeps. Its fields are those of the views that project it — here CustomerRecord.

How it is populated

Customer is populated as follows:

The Record customer service creates a Customer, identified by customerNumber.
The CustomerRecord data structure describes part of what it holds: The bank’s record of one customer.

Entity structure

The diagram below shows the Customer entity fully expanded, i.e. everything it holds, gathered from all of its facets, and the information it is related to. The same structure is described in words after it.

Figure 23. The Customer entity, fully expanded.

A Customer has:

one customerNumber, an Bank::Identifier, which identifies it: The customer’s number.
one name, a Bank::Text: The customer’s name.
one identityNumber, a Bank::Text, unique: The number on the identity document the customer registered with.
one login, a Bank::Text, unique: The login identity the customer uses — what `caller` is compared with.

Data dictionary

This section lists what Customer stores, attribute by attribute. An attribute gathers every field of that name in the entity’s facets. Where it gathers more than one, each is listed, since fields of one name are stored as one attribute whatever each was meant to hold. The services listed write or read it as their specifications say.

Attribute Type Role Multiplicity Unique Personal data Merged from Written by Read by

Attribute	Type	Role	Multiplicity	Unique	Personal data	Merged from	Written by	Read by
`customerNumber`	Bank::Identifier	identifies	`1`	yes	—	—	Record customer	findCustomerByIdentityNumber, getCustomer and findCustomerByLogin
`name`	Bank::Text	states	`1`	no	personal	—	Record customer	findCustomerByIdentityNumber, getCustomer and findCustomerByLogin
`identityNumber`	Bank::Text	states	`1`	yes	personal, retention obligated	—	Record customer	findCustomerByIdentityNumber, getCustomer, Record customer and findCustomerByLogin
`login`	Bank::Text	states	`1`	yes	personal	—	Record customer	findCustomerByIdentityNumber, getCustomer and findCustomerByLogin

customerNumber

Bank::Identifier

identifies

1

yes

—

Record customer

findCustomerByIdentityNumber, getCustomer and findCustomerByLogin

name

Bank::Text

states

1

personal

—

Record customer

findCustomerByIdentityNumber, getCustomer and findCustomerByLogin

identityNumber

Bank::Text

states

1

yes

personal, retention obligated

—

Record customer

findCustomerByIdentityNumber, getCustomer, Record customer and findCustomerByLogin

login

Bank::Text

states

1

yes

personal

—

Record customer

findCustomerByIdentityNumber, getCustomer and findCustomerByLogin

5. Bank / Accounts

This part specifies the Accounts responsibility domain. A responsibility domain is an area of responsibility, e.g. a business unit, a role or a system, which provides services to others and may in turn rely on services of other domains.

The bank’s accounts: opening, looking up and closing them.

Offers the use cases about an account itself — opening it, closing it, asking its balance. Accounts does not change a balance — that is the ledger's alone.

The scope diagram below shows what Accounts is responsible for, i.e. the services it provides and the lower-level responsibility domains it contains.

Figure 24. The scope of Accounts.

5.1. Services

Accounts is responsible for providing the following services. Each is described in its own section below: what it requires and what it guarantees (its service requirements), the information exchanged with it, how the work is allocated to the responsibility domains taking part, and the business process providing it.

Open account: A customer opens a new account.
Get balance: Reports what an account holds.
Close account: The holder closes an account they have emptied.
allAccountsOpen: Says whether every account in a list is open.
Create account: Opens a new, empty account for a registered customer.
Retrieve account: Looks an account up by its number.
Close account record: Marks an emptied account closed, keeping its record.
getAccount: Gives the account with the account number asked for, as its owning domain holds it. Generated from the entity; generate again rather than editing it.

5.1.1. Service: Open account

Accounts provides the Open account service.

A customer opens a new account.

Service requirements

The functional requirements diagram below shows who has an interest in the Open account service, i.e. its stakeholders, and what each requires of it. A pre-condition is a condition which must hold for the service to be provided at all. When one does not, the request is refused with an exception. A post-condition is what must be true once the service has been provided, i.e. what it must have achieved.

Figure 25. Functional requirements of the Open account service.

Its stakeholders, and what each requires of it, are:

Bank: The bank: its shared vocabulary and the departments that answer for its services.

Bank requires the pre-condition Customer is registered.
Customer: A customer of the bank, to whom the bank’s services are offered.

Customer requires the post-conditions Account opened and Holder advised.

It is provided only when:

Customer is registered: Only a customer can open an account.

Required by Bank. Formally: getCustomer(Tuple{customerNumber = request.customerNumber}) <> null

Once it has been provided:

Account opened: An open, empty account of that type now exists for the customer.

Required by Customer. Formally: Account.allInstances()->exists(a | a.accountNumber = response.accountNumber and a.holder = request.customerNumber and a.accountType = request.accountType and a.balance = 0 and a.status = AccountStatus::open)
Holder advised: The customer is told the account is open.

Required by Customer.

While meeting it, the service sends:
- AccountAdvice sent, carrying an Bank::AccountAdvice, to Customer, as a notification which any number of parties may act on

Exceptions

When a pre-condition does not hold, the Open account service is not provided. Instead, it raises the exception belonging to that pre-condition, which the requester may handle. These are the ways in which the service can fail:

Customer is registered not met, raised when Customer is registered does not hold: Raised when 'Open account' is requested while 'Customer is registered' does not hold.

Request data structure

The information a requester provides when asking for the service is a Bank::Accounts::Request.

What is supplied when requesting 'Open account'.

Figure 26. The Bank::Accounts::Request data structure, fully expanded.

A Bank::Accounts::Request has:

one customerNumber, an Bank::Identifier: The customer opening it.
one accountType, an Bank::AccountType: Current or savings.

One of current and savings.

Response data structure

The information the service returns once provided is a Bank::Accounts::Response.

What 'Open account' yields once rendered.

Figure 27. The Bank::Accounts::Response data structure, fully expanded.

A Bank::Accounts::Response has:

one accountNumber, an Bank::Identifier: The new account’s number.

Responsibility allocation

The responsibility allocation diagram below shows how the Open account process takes care of each requirement of the Open account service. It shows which of its steps addresses each pre- and post-condition, and which services it uses from other responsibility domains to do so.

Figure 28. Responsibility allocation for the Open account process.

Requirement by requirement:

Customer is registered (pre-condition) is addressed by checking it before anything else is done.
Account opened (post-condition) is addressed by requesting the Create account service from Accounts.
Holder advised (post-condition) is addressed by sending Bank::AccountAdvice.

To do so the process uses the following services:

From Accounts:
- Create account: Opens a new, empty account for a registered customer.

Business process

Opens the account in Accounts, then advises the customer.

The Open account business process provides the Open account service. The diagram below shows its flow. The numbered steps after it describe the same flow in words, with each choice, loop and parallel flow holding its own steps beneath it.

Figure 29. The business process Open account.

Step by step:

Check that Customer is registered holds. If it does not, stop and raise Customer is registered not met.

Formally: getCustomer(Tuple{customerNumber = request.customerNumber}) <> null
Request the Create account service from Accounts.

This step addresses Account opened.

The request is populated as follows:
- holder: providerRequest.holder = request.customerNumber
- accountType: providerRequest.accountType = request.accountType
  
  The answer is kept as opened, one Bank::Accounts::Response.
- If the service is provided:
  1. Send an Bank::AccountAdvice to Customer (the one given by request.customerNumber), as a notification which any number of parties may act on.
    
    This step addresses Holder advised.
    
    accountNumber: sent.accountNumber = opened.accountNumber
    
    notice: sent.notice = 'Your account is open.'
  2. Populate the response.
    
    accountNumber: response.accountNumber = opened.accountNumber

5.1.2. Service: Get balance

Accounts provides the Get balance service. It is a query, i.e. it answers from information already held and changes nothing.

Reports what an account holds.

A function, and so it cannot ask who is asking: two callers asking about one account must get the same answer, and caller would let them differ. Who may see a balance is therefore decided by whom the service is published to, not by a pre-condition — a real trade-off, and one a model should state rather than hide.

Service requirements

The functional requirements diagram below shows who has an interest in the Get balance service, i.e. its stakeholders, and what each requires of it. A pre-condition is a condition which must hold for the service to be provided at all. When one does not, the request is refused with an exception. A post-condition is what must be true once the service has been provided, i.e. what it must have achieved.

Figure 30. Functional requirements of the Get balance service.

Its stakeholders, and what each requires of it, are:

Bank: The bank: its shared vocabulary and the departments that answer for its services.

Bank requires the pre-condition Account exists.
Customer: A customer of the bank, to whom the bank’s services are offered.

Customer requires the post-condition Balance reported.

It is provided only when:

Account exists: There is an account with that number.

Required by Bank. Formally: getAccount(Tuple{accountNumber = request.accountNumber}) <> null

Once it has been provided:

Balance reported: The response states the account’s balance.

Required by Customer. Formally: Account.allInstances()->select(a | a.accountNumber = request.accountNumber)->forAll(a | response.balance = a.balance)

Exceptions

When a pre-condition does not hold, the Get balance service is not provided. Instead, it raises the exception belonging to that pre-condition, which the requester may handle. These are the ways in which the service can fail:

Account exists not met, raised when Account exists does not hold: Raised when 'Get balance' is requested while 'Account exists' does not hold.

Request data structure

The information a requester provides when asking for the service is a Bank::Accounts::Request.

What is supplied when requesting 'Get balance'.

Figure 31. The Bank::Accounts::Request data structure, fully expanded.

A Bank::Accounts::Request has:

one accountNumber, an Bank::Identifier: The account.

Response data structure

The information the service returns once provided is a Bank::Accounts::Response.

What 'Get balance' yields once rendered.

Figure 32. The Bank::Accounts::Response data structure, fully expanded.

A Bank::Accounts::Response has:

one balance, a Bank::Money: What it holds.

Responsibility allocation

The responsibility allocation diagram below shows how the Get balance process takes care of each requirement of the Get balance service. It shows which of its steps addresses each pre- and post-condition, and which services it uses from other responsibility domains to do so.

Figure 33. Responsibility allocation for the Get balance process.

Requirement by requirement:

Account exists (pre-condition) is addressed by checking it before anything else is done.
Balance reported (post-condition) is addressed by populating the response.

To do so the process uses the following services:

From Accounts:
- Retrieve account: Looks an account up by its number.

Business process

Looks the account up and reports its balance.

A function's process may only be orchestrated across functions — which Retrieve account is.

The Get balance business process provides the Get balance service. The diagram below shows its flow. The numbered steps after it describe the same flow in words, with each choice, loop and parallel flow holding its own steps beneath it.

Figure 34. The business process Get balance.

Step by step:

Check that Account exists holds. If it does not, stop and raise Account exists not met.

Formally: getAccount(Tuple{accountNumber = request.accountNumber}) <> null
Request the Retrieve account service from Accounts.

The request is populated as follows:
- accountNumber: providerRequest.accountNumber = request.accountNumber
  
  The answer is kept as found, one Bank::Accounts::Response.
- If the service is provided:
  1. Populate the response.
    
    This step addresses Balance reported.
    
    balance: response.balance = found.account.balance

5.1.3. Service: Close account

Accounts provides the Close account service.

The holder closes an account they have emptied.

Service requirements

The functional requirements diagram below shows who has an interest in the Close account service, i.e. its stakeholders, and what each requires of it. A pre-condition is a condition which must hold for the service to be provided at all. When one does not, the request is refused with an exception. A post-condition is what must be true once the service has been provided, i.e. what it must have achieved.

Figure 35. Functional requirements of the Close account service.

Its stakeholders, and what each requires of it, are:

Bank: The bank: its shared vocabulary and the departments that answer for its services.

Bank requires the pre-conditions Account is open, Requested by the holder and Account is empty and the post-condition Account closed.
Customer: A customer of the bank, to whom the bank’s services are offered.

Customer requires the pre-conditions Requested by the holder and Account is empty and the post-conditions Account closed and Holder advised.

It is provided only when:

Account is open: Only an open account can be closed.

Required by Bank. Formally: let a = getAccount(Tuple{accountNumber = request.accountNumber}) in a <> null and a.status = AccountStatus::open
Requested by the holder: Only the holder may close the account.

Required by Bank and Customer. Formally: let a = getAccount(Tuple{accountNumber = request.accountNumber}) in a <> null and (let c = findCustomerByLogin(Tuple{login = caller}) in c <> null and a.holder = c.customerNumber)
Account is empty: An account is closed only once nothing is left in it.

Required by Bank and Customer. Formally: let a = getAccount(Tuple{accountNumber = request.accountNumber}) in a <> null and a.balance = 0

Once it has been provided:

Account closed: The account is closed, and its record kept.

Required by Bank and Customer. Formally: Account.allInstances()->select(a | a.accountNumber = request.accountNumber)->forAll(a | a.status = AccountStatus::closed) and Account.allInstances()->size() = Account.allInstances@pre()->size()
Holder advised: The customer is told the account is closed.

Required by Customer.

While meeting it, the service sends:
- AccountAdvice sent, carrying an Bank::AccountAdvice, to Customer, as a notification which any number of parties may act on

Exceptions

When a pre-condition does not hold, the Close account service is not provided. Instead, it raises the exception belonging to that pre-condition, which the requester may handle. These are the ways in which the service can fail:

Account is open not met, raised when Account is open does not hold: Raised when 'Close account' is requested while 'Account is open' does not hold.
Requested by the holder not met, raised when Requested by the holder does not hold: Raised when 'Close account' is requested while 'Requested by the holder' does not hold.
Account is empty not met, raised when Account is empty does not hold: Raised when 'Close account' is requested while 'Account is empty' does not hold.

Request data structure

The information a requester provides when asking for the service is a Bank::Accounts::Request.

What is supplied when requesting 'Close account'.

Figure 36. The Bank::Accounts::Request data structure, fully expanded.

A Bank::Accounts::Request has:

one accountNumber, an Bank::Identifier: The account to close.

Response data structure

The information the service returns once provided is a Bank::Accounts::Response.

What 'Close account' yields once rendered.

Figure 37. The Bank::Accounts::Response data structure, fully expanded.

A Bank::Accounts::Response carries no information of its own.

Responsibility allocation

The responsibility allocation diagram below shows how the Close account process takes care of each requirement of the Close account service. It shows which of its steps addresses each pre- and post-condition, and which services it uses from other responsibility domains to do so.

Figure 38. Responsibility allocation for the Close account process.

Requirement by requirement:

Account is open (pre-condition) is addressed by checking it before anything else is done.
Requested by the holder (pre-condition) is addressed by checking it before anything else is done.
Account is empty (pre-condition) is addressed by checking it before anything else is done.
Account closed (post-condition) is addressed by requesting the Close account record service from Accounts.
Holder advised (post-condition) is addressed by sending Bank::AccountAdvice.

To do so the process uses the following services:

From Accounts:
- Close account record: Marks an emptied account closed, keeping its record.

Business process

Closes the account record, then advises the holder.

The Close account business process provides the Close account service. The diagram below shows its flow. The numbered steps after it describe the same flow in words, with each choice, loop and parallel flow holding its own steps beneath it.

Figure 39. The business process Close account.

Step by step:

Check that Account is open holds. If it does not, stop and raise Account is open not met.

Formally: let a = getAccount(Tuple{accountNumber = request.accountNumber}) in a <> null and a.status = AccountStatus::open
Check that Requested by the holder holds. If it does not, stop and raise Requested by the holder not met.

Formally: let a = getAccount(Tuple{accountNumber = request.accountNumber}) in a <> null and (let c = findCustomerByLogin(Tuple{login = caller}) in c <> null and a.holder = c.customerNumber)
Check that Account is empty holds. If it does not, stop and raise Account is empty not met.

Formally: let a = getAccount(Tuple{accountNumber = request.accountNumber}) in a <> null and a.balance = 0
Request the Close account record service from Accounts.

This step addresses Account closed.

The request is populated as follows:
- accountNumber: providerRequest.accountNumber = request.accountNumber
Send an Bank::AccountAdvice to Customer (the one given by request.accountNumber), as a notification which any number of parties may act on.

This step addresses Holder advised.
- accountNumber: sent.accountNumber = request.accountNumber
- notice: sent.notice = 'Your account is closed.'
Populate the response.

5.1.4. Service: allAccountsOpen

Accounts provides the allAccountsOpen service. It is a query, i.e. it answers from information already held and changes nothing.

Says whether every account in a list is open.

A query service written by hand, beside the generated getAccount: a payroll asks about every payee's account at once, and a function is answered for what it is applied to — here the whole list, which is what lets Pay salaries ask it in one pre-condition (docs/design/domainOwnedEntityData.md P2).

Service requirements

The functional requirements diagram below shows who has an interest in the allAccountsOpen service, i.e. its stakeholders, and what each requires of it. A pre-condition is a condition which must hold for the service to be provided at all. When one does not, the request is refused with an exception. A post-condition is what must be true once the service has been provided, i.e. what it must have achieved.

Figure 40. Functional requirements of the allAccountsOpen service.

Its stakeholders, and what each requires of it, are:

Ledger: The only thing that moves money, and the record of every movement.

Ledger requires the post-condition Openness given.

Once it has been provided:

Openness given: Whether each account named is on record and open.

Required by Ledger. Formally: response.allOpen = request.accountNumbers->forAll(n | Account.allInstances()->exists(a | a.accountNumber = n and a.status = AccountStatus::open))

Request data structure

The information a requester provides when asking for the service is a Bank::Accounts::Request.

What is supplied when requesting 'allAccountsOpen'.

Figure 41. The Bank::Accounts::Request data structure, fully expanded.

A Bank::Accounts::Request has:

any number of accountNumbers, each an Bank::Identifier: The accounts asked about.

Response data structure

The information the service returns once provided is a Bank::Accounts::Response.

What 'allAccountsOpen' yields once rendered.

Figure 42. The Bank::Accounts::Response data structure, fully expanded.

A Bank::Accounts::Response has:

one allOpen, a Bank::Flag: Whether every one of them is an open account.

Business process

No business process providing this service has been specified yet.

5.1.5. Service: Create account

Accounts provides the Create account service.

Opens a new, empty account for a registered customer.

Service requirements

The functional requirements diagram below shows who has an interest in the Create account service, i.e. its stakeholders, and what each requires of it. A pre-condition is a condition which must hold for the service to be provided at all. When one does not, the request is refused with an exception. A post-condition is what must be true once the service has been provided, i.e. what it must have achieved.

Figure 43. Functional requirements of the Create account service.

Its stakeholders, and what each requires of it, are:

Accounts: The bank’s accounts: opening, looking up and closing them.

Accounts requires the post-conditions Account created and Account number is new.
Bank: The bank: its shared vocabulary and the departments that answer for its services.

Bank requires the pre-condition Holder is registered.

It is provided only when:

Holder is registered: An account is opened only for a registered customer.

Required by Bank. Formally: getCustomer(Tuple{customerNumber = request.holder}) <> null

Once it has been provided:

Account created: An open, empty account of the type asked for exists for the holder.

Required by Accounts. Formally: Account.allInstances()->exists(a | a.accountNumber = response.accountNumber and a.holder = request.holder and a.accountType = request.accountType and a.balance = 0 and a.status = AccountStatus::open)
Account number is new: The number issued belonged to no account before.

Required by Accounts. Formally: Account.allInstances@pre()->forAll(a | a.accountNumber <> response.accountNumber)

Exceptions

When a pre-condition does not hold, the Create account service is not provided. Instead, it raises the exception belonging to that pre-condition, which the requester may handle. These are the ways in which the service can fail:

Holder is registered not met, raised when Holder is registered does not hold: Raised when 'Create account' is requested while 'Holder is registered' does not hold.

Request data structure

The information a requester provides when asking for the service is a Bank::Accounts::Request.

What is supplied when requesting 'Create account'.

Figure 44. The Bank::Accounts::Request data structure, fully expanded.

A Bank::Accounts::Request has:

one holder, an Bank::Identifier: The customer number of the holder.
one accountType, an Bank::AccountType: The kind of account.

One of current and savings.

Response data structure

The information the service returns once provided is a Bank::Accounts::Response.

What 'Create account' yields once rendered.

Figure 45. The Bank::Accounts::Response data structure, fully expanded.

A Bank::Accounts::Response has:

one accountNumber, an Bank::Identifier: The number issued.

Business process

No business process is needed. The service’s post-conditions say exactly what it records, i.e. it creates an Account. It is thus provided by making that one change.

5.1.6. Service: Retrieve account

Accounts provides the Retrieve account service. It is a query, i.e. it answers from information already held and changes nothing.

Looks an account up by its number.

A function: asking changes nothing, so it may be asked any number of times, cached, and applied inside a constraint. It may only be orchestrated across other functions, and its own conditions may not depend on caller or now().

Service requirements

The functional requirements diagram below shows who has an interest in the Retrieve account service, i.e. its stakeholders, and what each requires of it. A pre-condition is a condition which must hold for the service to be provided at all. When one does not, the request is refused with an exception. A post-condition is what must be true once the service has been provided, i.e. what it must have achieved.

Figure 46. Functional requirements of the Retrieve account service.

Its stakeholders, and what each requires of it, are:

Accounts: The bank’s accounts: opening, looking up and closing them.

Accounts requires the pre-condition Account exists and the post-condition Account reported.
Ledger: The only thing that moves money, and the record of every movement.

Ledger requires the post-condition Account reported.

It is provided only when:

Account exists: There is an account with that number.

Required by Accounts. Formally: Account.allInstances()->exists(a | a.accountNumber = request.accountNumber)

Once it has been provided:

Account reported: The account is reported as it stands.

Required by Accounts and Ledger. Formally: Account.allInstances()->select(a | a.accountNumber = request.accountNumber)->forAll(a | response.account.accountNumber = a.accountNumber and response.account.holder = a.holder and response.account.balance = a.balance and response.account.status = a.status)

Exceptions

When a pre-condition does not hold, the Retrieve account service is not provided. Instead, it raises the exception belonging to that pre-condition, which the requester may handle. These are the ways in which the service can fail:

Account exists not met, raised when Account exists does not hold: Raised when 'Retrieve account' is requested while 'Account exists' does not hold.

Request data structure

The information a requester provides when asking for the service is a Bank::Accounts::Request.

What is supplied when requesting 'Retrieve account'.

Figure 47. The Bank::Accounts::Request data structure, fully expanded.

A Bank::Accounts::Request has:

one accountNumber, an Bank::Identifier: The account to look up.

Response data structure

The information the service returns once provided is a Bank::Accounts::Response.

What 'Retrieve account' yields once rendered.

Figure 48. The Bank::Accounts::Response data structure, fully expanded.

A Bank::Accounts::Response has:

one account, an Bank::Accounts::AccountRecord: The account as it stands.

Bank::Accounts::AccountRecord: The bank’s record of one account.

An Bank::Accounts::AccountRecord has:

one accountNumber, an Bank::Identifier, which identifies it: The account’s number.
one holder, an Bank::Identifier: The customer number of the account’s holder.
one accountType, an Bank::AccountType: Current or savings.

One of current and savings.
one balance, a Bank::Money: What the account holds.
one status, an Bank::AccountStatus: Open or closed.

One of open and closed.

The following must always hold for an Bank::Accounts::AccountRecord:

No overdraft: self.balance >= 0

Business process

No business process providing this service has been specified yet.

5.1.7. Service: Close account record

Accounts provides the Close account record service.

Marks an emptied account closed, keeping its record.

Service requirements

The functional requirements diagram below shows who has an interest in the Close account record service, i.e. its stakeholders, and what each requires of it. A pre-condition is a condition which must hold for the service to be provided at all. When one does not, the request is refused with an exception. A post-condition is what must be true once the service has been provided, i.e. what it must have achieved.

Figure 49. Functional requirements of the Close account record service.

Its stakeholders, and what each requires of it, are:

Accounts: The bank’s accounts: opening, looking up and closing them.

Accounts requires the pre-condition Account is open and the post-condition Account closed.
Bank: The bank: its shared vocabulary and the departments that answer for its services.

Bank requires the pre-condition Account is empty and the post-condition Account record kept.

It is provided only when:

Account is open: Only an open account can be closed.

Required by Accounts. Formally: let a = getAccount(Tuple{accountNumber = request.accountNumber}) in a <> null and a.status = AccountStatus::open
Account is empty: An account is closed only once nothing is left in it.

Required by Bank. Formally: let a = getAccount(Tuple{accountNumber = request.accountNumber}) in a <> null and a.balance = 0

Once it has been provided:

Account closed: The account is closed.

Required by Accounts. Formally: Account.allInstances()->select(a | a.accountNumber = request.accountNumber)->forAll(a | a.status = AccountStatus::closed)
Account record kept: No account record is removed — closing is not deleting.

Required by Bank. Formally: Account.allInstances()->size() = Account.allInstances@pre()->size()

Exceptions

When a pre-condition does not hold, the Close account record service is not provided. Instead, it raises the exception belonging to that pre-condition, which the requester may handle. These are the ways in which the service can fail:

Account is open not met, raised when Account is open does not hold: Raised when 'Close account record' is requested while 'Account is open' does not hold.
Account is empty not met, raised when Account is empty does not hold: Raised when 'Close account record' is requested while 'Account is empty' does not hold.

Request data structure

The information a requester provides when asking for the service is a Bank::Accounts::Request.

What is supplied when requesting 'Close account record'.

Figure 50. The Bank::Accounts::Request data structure, fully expanded.

A Bank::Accounts::Request has:

one accountNumber, an Bank::Identifier: The account to close.

Response data structure

The information the service returns once provided is a Bank::Accounts::Response.

What 'Close account record' yields once rendered.

Figure 51. The Bank::Accounts::Response data structure, fully expanded.

A Bank::Accounts::Response carries no information of its own.

Business process

No business process providing this service has been specified yet.

5.1.8. Service: getAccount

Accounts provides the getAccount service. It is a query, i.e. it answers from information already held and changes nothing.

Gives the account with the account number asked for, as its owning domain holds it. Generated from the entity; generate again rather than editing it.

Service requirements

The functional requirements diagram below shows who has an interest in the getAccount service, i.e. its stakeholders, and what each requires of it. A pre-condition is a condition which must hold for the service to be provided at all. When one does not, the request is refused with an exception. A post-condition is what must be true once the service has been provided, i.e. what it must have achieved.

Figure 52. Functional requirements of the getAccount service.

It is provided only when:

Account exists: There is a account with that account number.

Formally: Account.allInstances()->exists(e | e.accountNumber = request.accountNumber)

Once it has been provided:

Account given: Every stored field of the account with that account number, an association as its target’s identity.

Formally: response.accountNumber = Account.allInstances()->any(e | e.accountNumber = request.accountNumber).accountNumber and response.accountType = Account.allInstances()->any(e | e.accountNumber = request.accountNumber).accountType and response.balance = Account.allInstances()->any(e | e.accountNumber = request.accountNumber).balance and response.holder = Account.allInstances()->any(e | e.accountNumber = request.accountNumber).holder and response.status = Account.allInstances()->any(e | e.accountNumber = request.accountNumber).status

Exceptions

When a pre-condition does not hold, the getAccount service is not provided. Instead, it raises the exception belonging to that pre-condition, which the requester may handle. These are the ways in which the service can fail:

Account exists not met, raised when Account exists does not hold: Raised when 'getAccount' is requested while 'Account exists' does not hold.

Request data structure

The information a requester provides when asking for the service is a Bank::Accounts::Request.

What is supplied when requesting 'getAccount'.

Figure 53. The Bank::Accounts::Request data structure, fully expanded.

A Bank::Accounts::Request has:

one accountNumber, an Bank::Identifier: The account number of the account asked for.

Response data structure

The information the service returns once provided is a Bank::Accounts::Response.

What 'getAccount' yields once rendered.

Figure 54. The Bank::Accounts::Response data structure, fully expanded.

A Bank::Accounts::Response has:

one accountNumber, an Bank::Identifier: The account’s account number.
one accountType, an Bank::AccountType: The account’s account type.

One of current and savings.
one balance, a Bank::Money: The account’s balance.
one holder, an Bank::Identifier: The account’s holder.
one status, an Bank::AccountStatus: The account’s status.

One of open and closed.

Business process

No business process providing this service has been specified yet.

5.2. Entities

An entity is information which Accounts keeps over time. It is a record which outlives any one request, and which its services create, change and read. Accounts maintains the following entities:

Account: A customer’s account at the bank.

The entity map below shows each entity together with its facets, i.e. the data structures whose fields make up what it stores.

Figure 55. The entities maintained by Accounts.

5.2.1. Entity: Account

A customer’s account at the bank.

Identified by its account number. Its balance is changed only by the ledger.

How it is populated

Account is populated as follows:

The Create account service creates an Account, identified by accountNumber.
The AccountRecord data structure describes part of what it holds: The bank’s record of one account.

Entity structure

The diagram below shows the Account entity fully expanded, i.e. everything it holds, gathered from all of its facets, and the information it is related to. The same structure is described in words after it.

Figure 56. The Account entity, fully expanded.

An Account has:

one accountNumber, an Bank::Identifier, which identifies it: The account’s number.
one holder, an Bank::Identifier: The customer number of the account’s holder.
one accountType, an Bank::AccountType: Current or savings.

One of current and savings.
one balance, a Bank::Money: What the account holds.
one status, an Bank::AccountStatus: Open or closed.

One of open and closed.

Data dictionary

This section lists what Account stores, attribute by attribute. An attribute gathers every field of that name in the entity’s facets. Where it gathers more than one, each is listed, since fields of one name are stored as one attribute whatever each was meant to hold. The services listed write or read it as their specifications say.

Attribute Type Role Multiplicity Unique Personal data Merged from Written by Read by

Attribute	Type	Role	Multiplicity	Unique	Personal data	Merged from	Written by	Read by
`accountNumber`	Bank::Identifier	identifies	`1`	yes	—	—	Create account	getAccount, Retrieve account and allAccountsOpen
`holder`	Bank::Identifier	states	`1`	no	—	—	Create account	getAccount
`accountType`	Bank::AccountType	states	`1`	no	—	—	Create account	getAccount
`balance`	Bank::Money	states	`1`	no	—	—	Create account	getAccount
`status`	Bank::AccountStatus	states	`1`	no	—	—	Create account	getAccount and allAccountsOpen

accountNumber

Bank::Identifier

identifies

1

yes

—

Create account

getAccount, Retrieve account and allAccountsOpen

holder

Bank::Identifier

states

1

—

Create account

getAccount

accountType

Bank::AccountType

states

1

—

Create account

getAccount

balance

Bank::Money

states

1

—

Create account

getAccount

status

Bank::AccountStatus

states

1

—

Create account

getAccount and allAccountsOpen

6. Bank / Ledger

This part specifies the Ledger responsibility domain. A responsibility domain is an area of responsibility, e.g. a business unit, a role or a system, which provides services to others and may in turn rely on services of other domains.

The only thing that moves money, and the record of every movement.

Every change to a balance is a ledger posting, and every posting leaves entries behind. A transfer is one posting, so it happens entirely or not at all. Offers the use cases that move money — deposits, withdrawals, transfers, salary runs and large transfers — each realized by requesting the ledger's own postings.

The scope diagram below shows what Ledger is responsible for, i.e. the services it provides and the lower-level responsibility domains it contains.

Figure 57. The scope of Ledger.

6.1. Services

Ledger is responsible for providing the following services. Each is described in its own section below: what it requires and what it guarantees (its service requirements), the information exchanged with it, how the work is allocated to the responsibility domains taking part, and the business process providing it.

Deposit cash: Cash is paid into an account.
Withdraw cash: The holder takes cash out of their account.
Transfer funds: The holder of one account pays money into another.
Pay salaries: An employer pays a batch of salaries from one account.
Transfer large amount: The holder moves more than one posting allows — up to 1000 postings' worth.
Credit account: Adds money to an account and records the entry.
Debit account: Takes money out of an account and records the entry.
Reverse transfer: Moves a posted transfer’s amount back, as one indivisible posting.
Post transfer: Moves money from one account to another as one indivisible posting.

6.1.1. Service: Deposit cash

Ledger provides the Deposit cash service.

Cash is paid into an account.

Anyone may pay into an account, so — unlike a withdrawal — nothing here asks who the caller is.

Service requirements

The functional requirements diagram below shows who has an interest in the Deposit cash service, i.e. its stakeholders, and what each requires of it. A pre-condition is a condition which must hold for the service to be provided at all. When one does not, the request is refused with an exception. A post-condition is what must be true once the service has been provided, i.e. what it must have achieved.

Figure 58. Functional requirements of the Deposit cash service.

Its stakeholders, and what each requires of it, are:

Bank: The bank: its shared vocabulary and the departments that answer for its services.

Bank requires the pre-condition Account is open.
Customer: A customer of the bank, to whom the bank’s services are offered.

Customer requires the post-conditions Balance increased and New balance reported.

It is provided only when:

Account is open: Only an open account is paid into.

Required by Bank. Formally: let a = getAccount(Tuple{accountNumber = request.accountNumber}) in a <> null and a.status = AccountStatus::open

Once it has been provided:

Balance increased: The balance went up by exactly the amount.

Required by Customer. Formally: Account.allInstances()->select(a | a.accountNumber = request.accountNumber)->forAll(a | a.balance = a.balance@pre + request.amount)
New balance reported: The response states the balance after the deposit.

Required by Customer. Formally: Account.allInstances()->select(a | a.accountNumber = request.accountNumber)->forAll(a | response.newBalance = a.balance)

Exceptions

When a pre-condition does not hold, the Deposit cash service is not provided. Instead, it raises the exception belonging to that pre-condition, which the requester may handle. These are the ways in which the service can fail:

Account is open not met, raised when Account is open does not hold: Raised when 'Deposit cash' is requested while 'Account is open' does not hold.

Request data structure

The information a requester provides when asking for the service is a Bank::Ledger::Request.

What is supplied when requesting 'Deposit cash'.

Figure 59. The Bank::Ledger::Request data structure, fully expanded.

A Bank::Ledger::Request has:

one accountNumber, an Bank::Identifier: The account paid into.
one amount, a Bank::Money: How much.

The following must always hold for a Bank::Ledger::Request:

Amount is positive: self.amount > 0

Required by Bank.

Response data structure

The information the service returns once provided is a Bank::Ledger::Response.

What 'Deposit cash' yields once rendered.

Figure 60. The Bank::Ledger::Response data structure, fully expanded.

A Bank::Ledger::Response has:

one newBalance, a Bank::Money: The balance after the deposit.

Responsibility allocation

The responsibility allocation diagram below shows how the Deposit cash process takes care of each requirement of the Deposit cash service. It shows which of its steps addresses each pre- and post-condition, and which services it uses from other responsibility domains to do so.

Figure 61. Responsibility allocation for the Deposit cash process.

Requirement by requirement:

Account is open (pre-condition) is addressed by requesting the Credit account service from Ledger.
Balance increased (post-condition) is addressed by requesting the Credit account service from Ledger.
New balance reported (post-condition) is addressed by populating the response.

To do so the process uses the following services:

From Ledger:
- Credit account: Adds money to an account and records the entry.

Business process

Credits the account through the ledger, and lets the ledger say whether it is open.

Catching an exception, and raising one. This process does not check Account is open itself: the ledger's Credit account has the same pre-condition and refuses a closed account anyway. Checking twice would be two statements of one rule. So the process requests the credit and handles the ledger's refusal — by raising its own Account is open not met, so a customer is refused in this service's terms rather than the ledger's.

Because the request handles an exception, its answer is read only on its success lane: past the merge the service may not have answered.

The Deposit cash business process provides the Deposit cash service. The diagram below shows its flow. The numbered steps after it describe the same flow in words, with each choice, loop and parallel flow holding its own steps beneath it.

Figure 62. The business process Deposit cash.

Step by step:

Request the Credit account service from Ledger.

This step addresses Account is open and Balance increased.

The request is populated as follows:
- accountNumber: providerRequest.accountNumber = request.accountNumber
- amount: providerRequest.amount = request.amount
  
  The answer is kept as credited, one Bank::Ledger::Response.
- If the service is provided:
  1. Populate the response.
    
    This step addresses New balance reported.
    
    newBalance: response.newBalance = credited.newBalance

6.1.2. Service: Withdraw cash

Ledger provides the Withdraw cash service.

The holder takes cash out of their account.

Service requirements

The functional requirements diagram below shows who has an interest in the Withdraw cash service, i.e. its stakeholders, and what each requires of it. A pre-condition is a condition which must hold for the service to be provided at all. When one does not, the request is refused with an exception. A post-condition is what must be true once the service has been provided, i.e. what it must have achieved.

Figure 63. Functional requirements of the Withdraw cash service.

Its stakeholders, and what each requires of it, are:

Bank: The bank: its shared vocabulary and the departments that answer for its services.

Bank requires the pre-conditions Account is open, Requested by the holder and Sufficient funds and the post-condition Balance reduced.
Customer: A customer of the bank, to whom the bank’s services are offered.

Customer requires the pre-condition Requested by the holder and the post-conditions Balance reduced and New balance reported.

It is provided only when:

Account is open: Only an open account is withdrawn from.

Required by Bank. Formally: let a = getAccount(Tuple{accountNumber = request.accountNumber}) in a <> null and a.status = AccountStatus::open
Requested by the holder: Only the account’s holder may take money out of it.

Required by Bank and Customer. Formally: let a = getAccount(Tuple{accountNumber = request.accountNumber}) in a <> null and (let c = findCustomerByLogin(Tuple{login = caller}) in c <> null and a.holder = c.customerNumber)
Sufficient funds: The account holds at least the amount.

Required by Bank. Formally: let a = getAccount(Tuple{accountNumber = request.accountNumber}) in a <> null and a.balance >= request.amount

Once it has been provided:

Balance reduced: The balance went down by exactly the amount.

Required by Bank and Customer. Formally: Account.allInstances()->select(a | a.accountNumber = request.accountNumber)->forAll(a | a.balance = a.balance@pre - request.amount)
New balance reported: The response states the balance after the withdrawal.

Required by Customer. Formally: Account.allInstances()->select(a | a.accountNumber = request.accountNumber)->forAll(a | response.newBalance = a.balance)

Exceptions

When a pre-condition does not hold, the Withdraw cash service is not provided. Instead, it raises the exception belonging to that pre-condition, which the requester may handle. These are the ways in which the service can fail:

Account is open not met, raised when Account is open does not hold: Raised when 'Withdraw cash' is requested while 'Account is open' does not hold.
Requested by the holder not met, raised when Requested by the holder does not hold: Raised when 'Withdraw cash' is requested while 'Requested by the holder' does not hold.
Sufficient funds not met, raised when Sufficient funds does not hold: Raised when 'Withdraw cash' is requested while 'Sufficient funds' does not hold.

Request data structure

The information a requester provides when asking for the service is a Bank::Ledger::Request.

What is supplied when requesting 'Withdraw cash'.

Figure 64. The Bank::Ledger::Request data structure, fully expanded.

A Bank::Ledger::Request has:

one accountNumber, an Bank::Identifier: The account withdrawn from.
one amount, a Bank::Money: How much.

The following must always hold for a Bank::Ledger::Request:

Amount is positive: self.amount > 0

Required by Bank.

Response data structure

The information the service returns once provided is a Bank::Ledger::Response.

What 'Withdraw cash' yields once rendered.

Figure 65. The Bank::Ledger::Response data structure, fully expanded.

A Bank::Ledger::Response has:

one newBalance, a Bank::Money: The balance after the withdrawal.

Responsibility allocation

The responsibility allocation diagram below shows how the Withdraw cash process takes care of each requirement of the Withdraw cash service. It shows which of its steps addresses each pre- and post-condition, and which services it uses from other responsibility domains to do so.

Figure 66. Responsibility allocation for the Withdraw cash process.

Requirement by requirement:

Account is open (pre-condition) is addressed by checking it before anything else is done.
Requested by the holder (pre-condition) is addressed by checking it before anything else is done.
Sufficient funds (pre-condition) is addressed by the step Enough in the account?.
Balance reduced (post-condition) is addressed by requesting the Debit account service from Ledger.
New balance reported (post-condition) is addressed by populating the response.

To do so the process uses the following services:

From Accounts:
- Retrieve account: Looks an account up by its number.
From Ledger:
- Debit account: Takes money out of an account and records the entry.

Business process

Looks the account up, then either debits it or refuses for lack of funds.

Alternate flows, and raising an exception. Rather than a check step, the process looks the account up and branches on what it finds: with enough money it debits the account and reports the new balance; otherwise it raises Sufficient funds not met, stating its shortfall from the account it found. Exactly one branch runs. The pre-condition is allocated to the branch as a whole, since the two flows together are what meet it.

The Withdraw cash business process provides the Withdraw cash service. The diagram below shows its flow. The numbered steps after it describe the same flow in words, with each choice, loop and parallel flow holding its own steps beneath it.

Figure 67. The business process Withdraw cash.

Step by step:

Check that Account is open holds. If it does not, stop and raise Account is open not met.

Formally: let a = getAccount(Tuple{accountNumber = request.accountNumber}) in a <> null and a.status = AccountStatus::open
Check that Requested by the holder holds. If it does not, stop and raise Requested by the holder not met.

Formally: let a = getAccount(Tuple{accountNumber = request.accountNumber}) in a <> null and (let c = findCustomerByLogin(Tuple{login = caller}) in c <> null and a.holder = c.customerNumber)
Request the Retrieve account service from Accounts.

The request is populated as follows:
- accountNumber: providerRequest.accountNumber = request.accountNumber
  
  The answer is kept as found, one Bank::Accounts::Response.
- If the service is provided:
  1. Choose one way to continue, the first whose condition holds:
    
    This step addresses Sufficient funds.
    
    If found.account.balance >= request.amount (Funds suffice):
    
    Request the Debit account service from Ledger.
    
    This step addresses Balance reduced.
    
    The request is populated as follows:
    
    accountNumber: providerRequest.accountNumber = request.accountNumber
    
    amount: providerRequest.amount = request.amount
    
    The answer is kept as debited, one Bank::Ledger::Response.
    
    If the service is provided:
    
    Populate the response.
    
    This step addresses New balance reported.
    
    newBalance: response.newBalance = debited.newBalance
    
    Otherwise:
    
    Stop, raising the Sufficient funds not met exception.
    
    shortfall: raised.shortfall = request.amount - found.account.balance

6.1.3. Service: Transfer funds

Ledger provides the Transfer funds service.

The holder of one account pays money into another.

Service requirements

The functional requirements diagram below shows who has an interest in the Transfer funds service, i.e. its stakeholders, and what each requires of it. A pre-condition is a condition which must hold for the service to be provided at all. When one does not, the request is refused with an exception. A post-condition is what must be true once the service has been provided, i.e. what it must have achieved.

Figure 68. Functional requirements of the Transfer funds service.

Its stakeholders, and what each requires of it, are:

Bank: The bank: its shared vocabulary and the departments that answer for its services.

Bank requires the pre-conditions Both accounts are open, Requested by the holder and Sufficient funds and the post-condition Money is conserved.
Customer: A customer of the bank, to whom the bank’s services are offered.

Customer requires the pre-condition Requested by the holder and the post-conditions Funds moved, New balance reported, Payer advised and Payee advised.

It is provided only when:

Both accounts are open: Money moves only between open accounts.

Required by Bank. Formally: (let a = getAccount(Tuple{accountNumber = request.fromAccount}) in a <> null and a.status = AccountStatus::open) and (let a = getAccount(Tuple{accountNumber = request.toAccount}) in a <> null and a.status = AccountStatus::open)
Requested by the holder: Only the paying account’s holder may transfer out of it.

Required by Bank and Customer. Formally: let a = getAccount(Tuple{accountNumber = request.fromAccount}) in a <> null and (let c = findCustomerByLogin(Tuple{login = caller}) in c <> null and a.holder = c.customerNumber)
Sufficient funds: The paying account holds at least the amount.

Required by Bank. Formally: let a = getAccount(Tuple{accountNumber = request.fromAccount}) in a <> null and a.balance >= request.amount

Once it has been provided:

Funds moved: The paying account went down, and the one paid went up, by the amount.

Required by Customer. Formally: Account.allInstances()->select(a | a.accountNumber = request.fromAccount)->forAll(a | a.balance = a.balance@pre - request.amount) and Account.allInstances()->select(a | a.accountNumber = request.toAccount)->forAll(a | a.balance = a.balance@pre + request.amount)
Money is conserved: The bank holds as much money in total as before.

Required by Bank. Formally: Account.allInstances()->collect(a | a.balance)->sum() = Account.allInstances@pre()->collect(a | a.balance)->sum()
New balance reported: The response states the paying account’s new balance.

Required by Customer. Formally: Account.allInstances()->select(a | a.accountNumber = request.fromAccount)->forAll(a | response.newBalance = a.balance)
Payer advised: The paying customer is told of the transfer.

Required by Customer.

While meeting it, the service sends:
- AccountAdvice sent, carrying an Bank::AccountAdvice, to Customer, as a notification which any number of parties may act on
Payee advised: The customer paid is told of the transfer.

Required by Customer.

While meeting it, the service sends:
- AccountAdvice sent, carrying an Bank::AccountAdvice, to Customer, as a notification which any number of parties may act on

Exceptions

When a pre-condition does not hold, the Transfer funds service is not provided. Instead, it raises the exception belonging to that pre-condition, which the requester may handle. These are the ways in which the service can fail:

Both accounts are open not met, raised when Both accounts are open does not hold: Raised when 'Transfer funds' is requested while 'Both accounts are open' does not hold.
Requested by the holder not met, raised when Requested by the holder does not hold: Raised when 'Transfer funds' is requested while 'Requested by the holder' does not hold.
Sufficient funds not met, raised when Sufficient funds does not hold: Raised when 'Transfer funds' is requested while 'Sufficient funds' does not hold.

Request data structure

The information a requester provides when asking for the service is a Bank::Ledger::Request.

What is supplied when requesting 'Transfer funds'.

Figure 69. The Bank::Ledger::Request data structure, fully expanded.

A Bank::Ledger::Request has:

one fromAccount, an Bank::Identifier: The holder’s account, which pays.
one toAccount, an Bank::Identifier: The account paid.
one amount, a Bank::Money: How much.

The following must always hold for a Bank::Ledger::Request:

Amount is positive: self.amount > 0

Required by Bank.
Within the transfer limit: self.amount <= 50000

Required by Bank.
Different accounts: self.fromAccount <> self.toAccount

Required by Bank.

Response data structure

The information the service returns once provided is a Bank::Ledger::Response.

What 'Transfer funds' yields once rendered.

Figure 70. The Bank::Ledger::Response data structure, fully expanded.

A Bank::Ledger::Response has:

one newBalance, a Bank::Money: The paying account’s balance after the transfer.

Responsibility allocation

The responsibility allocation diagram below shows how the Transfer funds process takes care of each requirement of the Transfer funds service. It shows which of its steps addresses each pre- and post-condition, and which services it uses from other responsibility domains to do so.

Figure 71. Responsibility allocation for the Transfer funds process.

Requirement by requirement:

Both accounts are open (pre-condition) is addressed by checking it before anything else is done.
Requested by the holder (pre-condition) is addressed by checking it before anything else is done.
Sufficient funds (pre-condition) is addressed by checking it before anything else is done.
Funds moved (post-condition) is addressed by requesting the Post transfer service from Ledger.
Money is conserved (post-condition) is addressed by requesting the Post transfer service from Ledger.
New balance reported (post-condition) is addressed by populating the response.
Payer advised (post-condition) is addressed by sending Bank::AccountAdvice.
Payee advised (post-condition) is addressed by sending Bank::AccountAdvice.

To do so the process uses the following services:

From Ledger:
- Post transfer: Moves money from one account to another as one indivisible posting.

Business process

Posts the transfer through the ledger as one posting, then advises both parties at once.

The process does not debit one account and credit the other itself: a transfer must happen entirely or not at all, so it is allocated to the ledger's Post transfer, which guarantees that. One step therefore addresses two requirements.

Concurrent flows. The payer and the payee are advised at the same time: neither advice depends on the other, and the response waits for both.

The Transfer funds business process provides the Transfer funds service. The diagram below shows its flow. The numbered steps after it describe the same flow in words, with each choice, loop and parallel flow holding its own steps beneath it.

Figure 72. The business process Transfer funds.

Step by step:

Check that Both accounts are open holds. If it does not, stop and raise Both accounts are open not met.

Formally: (let a = getAccount(Tuple{accountNumber = request.fromAccount}) in a <> null and a.status = AccountStatus::open) and (let a = getAccount(Tuple{accountNumber = request.toAccount}) in a <> null and a.status = AccountStatus::open)
Check that Requested by the holder holds. If it does not, stop and raise Requested by the holder not met.

Formally: let a = getAccount(Tuple{accountNumber = request.fromAccount}) in a <> null and (let c = findCustomerByLogin(Tuple{login = caller}) in c <> null and a.holder = c.customerNumber)
Check that Sufficient funds holds. If it does not, stop and raise Sufficient funds not met.

Formally: let a = getAccount(Tuple{accountNumber = request.fromAccount}) in a <> null and a.balance >= request.amount
Request the Post transfer service from Ledger.

This step addresses Funds moved and Money is conserved.

The request is populated as follows:
- fromAccount: providerRequest.fromAccount = request.fromAccount
- toAccount: providerRequest.toAccount = request.toAccount
- amount: providerRequest.amount = request.amount
  
  The answer is kept as posted, one Bank::Ledger::Response.
- If the service is provided:
  1. Do the following at the same time, and carry on once all of them are done:
    
    Flow 1:
    
    Send an Bank::AccountAdvice to Customer (the one given by request.fromAccount), as a notification which any number of parties may act on.
    
    This step addresses Payer advised.
    
    accountNumber: sent.accountNumber = request.fromAccount
    
    notice: sent.notice = 'Your transfer was made.'
    
    Flow 2:
    
    Send an Bank::AccountAdvice to Customer (the one given by request.toAccount), as a notification which any number of parties may act on.
    
    This step addresses Payee advised.
    
    accountNumber: sent.accountNumber = request.toAccount
    
    notice: sent.notice = 'Money arrived in your account.'
  2. Populate the response.
    
    This step addresses New balance reported.
    
    newBalance: response.newBalance = posted.newBalance

6.1.4. Service: Pay salaries

Ledger provides the Pay salaries service.

An employer pays a batch of salaries from one account.

Each salary is its own posting, made one after another — a for-each over the batch. The batch as a whole is not one posting: the ledger guarantees each transfer, and the pre-conditions rule out every reason one could be refused before the first is made.

Service requirements

The functional requirements diagram below shows who has an interest in the Pay salaries service, i.e. its stakeholders, and what each requires of it. A pre-condition is a condition which must hold for the service to be provided at all. When one does not, the request is refused with an exception. A post-condition is what must be true once the service has been provided, i.e. what it must have achieved.

Figure 73. Functional requirements of the Pay salaries service.

Its stakeholders, and what each requires of it, are:

Bank: The bank: its shared vocabulary and the departments that answer for its services.

Bank requires the pre-conditions Requested by the holder, Payer account is open, Payees are open accounts and Sufficient funds and the post-condition Payer debited by the total.
Customer: A customer of the bank, to whom the bank’s services are offered.

Customer requires the pre-condition Requested by the holder and the post-conditions Payees credited, Payer debited by the total and New balance reported.

It is provided only when:

Requested by the holder: Only the paying account’s holder may pay from it.

Required by Bank and Customer. Formally: let a = getAccount(Tuple{accountNumber = request.fromAccount}) in a <> null and (let c = findCustomerByLogin(Tuple{login = caller}) in c <> null and a.holder = c.customerNumber)
Payer account is open: Salaries are paid only from an open account.

Required by Bank. Formally: let a = getAccount(Tuple{accountNumber = request.fromAccount}) in a <> null and a.status = AccountStatus::open
Payees are open accounts: Every account paid is open.

Required by Bank. Formally: allAccountsOpen(Tuple{accountNumbers = request.payments->collect(p | p.toAccount)}).allOpen
Sufficient funds: The employer’s account holds at least the batch’s total.

Required by Bank. Formally: let a = getAccount(Tuple{accountNumber = request.fromAccount}) in a <> null and a.balance >= request.payments->collect(p | p.amount)->sum()

Once it has been provided:

Payees credited: Every payee’s balance went up by their salary.

Required by Customer. Formally: request.payments->forAll(p | Account.allInstances()->select(a | a.accountNumber = p.toAccount)->forAll(a | a.balance = a.balance@pre + p.amount))
Payer debited by the total: The employer’s balance went down by the batch’s total.

Required by Bank and Customer. Formally: Account.allInstances()->select(a | a.accountNumber = request.fromAccount)->forAll(a | a.balance = a.balance@pre - request.payments->collect(p | p.amount)->sum())
New balance reported: The response states the employer’s balance afterwards.

Required by Customer. Formally: Account.allInstances()->select(a | a.accountNumber = request.fromAccount)->forAll(a | response.newBalance = a.balance)

Exceptions

When a pre-condition does not hold, the Pay salaries service is not provided. Instead, it raises the exception belonging to that pre-condition, which the requester may handle. These are the ways in which the service can fail:

Requested by the holder not met, raised when Requested by the holder does not hold: Raised when 'Pay salaries' is requested while 'Requested by the holder' does not hold.
Payer account is open not met, raised when Payer account is open does not hold: Raised when 'Pay salaries' is requested while 'Payer account is open' does not hold.
Payees are open accounts not met, raised when Payees are open accounts does not hold: Raised when 'Pay salaries' is requested while 'Payees are open accounts' does not hold.
Sufficient funds not met, raised when Sufficient funds does not hold: Raised when 'Pay salaries' is requested while 'Sufficient funds' does not hold.

Request data structure

The information a requester provides when asking for the service is a Bank::Ledger::Request.

What is supplied when requesting 'Pay salaries'.

Figure 74. The Bank::Ledger::Request data structure, fully expanded.

A Bank::Ledger::Request has:

one fromAccount, an Bank::Identifier: The employer’s account, which pays.
one or more payments, each a Bank::Ledger::Payment: Who is paid, and how much.

The following must always hold for a Bank::Ledger::Request:

Each payee once: self.payments->forAll(p | self.payments->select(q | q.toAccount = p.toAccount)->size() = 1)

Required by Customer.
Not paying itself: self.payments->forAll(p | p.toAccount <> self.fromAccount)

Required by Bank.
Amounts within the posting limit: self.payments->forAll(p | p.amount > 0 and p.amount <= 50000)

Required by Bank.

Bank::Ledger::Payment: One payment in a batch: who is paid, and how much.

A Bank::Ledger::Payment has:

one toAccount, an Bank::Identifier: The account paid.
one amount, a Bank::Money: How much.

Response data structure

The information the service returns once provided is a Bank::Ledger::Response.

What 'Pay salaries' yields once rendered.

Figure 75. The Bank::Ledger::Response data structure, fully expanded.

A Bank::Ledger::Response has:

one newBalance, a Bank::Money: The employer’s balance once every salary is paid.

Responsibility allocation

The responsibility allocation diagram below shows how the Pay salaries process takes care of each requirement of the Pay salaries service. It shows which of its steps addresses each pre- and post-condition, and which services it uses from other responsibility domains to do so.

Figure 76. Responsibility allocation for the Pay salaries process.

Requirement by requirement:

Requested by the holder (pre-condition) is addressed by checking it before anything else is done.
Payer account is open (pre-condition) is addressed by checking it before anything else is done.
Payees are open accounts (pre-condition) is addressed by checking it before anything else is done.
Sufficient funds (pre-condition) is addressed by the step Each payment.
Payees credited (post-condition) is addressed by the step Each payment.
Payer debited by the total (post-condition) is addressed by the step Each payment.
New balance reported (post-condition) is addressed by populating the response.

To do so the process uses the following services:

From Ledger:
- Post transfer: Moves money from one account to another as one indivisible posting.
From Accounts:
- Retrieve account: Looks an account up by its number.

Business process

Posts each salary in turn, then reports the employer’s balance.

For-each. The batch is a collection in the request, and each payment is posted by the same step — so the step is written once, inside a loop over request.payments. The loop is sequential: each posting draws on the same paying account.

Only what a loop carries outlives it, and this one carries nothing: the balance it leaves behind is the account's, which only the ledger knows, so it is looked up afterwards rather than folded through the loop.

The Pay salaries business process provides the Pay salaries service. The diagram below shows its flow. The numbered steps after it describe the same flow in words, with each choice, loop and parallel flow holding its own steps beneath it.

Figure 77. The business process Pay salaries.

Step by step:

Check that Requested by the holder holds. If it does not, stop and raise Requested by the holder not met.

Formally: let a = getAccount(Tuple{accountNumber = request.fromAccount}) in a <> null and (let c = findCustomerByLogin(Tuple{login = caller}) in c <> null and a.holder = c.customerNumber)
Check that Payer account is open holds. If it does not, stop and raise Payer account is open not met.

Formally: let a = getAccount(Tuple{accountNumber = request.fromAccount}) in a <> null and a.status = AccountStatus::open
Check that Payees are open accounts holds. If it does not, stop and raise Payees are open accounts not met.

Formally: allAccountsOpen(Tuple{accountNumbers = request.payments->collect(p | p.toAccount)}).allOpen
For each payment in request.payments, one at a time:

This step addresses Payees credited, Payer debited by the total and Sufficient funds.
1. Request the Post transfer service from Ledger.
  
  The request is populated as follows:
  - fromAccount: providerRequest.fromAccount = request.fromAccount
  - toAccount: providerRequest.toAccount = payment.toAccount
  - amount: providerRequest.amount = payment.amount
Request the Retrieve account service from Accounts.

The request is populated as follows:
- accountNumber: providerRequest.accountNumber = request.fromAccount
  
  The answer is kept as found, one Bank::Accounts::Response.
- If the service is provided:
  1. Populate the response.
    
    This step addresses New balance reported.
    
    newBalance: response.newBalance = found.account.balance

6.1.5. Service: Transfer large amount

Ledger provides the Transfer large amount service.

The holder moves more than one posting allows — up to 1000 postings' worth.

Posted in tranches of at most the posting limit, while anything remains to be paid. How many tranches depends on the amount, which is what makes this a while rather than a for-each: there is no collection to walk, only a condition to keep testing.

Each tranche is a posting, and so indivisible; the transfer as a whole is not. That is a real consequence of the posting limit, and the model states it rather than hiding it.

Service requirements

The functional requirements diagram below shows who has an interest in the Transfer large amount service, i.e. its stakeholders, and what each requires of it. A pre-condition is a condition which must hold for the service to be provided at all. When one does not, the request is refused with an exception. A post-condition is what must be true once the service has been provided, i.e. what it must have achieved.

Figure 78. Functional requirements of the Transfer large amount service.

Its stakeholders, and what each requires of it, are:

Bank: The bank: its shared vocabulary and the departments that answer for its services.

Bank requires the pre-conditions Both accounts are open, Requested by the holder and Sufficient funds and the post-condition Money is conserved.
Customer: A customer of the bank, to whom the bank’s services are offered.

Customer requires the pre-condition Requested by the holder and the post-conditions Funds moved and New balance reported.

It is provided only when:

Both accounts are open: Money moves only between open accounts.

Required by Bank. Formally: (let a = getAccount(Tuple{accountNumber = request.fromAccount}) in a <> null and a.status = AccountStatus::open) and (let a = getAccount(Tuple{accountNumber = request.toAccount}) in a <> null and a.status = AccountStatus::open)
Requested by the holder: Only the paying account’s holder may transfer out of it.

Required by Bank and Customer. Formally: let a = getAccount(Tuple{accountNumber = request.fromAccount}) in a <> null and (let c = findCustomerByLogin(Tuple{login = caller}) in c <> null and a.holder = c.customerNumber)
Sufficient funds: The paying account holds at least the amount.

Required by Bank. Formally: let a = getAccount(Tuple{accountNumber = request.fromAccount}) in a <> null and a.balance >= request.amount

Once it has been provided:

Funds moved: The paying account went down, and the one paid went up, by the amount.

Required by Customer. Formally: Account.allInstances()->select(a | a.accountNumber = request.fromAccount)->forAll(a | a.balance = a.balance@pre - request.amount) and Account.allInstances()->select(a | a.accountNumber = request.toAccount)->forAll(a | a.balance = a.balance@pre + request.amount)
Money is conserved: The bank holds as much money in total as before.

Required by Bank. Formally: Account.allInstances()->collect(a | a.balance)->sum() = Account.allInstances@pre()->collect(a | a.balance)->sum()
New balance reported: The response states the paying account’s new balance.

Required by Customer. Formally: Account.allInstances()->select(a | a.accountNumber = request.fromAccount)->forAll(a | response.newBalance = a.balance)

Exceptions

When a pre-condition does not hold, the Transfer large amount service is not provided. Instead, it raises the exception belonging to that pre-condition, which the requester may handle. These are the ways in which the service can fail:

Both accounts are open not met, raised when Both accounts are open does not hold: Raised when 'Transfer large amount' is requested while 'Both accounts are open' does not hold.
Requested by the holder not met, raised when Requested by the holder does not hold: Raised when 'Transfer large amount' is requested while 'Requested by the holder' does not hold.
Sufficient funds not met, raised when Sufficient funds does not hold: Raised when 'Transfer large amount' is requested while 'Sufficient funds' does not hold.

Request data structure

The information a requester provides when asking for the service is a Bank::Ledger::Request.

What is supplied when requesting 'Transfer large amount'.

Figure 79. The Bank::Ledger::Request data structure, fully expanded.

A Bank::Ledger::Request has:

one fromAccount, an Bank::Identifier: The holder’s account, which pays.
one toAccount, an Bank::Identifier: The account paid.
one amount, a Bank::Money: How much, in all.

The following must always hold for a Bank::Ledger::Request:

Amount is positive: self.amount > 0

Required by Bank.
Within the large-transfer limit: self.amount <= 50000000

Required by Bank.
Different accounts: self.fromAccount <> self.toAccount

Required by Bank.

Response data structure

The information the service returns once provided is a Bank::Ledger::Response.

What 'Transfer large amount' yields once rendered.

Figure 80. The Bank::Ledger::Response data structure, fully expanded.

A Bank::Ledger::Response has:

one newBalance, a Bank::Money: The paying account’s balance after the transfer.

Responsibility allocation

The responsibility allocation diagram below shows how the Transfer large amount process takes care of each requirement of the Transfer large amount service. It shows which of its steps addresses each pre- and post-condition, and which services it uses from other responsibility domains to do so.

Figure 81. Responsibility allocation for the Transfer large amount process.

Requirement by requirement:

Both accounts are open (pre-condition) is addressed by checking it before anything else is done.
Requested by the holder (pre-condition) is addressed by checking it before anything else is done.
Sufficient funds (pre-condition) is addressed by the step Until all is paid.
Funds moved (post-condition) is addressed by the step Until all is paid.
Money is conserved (post-condition) is addressed by the step Until all is paid.
New balance reported (post-condition) is addressed by populating the response.

To do so the process uses the following services:

From Ledger:
- Post transfer: Moves money from one account to another as one indivisible posting.
From Accounts:
- Retrieve account: Looks an account up by its number.

Business process

Posts the amount in tranches of at most the posting limit, while anything remains.

While. The loop carries what remains to be paid: it starts at the whole amount, and each time round a tranche — the posting limit, or what remains if that is less — is posted and taken off. The loop goes round while something remains.

It states an iteration bound of 1000, which is what Within the large-transfer limit guarantees is enough. A loop with no bound is reported, because nothing then says it ends.

The Transfer large amount business process provides the Transfer large amount service. The diagram below shows its flow. The numbered steps after it describe the same flow in words, with each choice, loop and parallel flow holding its own steps beneath it.

Figure 82. The business process Transfer large amount.

Step by step:

Check that Both accounts are open holds. If it does not, stop and raise Both accounts are open not met.

Formally: (let a = getAccount(Tuple{accountNumber = request.fromAccount}) in a <> null and a.status = AccountStatus::open) and (let a = getAccount(Tuple{accountNumber = request.toAccount}) in a <> null and a.status = AccountStatus::open)
Check that Requested by the holder holds. If it does not, stop and raise Requested by the holder not met.

Formally: let a = getAccount(Tuple{accountNumber = request.fromAccount}) in a <> null and (let c = findCustomerByLogin(Tuple{login = caller}) in c <> null and a.holder = c.customerNumber)
While remaining > 0 holds, repeat (at most 1000 times):

This step addresses Funds moved, Money is conserved and Sufficient funds.
- Carried from one pass to the next:
  - remaining, starting as request.amount, then becoming remaining - tranche
    
    Define tranche, one Bank::Money as if remaining > 50000 then 50000 else remaining endif.
    
    Request the Post transfer service from Ledger.
    
    The request is populated as follows:
  - fromAccount: providerRequest.fromAccount = request.fromAccount
  - toAccount: providerRequest.toAccount = request.toAccount
  - amount: providerRequest.amount = tranche
Request the Retrieve account service from Accounts.

The request is populated as follows:
- accountNumber: providerRequest.accountNumber = request.fromAccount
  
  The answer is kept as found, one Bank::Accounts::Response.
- If the service is provided:
  1. Populate the response.
    
    This step addresses New balance reported.
    
    newBalance: response.newBalance = found.account.balance

6.1.6. Service: Credit account

Ledger provides the Credit account service.

Adds money to an account and records the entry.

Service requirements

The functional requirements diagram below shows who has an interest in the Credit account service, i.e. its stakeholders, and what each requires of it. A pre-condition is a condition which must hold for the service to be provided at all. When one does not, the request is refused with an exception. A post-condition is what must be true once the service has been provided, i.e. what it must have achieved.

Figure 83. Functional requirements of the Credit account service.

Its stakeholders, and what each requires of it, are:

Bank: The bank: its shared vocabulary and the departments that answer for its services.

Bank requires the pre-condition Account is open and the post-condition Entry recorded.
Ledger: The only thing that moves money, and the record of every movement.

Ledger requires the post-conditions Balance increased and New balance reported.

It is provided only when:

Account is open: Money is moved only into an open account.

Required by Bank. Formally: let a = getAccount(Tuple{accountNumber = request.accountNumber}) in a <> null and a.status = AccountStatus::open

Once it has been provided:

Balance increased: The balance went up by exactly the amount.

Required by Ledger. Formally: Account.allInstances()->select(a | a.accountNumber = request.accountNumber)->forAll(a | a.balance = a.balance@pre + request.amount)
New balance reported: The response states the balance after the credit.

Required by Ledger. Formally: Account.allInstances()->select(a | a.accountNumber = request.accountNumber)->forAll(a | response.newBalance = a.balance)
Entry recorded: Exactly one ledger entry was added.

Required by Bank. Formally: LedgerEntry.allInstances()->size() = LedgerEntry.allInstances@pre()->size() + 1

Exceptions

When a pre-condition does not hold, the Credit account service is not provided. Instead, it raises the exception belonging to that pre-condition, which the requester may handle. These are the ways in which the service can fail:

Account is open not met, raised when Account is open does not hold: Raised when 'Credit account' is requested while 'Account is open' does not hold.

Request data structure

The information a requester provides when asking for the service is a Bank::Ledger::Request.

What is supplied when requesting 'Credit account'.

Figure 84. The Bank::Ledger::Request data structure, fully expanded.

A Bank::Ledger::Request has:

one accountNumber, an Bank::Identifier: The account to credit.
one amount, a Bank::Money: How much to add.

The following must always hold for a Bank::Ledger::Request:

Amount is positive: self.amount > 0

Required by Ledger.

Response data structure

The information the service returns once provided is a Bank::Ledger::Response.

What 'Credit account' yields once rendered.

Figure 85. The Bank::Ledger::Response data structure, fully expanded.

A Bank::Ledger::Response has:

one newBalance, a Bank::Money: The balance after the credit.

Business process

No business process providing this service has been specified yet.

6.1.7. Service: Debit account

Ledger provides the Debit account service.

Takes money out of an account and records the entry.

Service requirements

The functional requirements diagram below shows who has an interest in the Debit account service, i.e. its stakeholders, and what each requires of it. A pre-condition is a condition which must hold for the service to be provided at all. When one does not, the request is refused with an exception. A post-condition is what must be true once the service has been provided, i.e. what it must have achieved.

Figure 86. Functional requirements of the Debit account service.

Its stakeholders, and what each requires of it, are:

Bank: The bank: its shared vocabulary and the departments that answer for its services.

Bank requires the pre-conditions Account is open and Sufficient funds and the post-condition Entry recorded.
Ledger: The only thing that moves money, and the record of every movement.

Ledger requires the post-conditions Balance reduced and New balance reported.

It is provided only when:

Account is open: Money is moved only out of an open account.

Required by Bank. Formally: let a = getAccount(Tuple{accountNumber = request.accountNumber}) in a <> null and a.status = AccountStatus::open
Sufficient funds: The account holds at least the amount.

Required by Bank. Formally: let a = getAccount(Tuple{accountNumber = request.accountNumber}) in a <> null and a.balance >= request.amount

Once it has been provided:

Balance reduced: The balance went down by exactly the amount.

Required by Ledger. Formally: Account.allInstances()->select(a | a.accountNumber = request.accountNumber)->forAll(a | a.balance = a.balance@pre - request.amount)
New balance reported: The response states the balance after the debit.

Required by Ledger. Formally: Account.allInstances()->select(a | a.accountNumber = request.accountNumber)->forAll(a | response.newBalance = a.balance)
Entry recorded: Exactly one ledger entry was added.

Required by Bank. Formally: LedgerEntry.allInstances()->size() = LedgerEntry.allInstances@pre()->size() + 1

Exceptions

When a pre-condition does not hold, the Debit account service is not provided. Instead, it raises the exception belonging to that pre-condition, which the requester may handle. These are the ways in which the service can fail:

Account is open not met, raised when Account is open does not hold: Raised when 'Debit account' is requested while 'Account is open' does not hold.
Sufficient funds not met, raised when Sufficient funds does not hold: Raised when 'Debit account' is requested while 'Sufficient funds' does not hold.

Request data structure

The information a requester provides when asking for the service is a Bank::Ledger::Request.

What is supplied when requesting 'Debit account'.

Figure 87. The Bank::Ledger::Request data structure, fully expanded.

A Bank::Ledger::Request has:

one accountNumber, an Bank::Identifier: The account to debit.
one amount, a Bank::Money: How much to take.

The following must always hold for a Bank::Ledger::Request:

Amount is positive: self.amount > 0

Required by Ledger.

Response data structure

The information the service returns once provided is a Bank::Ledger::Response.

What 'Debit account' yields once rendered.

Figure 88. The Bank::Ledger::Response data structure, fully expanded.

A Bank::Ledger::Response has:

one newBalance, a Bank::Money: The balance after the debit.

Business process

No business process providing this service has been specified yet.

6.1.8. Service: Reverse transfer

Ledger provides the Reverse transfer service.

Moves a posted transfer’s amount back, as one indivisible posting.

What undoes a Post transfer (its compensation): a transfer that refused partway through a batch leaves earlier postings in place, and a pre-condition exception means the service had no net effect. A reversal can itself fail — the payee may have spent the money — and a failed compensation needs a person to resolve.

Service requirements

The functional requirements diagram below shows who has an interest in the Reverse transfer service, i.e. its stakeholders, and what each requires of it. A pre-condition is a condition which must hold for the service to be provided at all. When one does not, the request is refused with an exception. A post-condition is what must be true once the service has been provided, i.e. what it must have achieved.

Figure 89. Functional requirements of the Reverse transfer service.

Its stakeholders, and what each requires of it, are:

Bank: The bank: its shared vocabulary and the departments that answer for its services.

Bank requires the pre-condition Payee can repay and the post-condition Entries recorded.
Ledger: The only thing that moves money, and the record of every movement.

Ledger requires the post-conditions Payee debited, Payer credited and Payer balance reported.

It is provided only when:

Payee can repay: The account paid still holds the amount.

Required by Bank. Formally: let a = getAccount(Tuple{accountNumber = request.toAccount}) in a <> null and a.balance >= request.amount

Once it has been provided:

Payee debited: The account paid went down by the amount.

Required by Ledger. Formally: Account.allInstances()->select(a | a.accountNumber = request.toAccount)->forAll(a | a.balance = a.balance@pre - request.amount)
Payer credited: The paying account went up by the amount.

Required by Ledger. Formally: Account.allInstances()->select(a | a.accountNumber = request.fromAccount)->forAll(a | a.balance = a.balance@pre + request.amount)
Payer balance reported: The response states the paying account’s new balance.

Required by Ledger. Formally: Account.allInstances()->select(a | a.accountNumber = request.fromAccount)->forAll(a | response.newBalance = a.balance)
Entries recorded: Exactly two ledger entries were added: a debit and a credit.

Required by Bank. Formally: LedgerEntry.allInstances()->size() = LedgerEntry.allInstances@pre()->size() + 2

Exceptions

When a pre-condition does not hold, the Reverse transfer service is not provided. Instead, it raises the exception belonging to that pre-condition, which the requester may handle. These are the ways in which the service can fail:

Payee can repay not met, raised when Payee can repay does not hold: Raised when 'Reverse transfer' is requested while 'Payee can repay' does not hold.

Request data structure

The information a requester provides when asking for the service is a Bank::Ledger::Request.

What is supplied when requesting 'Reverse transfer'.

Figure 90. The Bank::Ledger::Request data structure, fully expanded.

A Bank::Ledger::Request has:

one fromAccount, an Bank::Identifier: The account the transfer paid from, which is paid back.
one toAccount, an Bank::Identifier: The account the transfer paid, which pays it back.
one amount, a Bank::Money: The amount the transfer moved.

Response data structure

The information the service returns once provided is a Bank::Ledger::Response.

What 'Reverse transfer' yields once rendered.

Figure 91. The Bank::Ledger::Response data structure, fully expanded.

A Bank::Ledger::Response has:

one newBalance, a Bank::Money: The original paying account’s balance after the reversal.

Business process

No business process providing this service has been specified yet.

6.1.9. Service: Post transfer

Ledger provides the Post transfer service.

Moves money from one account to another as one indivisible posting.

Why a service of its own rather than a debit followed by a credit: a transfer must happen entirely or not at all. Requested as two services, a failure between them would leave money taken and not delivered. Atomicity is therefore allocated to the ledger, which is the domain able to guarantee it. Undone by Reverse transfer, for a process that refuses after posting.

Service requirements

The functional requirements diagram below shows who has an interest in the Post transfer service, i.e. its stakeholders, and what each requires of it. A pre-condition is a condition which must hold for the service to be provided at all. When one does not, the request is refused with an exception. A post-condition is what must be true once the service has been provided, i.e. what it must have achieved.

Figure 92. Functional requirements of the Post transfer service.

Its stakeholders, and what each requires of it, are:

Bank: The bank: its shared vocabulary and the departments that answer for its services.

Bank requires the pre-conditions Both accounts are open and Sufficient funds and the post-conditions Money is conserved, No other account changed and Entries recorded.
Ledger: The only thing that moves money, and the record of every movement.

Ledger requires the post-conditions Payer debited, Payee credited and Payer balance reported.

It is provided only when:

Both accounts are open: Money moves only between open accounts.

Required by Bank. Formally: (let a = getAccount(Tuple{accountNumber = request.fromAccount}) in a <> null and a.status = AccountStatus::open) and (let a = getAccount(Tuple{accountNumber = request.toAccount}) in a <> null and a.status = AccountStatus::open)
Sufficient funds: The paying account holds at least the amount.

Required by Bank. Formally: let a = getAccount(Tuple{accountNumber = request.fromAccount}) in a <> null and a.balance >= request.amount

Once it has been provided:

Payer debited: The paying account went down by the amount.

Required by Ledger. Formally: Account.allInstances()->select(a | a.accountNumber = request.fromAccount)->forAll(a | a.balance = a.balance@pre - request.amount)
Payee credited: The account paid went up by the amount.

Required by Ledger. Formally: Account.allInstances()->select(a | a.accountNumber = request.toAccount)->forAll(a | a.balance = a.balance@pre + request.amount)
Money is conserved: The bank holds as much money in total as before.

Required by Bank. Formally: Account.allInstances()->collect(a | a.balance)->sum() = Account.allInstances@pre()->collect(a | a.balance)->sum()
No other account changed: Only the two accounts' balances moved.

Required by Bank. Formally: Account.allInstances()->select(a | a.accountNumber <> request.fromAccount and a.accountNumber <> request.toAccount)->forAll(a | a.balance = a.balance@pre)
Payer balance reported: The response states the paying account’s new balance.

Required by Ledger. Formally: Account.allInstances()->select(a | a.accountNumber = request.fromAccount)->forAll(a | response.newBalance = a.balance)
Entries recorded: Exactly two ledger entries were added: a debit and a credit.

Required by Bank. Formally: LedgerEntry.allInstances()->size() = LedgerEntry.allInstances@pre()->size() + 2

Exceptions

When a pre-condition does not hold, the Post transfer service is not provided. Instead, it raises the exception belonging to that pre-condition, which the requester may handle. These are the ways in which the service can fail:

Both accounts are open not met, raised when Both accounts are open does not hold: Raised when 'Post transfer' is requested while 'Both accounts are open' does not hold.
Sufficient funds not met, raised when Sufficient funds does not hold: Raised when 'Post transfer' is requested while 'Sufficient funds' does not hold.

Request data structure

The information a requester provides when asking for the service is a Bank::Ledger::Request.

What is supplied when requesting 'Post transfer'.

Figure 93. The Bank::Ledger::Request data structure, fully expanded.

A Bank::Ledger::Request has:

one fromAccount, an Bank::Identifier: The account paying.
one toAccount, an Bank::Identifier: The account paid.
one amount, a Bank::Money: How much to move.

The following must always hold for a Bank::Ledger::Request:

Different accounts: self.fromAccount <> self.toAccount

Required by Ledger.
Amount is positive: self.amount > 0

Required by Ledger.
Within the posting limit: self.amount <= 50000

Required by Bank.

Response data structure

The information the service returns once provided is a Bank::Ledger::Response.

What 'Post transfer' yields once rendered.

Figure 94. The Bank::Ledger::Response data structure, fully expanded.

A Bank::Ledger::Response has:

one newBalance, a Bank::Money: The paying account’s balance after the transfer.

Business process

No business process providing this service has been specified yet.

6.2. Entities

An entity is information which Ledger keeps over time. It is a record which outlives any one request, and which its services create, change and read. Ledger maintains the following entities:

LedgerEntry: One movement of money into or out of one account.

The entity map below shows each entity together with its facets, i.e. the data structures whose fields make up what it stores.

Figure 95. The entities maintained by Ledger.

6.2.1. Entity: LedgerEntry

One movement of money into or out of one account.

The ledger's audit trail. Every change to a balance leaves exactly one entry per account it touched.

How it is populated

LedgerEntry is populated as follows:

The LedgerEntryRecord data structure describes part of what it holds: The ledger’s record of one entry.

Entity structure

The diagram below shows the LedgerEntry entity fully expanded, i.e. everything it holds, gathered from all of its facets, and the information it is related to. The same structure is described in words after it.

Figure 96. The LedgerEntry entity, fully expanded.

A LedgerEntry has:

one entryNumber, an Bank::Identifier, which identifies it: The entry’s number.
one accountNumber, an Bank::Identifier: The account it moved money in or out of.
one amount, a Bank::Money: How much moved.
one kind, an Bank::EntryKind: Credit or debit.

One of credit and debit.

Data dictionary

This section lists what LedgerEntry stores, attribute by attribute. An attribute gathers every field of that name in the entity’s facets. Where it gathers more than one, each is listed, since fields of one name are stored as one attribute whatever each was meant to hold. The services listed write or read it as their specifications say.

Attribute Type Role Multiplicity Unique Personal data Merged from Written by Read by

Attribute	Type	Role	Multiplicity	Unique	Personal data	Merged from	Written by	Read by
`entryNumber`	Bank::Identifier	identifies	`1`	yes	—	—	—	—
`accountNumber`	Bank::Identifier	states	`1`	no	—	—	—	—
`amount`	Bank::Money	states	`1`	no	—	—	—	—
`kind`	Bank::EntryKind	states	`1`	no	—	—	—	—

entryNumber

Bank::Identifier

identifies

1

yes

—

accountNumber

Bank::Identifier

states

1

—

amount

Bank::Money

states

1

—

kind

Bank::EntryKind

states

1

—

6.3. Dependencies

To provide its services, Ledger relies on services provided by other responsibility domains. The dependency diagram below shows which.

Figure 97. The responsibility domains Ledger depends on.

Ledger uses:

from Accounts: The bank’s accounts: opening, looking up and closing them.
- the Retrieve account service: Looks an account up by its number.