Toggle Main Menu Toggle Search

Open Access padlockePrints

Experiences in Developing a Proof Theory for VDM Specifications

Lookup NU author(s): Professor John Fitzgerald

Downloads

Full text is not currently available for this publication.


Abstract

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.


Publication metadata

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


Share