| This book is intended for final-year undergraduate and postgraduate computing students specializing in the field of software engineering. The text concentrates on the challenges that high integrity software development poses, and how formal methods can help meet these challenges.
Formal methods have long been advocated for the development of high integrity software. However, these methods are often perceived as being difficult to learn and apply. In particular, the step from formal specification to code is often left uncovered in text books. Without this, however, it is the authors’ experience that students tend to view such methods as purely academic tasks, divorced from the realities of the software development process. So, as well as providing a thorough introduction to the use of a formal method, we motivate the student by demonstrating the development of programs from formal specifications.
When formal program development is covered in many other text books, it tends to be in the context of proof obligations. We have found that students have greatest difficulty with this area – and in addition it is hard, in a text book, to demonstrate the complete formal development of a working application. In recent years, however, a lightweight approach to formal methods has been put forward. This approach places far less emphasis on the discharge of proof obligations and instead advocates the use of run-time assertions to ensure the integrity of final code. It is the lightweight approach we adopt in this book.
The formal method we have chosen is VDM (the Vienna Development Method). This is one of the most mature and widely used formal methods, with an internationally recognized standard. The implementation language we have chosen is Java – oneof the most common programming languages taught at universities. While we assume no previous knowledge of VDM, we do assume that the reader is familiar with the basics of programming in Java. The UML notation is also used to informally specify classes. Most readers should be familiar with this notation, but a brief overview is provided. |
