J.S. Fitzgerald
R. Moore
University of Newcastle upon Tyne. 1993
This paper records experience in the provision of the necessary theories to support formal reasoning about the contents of specifications written in the VDM Specification Language. The need for an axiomatisation of VDM logic and data types is briefly reviewed and a framework suitable for its expression is introduced. This is illustrated with examples from the predicate Logic of Partial Functions and the theory of finite sets. The main part of the paper discusses problems of choosing the form of the axiomatisation of specification language constructs. Specifically, we address the use of syntactic versus axiomatic definition and direct versus indirect interpretation of language constructs. Aspects of VDM which have been found difficult to describe, or which complicate proofs, are discussed. These include proliferation of typing hypotheses, finiteness of comprehensions, flatness of data types involving functions, and interpretation of loose expressions. Particular stress is laid on the repercussions a choice made during axiomatisation may have on the intuitive clarity of the axioms and the ease of construction of proofs.