20.2.4 Reasoning with pre- and post-conditions 567
20.2.5 Introduction to VDM data types 568
20.2.6 The primitive types 568
20.2.7 The set type 569
20.2.8 Implicit defi nition of sets 570
20.2.9 Creating VDM state models 571
20.2.10 Composites 572
20.3 A Systematic Approach to the Construction of VDM Specifi cations 573
20.3.1 Creation of a system state 573
20.3.2 Construction of data type invariants 574
20.3.3 Modeling of the system’s operations 575
20.3.4 Discharging proof obligations 576
20.3.5 Specifi cation refi nement 579
20.3.6 Formal proof obligations 579
20.3.7 Recapitulation 580
20.4 The Sequence and Map Types 580
20.4.1 The sequence data type 580
20.4.2 The map data ...