Program Specification and Verification in VDM

Abstract

Formal methods employ mathematical notation in writing specifications and use mathematical reasoning in justifying designs with respect to such specifications. One avenue of formal methods research is known as the Vienna Development Method. VDM has been used on programming language and non-language applications. In this paper, programming languages and their compilers are ignored; the focus is on the specification and verification of programs. VDM emphasizes the model-oriented approach to the specification of data. The reifi-cation of abstract objects to representations gives rise to proof obligations; one such set which has wide applicability assumes an increase in implementation bias during the design process. The incompleteness of this approach and an alternative set of rules are discussed. The decision to show the input/output relation by post-conditions of two states is also a feature of VDM. In early publications, the proof obligations which support decomposition were poorly worked out; those presented below are as convenient to use as the original "Hoare-logic". Recent work on a logic (which is tailored to partial functions) is also described .