John Fitgerald et al. Validated Designs for Object-oriented Systems. 2004, ISBN-13: 978-1852338817
This book is one of my favorites on formal methods. While many books on formal methods focus on presenting detailed mathematics and formal proofs, this book provides a tutorial on how to model specifications using a formal specification language. The specification language is the Vienna Development Method Specification Language++ (VDM++). VDM++ is a functional programming language with excellent abilities to express types, data modeling, and algorithms. VDM++ adds object orientation to its predecessor VDM-SL. Unlike some formal specification languages, VDM++ is written using normal characters on a computer keyboard (no Greek letters or special mathematical symbols needed). The book begins with a discussion of why formal modeling is useful in software development. It provides an overview on building a simple model. Part II of the book explains the VDM++ language and how to use those features in building models. Part III provides three case studies. Part IV discusses generating code from the specification. This is a book that programmers without advanced degrees in mathematics can enjoy and profit from. While formal specification is not as widely used as some other requirements approaches, it is particularly effective for use with critical or complex software development. If you have never used formal specification, this is the book to start with.