Formal Software Development: From VDM to Java

Formal Software Development: From VDM to Java

Contents
Preface xi
1 High Integrity Software Development 1
1.1 Introduction 1
1.2 High Integrity Software 1
1.3 The Importance of the Specification 3
1.4 Formal Methods 6
1.5 Classifying Formal Methods 7
1.6 Lightweight Formal Methods 8
2 Propositional and Predicate Logic 11
2.1 Introduction 11
2.2 Propositions 11
2.3 Predicate Logic 20
3 An Introduction to Specification in VDM-SL 25
3.1 Introduction 25
3.2 The Case Study: Requirements Analysis 25
3.3 The UML Specification 26
3.4 Specifying the State 26
3.5 Specifying the Operations 27
3.6 Declaring Constants 31
3.7 Specifying Functions 31
3.8 Specifying a State Invariant 33
3.9 Specifying an Initialization Function 34
3.10 User-defined Types 34
3.11 The nil Value 35
3.12 Improving the Incubator System 35
3.13 Specifying the State of the IncubatorController System 37
3.14 Specifying the Operations of the IncubatorController System 38
3.15 A Standard Template for VDM-SL Specifications 41
3.16 Including Comments 41
3.17 The Complete Specification of the IncubatorController System 41
4 From VDM Specifications to Java Implementations 45
4.1 Introduction 45
4.2 Java 45
4.3 From VDM-SL Types to Java Types 47
4.4 Implementing the IncubatorMonitor Specification 47
vii
4.5 Testing the Java Class 58
4.6 Implementing the IncubatorController Specification 63
5 Sets 75
5.1 Introduction 75
5.2 Sets for System Modelling 75
5.3 Declaring Sets in VDM-SL 75
5.4 Defining Sets in VDM-SL 76
5.5 Set Operations 78
5.6 The Patient Register 81
5.7 Modelling the PatientRegister Class in VDM-SL 82
5.8 The Airport Class 86
6 Implementing Sets 93
6.1 Introduction 93
6.2 The Collection Classes of Java 93
6.3 Using a Vector to Implement a Set 95
6.4 Implementing the PatientRegister Specification 101
6.5 Implementing the Airport Specification 106
7 Sequences 111
7.1 Introduction 111
7.2 Notation 111
7.3 Sequence Operators 112
7.4 Defining a Sequence by Comprehension 113
7.5 Using the Sequence Type in VDM-SL 114
7.6 Specifying a Stack 114
7.7 Specifying the State of the Stack 115
7.8 Specifying the Operations on the Stack 116
7.9 Rethinking our Airport System 116
7.10 Some Useful Functions to Use with Sequences 121
8 Implementing Sequences 125
8.1 Introduction 125
8.2 The VDMSequence Class 125
8.3 Implementing the Enhanced Airport Specification 129
8.4 Analysis of the Airport2 Class 131
9 Composite Objects 135
9.1 Defining Composite Object Types 135
9.2 Composite Object operators 136
9.3 A Specification of a Disk Scanner 138
9.4 A Process Management System 141
10 Implementing Composite Objects 151
10.1 Introduction 151
10.2 Implementing the Time Type 151
10.3 Implementing the DiskScanner Specification 155
viii Contents
10.4 Implementing the ProcessManagement System 160
10.5 The Data Model 161
10.6 The Functions 167
10.7 The Operations 171
11 Maps 175
11.1 Introduction 175
11.2 Notation 175
11.3 Map Operators 176
11.4 Map Application 177
11.5 Using the Map Type in VDM-SL 177
11.6 Specifying a High-Security Building 177
11.7 A Robot Monitoring System 181
11.8 The Complete Specification of the Robot Monitoring Software 184
12 Implementing Maps 189
12.1 Introduction 189
12.2 The Hashtable Class 189
12.3 The VDMMap Class 190
12.4 Implementing the RobotMonitor Software 193
12.5 Analysis of the RobotMonitor Class 199
13 Case Study Part 1: Specification 205
13.1 Introduction 205
13.2 The Requirements Definition 205
13.3 The Informal Specification 205
13.4 The Formal Specification 207
14 Case Study Part 2: Implementation 221
14.1 Introduction 221
14.2 Developing the AccountSys Class 221
14.3 Using the AccountSys Class in an Application 230
Index 237
Contents ix