Proof in VDM: A Practitioner's Guide

ISBN-13: 9783540198130 / Angielski / Miękka / 1993 / 362 str.

Juan C. Bicarregui; John S. Fitzgerald; Peter A. Lindsay

Opis

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.

Spis treści

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.- 2.1 Introduction.- 2.2 Basic axiomatisation.- 2.3 Derived rules; reasoning by cases; reasoning using contradiction.- 2.4 Using definitions: conjunction.- 2.5 Implication; definedness; further defined constructs.- 2.6 Summary.- 2.7 Exercises.- 3 Predicate LPF with Equality.- 3.1 Predicates.- 3.2 Types in predicates.- 3.3 Predicate calculus for LPF: proof strategies for quantifiers.- 3.4 Reasoning about equality: substitution and chains of equality.- 3.5 Extensions to typed predicate LPF with equality.- 3.6 Summary.- 3.7 Exercises.- 4 Basic Type Constructors.- 4.1 Introduction.- 4.2 Union types.- 4.3 Cartesian product types.- 4.4 Optional types.- 4.5 Subtypes.- 4.6 A note on composite types.- 4.7 Summary.- 4.8 Exercises.- 5 Numbers.- 5.1 Introduction.- 5.2 Axiomatising the natural numbers.- 5.3 Axiomatisation of addition and proof by induction.- 5.4 More on proof by induction.- 5.5 Using direct definitions.- 5.6 Summary.- 5.7 Exercises.- 6 Finite Sets.- 6.1 Introduction.- 6.2 Generators for sets; set membership; set induction.- 6.3 Proof using set induction.- 6.4 Quantification over sets.- 6.5 Subsets; set equality; cardinality.- 6.6 Other set constructors.- 6.7 Set comprehension.- 6.8 Reasoning about set comprehension.- 6.9 Summary.- 6.10 Exercises.- 7 Finite Maps.- 7.1 Introduction.- 7.2 Basic axiomatisation.- 7.3 Axiomatisation using generators.- 7.4 Extraction and abstraction of lemmas.- 7.5 Using subsidiary definitions.- 7.6 Polymorphic subtypes and associated induction rules.- 7.7 Map comprehension.- 7.8 Summary.- 7.9 Exercises.- 8 Finite Sequences.- 8.1 Introduction.- 8.2 Basic axiomatisation.- 8.3 Destructors.- 8.4 Equality between lists.- 8.5 Operators on lists.- 8.6 An alternative generator set.- 8.7 Summary.- 8.8 Exercises.- 9 Booleans.- 9.1 Introduction.- 9.2 Basic axiomatisation.- 9.3 Formation rules for boolean-valued operators.- 9.4 An example of a well-formedness proof obligation.- 9.5 Summary.- 9.6 Exercises.- II Proof in Practice.- 10 Proofs From Specifications.- 10.1 Introduction.- 10.2 Type definitions.- 10.3 The state.- 10.4 Functions and values.- 10.5 Operations.- 10.6 Validation proofs.- 10.7 Summary.- 10.8 Exercises.- 11 Verifying Reifications.- 11.1 Introduction.- 11.2 Data reification.- 11.3 Operation modelling.- 11.4 An example reification proof.- 11.5 Implementing functions.- 11.6 Implementation bias and unreachable states.- 11.7 Summary.- 11.8 Exercises.- 12 A Case Study in Air-Traffic Control.- 12.1 Introduction.- 12.2 The air-traffic control system.- 12.3 Formalisation of the state model.- 12.4 Top-level operations.- 12.5 First refinement step.- 12.6 Second refinement step.- 12.7 Concluding remarks.- 13 Advanced Topics.- 13.1 Introduction.- 13.2 Functions as a data type.- 13.3 Comparing elements of disjoint types.- 13.4 Recursive type definitions.- 13.5 Enumerated sets, maps and sequences.- 13.6 Patterns.- 13.7 Other expressions.- 13.8 Other types.- III Directory of Theorems.- 14 Directory of Theorems.- 14.1 Propositonal LPF.- 14.2 Predicate LPF with equality.- 14.3 Basic type constructors.- 14.4 Natural numbers.- 14.5 Finite sets.- 14.6 Finite maps.- 14.7 Finite sequences.- 14.8 Booleans.- 14.9 Specifications.- 14.10 Reifications.- 14.11 Case study I: abstract specification.- 14.12 Case study II: refinement.- Index of Symbols.- Index of Rules.