Proof in Vdm: A Practitioner's Guide (Formal Approaches to Computing and Information Technology)

Proof in VDM: A Practitioners' Guide is a textbook and manual on the practical aspects of using and constructing proofs in the specification and development of computing systems. Many introductory courses on formal techniques are, by their nature, unable to cover the pragmatics of proof. Practitioners competent in writing and comprehending formal specifications are therefore often at a loss when it comes to conducting the relevant proofs. Proof in VDM: A Practitioners' Guide addresses that need. The reader is guided through the elements of proof construction with the help of numerous worked examples. The techniques can be applied to specification and development in a range of formalisms, and are illustrated using the logic and the basic data types of the VDM specification language. The construction of theorems and proofs from actual specifications and refinements is also described, and a detailed case study, including several refinement steps, shows how formal proof can be used in practice. In addition, the book contains a directory of axioms and formally proved theorems.