Programming with VDM

Formal Specijication and Object-Oriented Design The need for software that works In the summer of 1988, an Iranian civilian aircraft was shot down by the USS Vincennes over the Gulf of Persia, killing all of the 290 passengers and crew within. The following winter, in what has been widely represented as a retaliatory gesture, a Pan American Jumbo jet was blown up over Scotland, killing the 270 occupants on board. An enquiry into the original incident has since blamed computer error for the calamity. At the critical point, the software-controlled radar system mistakenly identified the Iranian airbus as an aggressive military target. Thus, two major international incidents involving the loss of many hundreds of innocent lives may eventually be attributed to a programming error.Faulty software may yet have even more calamitous consequences. Numerous false alarms have been set off by the US nuc1ear attack early warning system. Red alerts set off by software errors have on more than one occasion pushed the system to the brink of setting off a nuc1ear response to non-existent attacks.More and more life-critical systems are being built using potentially errorprone software. Already, hospitals are being successfully sued as a result of computer-controlled medication systems, such as radiotherapy, administering fatal doses to their patients. Aeroplanes have often mysteriously ftown offcourse, lost their way and crashed due to a software fault in their navigation systems.Software errors are not always a matter of life and death. They may simply cause firms to go bankrupt as a result of faulty accounting or decision support systems. This, of course, is not a trivial matter for the newly unemployed workers in such unfortunate enterprises.We therefore cannot afford to be complacent about software error. It is a truism that the production of totally fault-free software is as difficult to achieve as leading a totally pure life. The more that software is required to do, the more opportunity it has for going wrong. However, it behoves software professionals to use those tools and techniques that enable them to deliver software that is as near perfect as possible. In this chapter, we will References This text aims to provide a practical programmer's introduction to VDM (Vienna Development Method) - one of the leading methods of formal methods for program development. Adopts an object-oriented approach to software design and includes many examples of target programs written in Modula-2. Although intended for readers with some experience of programming, no prior knowledge of mathematics is assumed: the contents include a chapter on the mathematics required for VDM. The final chapter contains a prototype electronic mail system, specified using VDM, and implemented in Modula-2. Front Matter....Pages i-viii Formal Specification and Object-Oriented Design....Pages 1-10 Mathematical Foundations....Pages 11-20 Functions....Pages 21-30 Operations....Pages 31-41 Composite Objects....Pages 42-52 Further Structured Data Types....Pages 53-66 Specification Using Maps....Pages 67-78 A Simple Case Study....Pages 79-104 Epilogue....Pages 105-106 Back Matter....Pages 107-122