Browse by author
Lookup NU author(s): Professor John Fitzgerald
Full text is not currently available for this publication.
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.
Author(s): Fitzgerald JS, Moore R
Publication type: Report
Publication status: Published
Series Title: Department of Computing Science Technical Report Series
Year: 1993
Pages: 15
Print publication date: 01/01/1993
Source Publication Date: 1993
Report Number: 424
Institution: Department of Computing Science, University of Newcastle upon Tyne
Place Published: Newcastle upon Tyne
