Proof in VDM: A Practitioners' Guide

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