A model written in VDM-SL is a collection of the following:

• modular structuring mechanisms;

• data type definitions;

• function definitions;

• operation definitions;

• value (constant) definitions; and

• a state definition.

Each collection of definitions is prefixed by a keyword (e.g. types). Individual definitions are separated by semicolons. Such definitions may be structured inside modules.

This appendix provides an overview of the constructs in the subset of VDM-SL treated in this book. Finally there is a BNF grammar for the subset of VDM-SL covered in this book.

Identifiers

The different kinds of definitions which can be made in VDM-SL are named using identifiers. The naming conventions used in this book are as follows:

• Functions, operations and types begin with an upper-case letter for each word or abbreviation of which the name is composed.

• Constant values begin with lower-case characters and use underscores between words or abbreviations of which these are composed.

• Local identifiers are always sequences of lower-case characters and usually rather short names are used.

However, this is only a convention and is not mandatory.

Type definitions

As in traditional programming languages it is possible to define data types in VDM-SL and give them appropriate names. For example,

Amount = nat

Hereby we have defined a data type with the name “Amount” and stated that the values which belong to this type are natural numbers (nat is one of the basic types described below). One general point about the type system of VDM-SL which is worth mentioning at this point is that equality and inequality can be used between any values.

Aims

An important aspect of the analysis of a model is gaining confidence that the model is an accurate reflection of the informally stated requirements. This chapter aims to provide an awareness of the techniques through which such confidence can be gained. The idea of model validation is introduced: checks for internal consistency are discussed; techniques of visualisation, integration with legacy code, testing and proof are illustrated. On completion of this chapter, the reader should be equipped to choose appropriate validation techniques for a given modelling task.

Introduction

In previous chapters we have introduced a number of different models in VDM-SL. In several cases (e.g. the alarm example in Chapter 2) we started from an informal collection of requirements and built up a model in stages. But just how confident can one be that the formal model really describes the system the customer wanted? This problem arises continually in industry. When the imprecision of the customer requirement is replaced by the precision of a model, how can the modeller be sure that those areas of incompleteness and ambiguity in the original requirement have been resolved in a way that satisfies the customer? There is a further complication: requirement documents often state the client's intentions incorrectly. Such errors can only be resolved by somehow presenting a model of the system to the client in order to obtain feedback which may lead to modifying the model.

Foundations of mathematics is the study of the most basic concepts and logical structure of mathematics, with an eye to the unity of human knowledge. Among the most basic mathematical concepts are: number, shape, set, function, algorithm, mathematical axiom, mathematical definition, and mathematical proof. Typical questions in foundations of mathematics include: What is a number? What is a shape? What is a set? What is a function? What is an algorithm? What is a mathematical axiom? What is a mathematical definition? What is a mathematical proof? What are the most basic concepts of mathematics? What is the logical structure of mathematics? What are the appropriate axioms for numbers? What are the appropriate axioms for shapes? What are the appropriate axioms for sets? What are the appropriate axioms for functions?

Obviously, foundations of mathematics is a subject of the greatest mathematical and philosophical importance. Beyond this, foundations of mathematics is a rich subject with a long history, going back to Aristotle and Euclid and continuing in the hands of outstanding modern figures such as Descartes, Cauchy, Weierstraβ, Dedekind, Peano, Frege, Russell, Cantor, Hilbert, Brouwer, Weyl, von Neumann, Skolem, Tarski, Heyting, and Gödel. An excellent reference for the modern era in foundations of mathematics is van Heijenoort [272].

In the late 19th and early 20th centuries, virtually all leading mathematicians were intensely interested in foundations of mathematics and spoke and wrote extensively on this subject. Today that is no longer the case. Regrettably, foundations of mathematics is now out of fashion.