ePrints

The Typed Logic of Partial Functions and the Vienna Development Method

Lookup NU author(s): Professor John Fitzgerald

Downloads

• Published version [.pdf]

Abstract

Decisions about the logic underpinning a formal specification language have important consequences for the utility of the formalism. This paper describes the major features of the typed Logic of Partial Functions~(LPF) as it has been implemented in support of the Vienna Development Method's Specification Language, VDM-SL. It compares attempts to realise the logic in different environments: a user-centred proof support tool, a specification interpreter and an automated proof tool. Future directions in integrated proof support for the language are suggested.

Publication metadata

Author(s): Fitzgerald JS

Publication type: Report

Publication status: Published

Series Title: School of Computing Science Technical Report Series

Year: 2006

Pages: 33

Print publication date: 01/10/2006

Source Publication Date: October 2006

Report Number: 984

Institution: School of Computing Science, University of Newcastle upon Tyne

Place Published: Newcastle upon Tyne

URL: http://www.cs.ncl.ac.uk/publications/trs/papers/984.pdf

Share