Program Specification and Verification in VDM

  • Jones C
N/ACitations
Citations of this article
14Readers
Mendeley users who have this article in their library.
Get full text

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 .

Cite

CITATION STYLE

APA

Jones, C. B. (1987). Program Specification and Verification in VDM. In Logic of Programming and Calculi of Discrete Design (pp. 149–184). Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-642-87374-4_7

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free