
Proof in VDM: A Practitioner's Guide
Springer (Publisher)
Published on 1. December 1993
Book
Paperback/Softback
XVI, 362 pages
978-3-540-19813-0 (ISBN)
Description
Formal specifications were first used in the description of program ming languages because of the central role that languages and their compilers play in causing a machine to perform the computations required by a programmer. In a relatively short time, specification notations have found their place in industry and are used for the description of a wide variety of software and hardware systems. A formal method - like VDM - must offer a mathematically-based specification language. On this language rests the other key element of the formal method: the ability to reason about a specification. Proofs can be empioyed in reasoning about the potential behaviour of a system and in the process of showing that the design satisfies the specification. The existence of a formal specification is a prerequisite for the use of proofs; but this prerequisite is not in itself sufficient. Both proofs and programs are large formal texts. Would-be proofs may therefore contain errors in the same way as code. During the difficult but inevitable process of revising specifications and devel opments, ensuring consistency is a major challenge. It is therefore evident that another requirement - for the successful use of proof techniques in the development of systems from formal descriptions - is the availability of software tools which support the manipu lation of large bodies of formulae and help the user in the design of the proofs themselves.
More details
Series
Edition
Softcover reprint of the original 1st ed. 1994
Language
English
Place of publication
London
United Kingdom
Publishing group
Springer Berlin
Target group
Professional and scholarly
Research
Illustrations
XVI, 362 p.
Dimensions
Height: 235 mm
Width: 155 mm
Thickness: 21 mm
Weight
575 gr
ISBN-13
978-3-540-19813-0 (9783540198130)
DOI
10.1007/978-1-4471-2033-9
Schweitzer Classification
Content
1 Introduction.- 1.1 Background.- 1.2 How proofs arise in practice: an introductory example.- 1.3 A logical framework for proofs.- 1.4 Summary.- I A Logical Basis for Proof in VDM.- 2 Propositional LPF.- 3 Predicate LPF with Equality.- 4 Basic Type Constructors.- 5 Numbers.- 6 Finite Sets.- 7 Finite Maps.- 8 Finite Sequences.- 9 Booleans.- II Proof in Practice.- 10 Proofs From Specifications.- 11 Verifying Reifications.- 12 A Case Study in Air-Traffic Control.- 13 Advanced Topics.- III Directory of Theorems.- 14 Directory of Theorems.- Index of Symbols.- Index of Rules.