:santagrin: This book was suggested by jpbowen

Book excerpts:

Formal methods are becoming more accepted in both academia and industry as one possible way in which to help improve the quality of both software and hardware systems. It should be remembered however that they are not a panacea, but rather one more weapon in the armoury against making design mistakes. Thus one should not expect too much from formal methods, but rather use them to advantage where appropriate.

This book presents an even more pragmatic view of the use of formal methods than that held by some academics: that is that formal specification alone can still be beneficial (and is much more cost effective in general) than attempting proofs in many cases. While the cost of proving a system correct may be justified in safety-critical systems where lives are at risk, many systems are less critical, but could still benefit from formalization earlier on in the design process than is normally the case in much industrial practice.

This book presents the use of one notation in the accumulation of available mathematical techniques to help ensure the correctness of computer-based systems, namely the Z notation (pronounced 'zed'), intended for the specification of such systems. The formal notation Z is based on set theory and predicate calculus, and has been developed at the Oxford University Computing Laboratory since the late 1970?s.

The use of a formal notation early on in the design process helps to remove many errors that would not otherwise be discovered until a later stage. The book includes specification of a number of digital systems in a variety of areas to help demonstrate the scope of the notation. Most of the specifications are of real systems that have been built, either commercially or experimentally. It is hoped that the variety of examples in this book will encourage more developers to attempt to specify their systems in a more formal manner before they attempt the development or programming stage.

It is hoped that the specifications presented here will help students and industrial practitioners alike to produce better specifications of their designs, be they large or small. Even if no proofs or refinement of a system are attempted, mere formalization early on in the design process will help to clarify a designer?s thoughts (especially when undertaken as part of a team) and remove many errors before they become implemented, and therefore much more difficult and expensive to rectify.