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.