VDM-SL Assignment

Question 1.

This question concerns a banking application, to be modelled formally using VDM-SL. Read the following information and answer the questions which follow.

Bank customers have unique identifiers of type CustId. Each customer can have more than one account. Accounts are represented by unique identifiers of type AcctNo. Both types are modelled as character strings:

CustId = seq of char;

AcctNo = seq of char;

Customers are related to accounts using a customer database represented as a mapping type

CustDb = map CustId to AcctInfo;

Information about accounts is recorded using a mapping between AcctNo and Account. The Account is represented as a record type recording the balance and the type of account (Current or Savings):

AcctInfo = map AcctNo to Account;

Account :: balance : real

type : <Current> | <Savings>;

1. Customer identifiers and account numbers are both limited to a maximum of 40 characters. Show how you would specify these constraints in the model. [8 marks]
2. The following datatype invariant has been added to the Customer Database. Give an English language description, for the benefit of a user who is not familiar with VDM, of the constraint that is specified by this invariant.

inv cdb == forall accts in set rng cdb &

not exists ac1, ac2 in set dom accts &

ac1 <> ac2 and

accts(ac1).type = <Current> and

accts(ac2).type = <Current>;

1. The bank wishes to maintain a record of transactions in each account. Transactions are modelled by the type Transaction as follows:

Transaction :: description : seq of char

amount : real;

A positive amount field indicates a deposit of money into the account, a withdrawal is indicated by a negative amount. Each day, a sequence of transactions is recorded with the account.

Show how you would modify the type Account to contain a sequence of today’s transactions.                                               [5 marks]

Question 2.

Given the following VDM-SL expressions, answer the questions below

1. What does function f compute? Provide valid values for input parameters and output result (e.g. f(x,y) = RESULT)

f: nat * seq of nat -> nat

f(x, y) == len [ 0 | i in set inds y & y(i) = x];

1. What does function g compute? Provide valid values for input parameters and output result (e.g. g(a, b) = RESULT)

g: seq of nat * seq of nat -> bool

g(a, b) ==

len a = len b and

(forall i in set inds a &

f(a(i), a) = f(a(i),b));

END