Aims

The aim of this chapter is to show how unordered collections of values can be modelled as sets. The set type constructor and set operators in VDMSL are introduced via an example of a safety-related system. On completion of this chapter, the reader should be confident in the use of sets and the associated operators in models of systems involving collections of values.

Introduction

This is the first of three chapters that describe ways of modelling collections of data values. The three collection types covered (sets, sequences and mappings) describe progressively more structured collections. For each collection type, we will show how collections may be expressed

A formal model of a computing system should be sufficiently abstract to model the system properties of interest, and not so concrete that a great deal of irrelevant detail has to be tackled in order to understand or analyse the model. Modelling languages such as VDM-SL contain a number of features supporting such abstraction. One of the most fundamental is the facility to model sets of values without being concerned about the order in which they are stored.