Proof in VDM: A Practitioner’s Guide

This title is printed to order. This book may have been self-published. If so, we cannot guarantee the quality of the content. In the main most books will have gone through the editing process however some may not. We therefore suggest that you be aware of this before ordering this book. If in doubt check either the author or publisher’s details as we are unable to accept any returns unless they are faulty. Please contact us if you have any questions.

This manual examines the practical aspects of using and constructing proofs in the specification and development of computing systems. 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 proofs can be used in practice. In addition, the book contains a directory of axioms and formally proved theorems.