Aims

The aim of this chapter is to show how relationships between data can be modelled as mappings. The mapping type constructor and operators in VDMSL are introduced through an example from the nuclear industry. On completing this chapter, the reader should be confident in modelling and analysing systems involving mappings.

Introduction

Computing systems frequently centre on relationships between sets of values. For example, a database might link a set of customer identifiers to detailed information. Such relationships can often be modelled as mappings from elements of one set, known as the domain, to elements of the other set, known as the range. Mappings can be thought of as tables in which one can look up the domain element and read across to see the range element to which it is related. We will say that each domain element maps to the corresponding range element. Each line of the table, being a small part of the mapping, is called a maplet. Each domain element can have only one maplet in a mapping, so there is no ambiguity about which range element it points to. For example, the following table represents a mapping from names (strings of characters) to bank balances (integers).