This is an excellent introduction to formal methods which will bring anyone who needs to know about this important topic up to speed. It is comprehensive, giving the reader all the information needed to explore the field of formal methods in more detail. It offers: a guide to the mathematics required; comprehensive but easy-to-understand introductions to various methods; a run-down of how formal methods can help to develop high-quality systems that come in on time, within budget, and according to requirements.

Table of Contents:
1. Motivation.- 1.1 Some Industrial Applications.- 1.1.1 Specification for Re-engineering.- 1.1.2 Proving Critical Railway Software.- 1.2 What Is a Formal Method?.- 1.3 From Software Engineering to Formal Methods.- 1.3.1 Towards More Rigorous Processes.- 1.3.2 Software Development Using Formal Methods.- 1.3.3 Formal Methods for the Customer.- 1.4 On Weaknesses of Formal Methods.- 1.5 A Survey of Formal Methods.- 1.5.1 Specialized and General Approaches.- 1.5.2 Emphasizing the Specification or the Verification.- 1.6 Aim of this Book.- 1.7 How to Read this Book.- 1.8 Notes and Suggestions for Further Reading.- 2. Introductory Exercise.- 2.1 Exposition.- 2.2 Sketch of a Formal Specification.- 2.3 Is There a Solution?.- 2.3.1 Doing Nothing.- 2.3.2 Attempting the Impossible.- 2.3.3 Weakening the Postcondition.- 2.3.4 Intermezzo: Sum of Sets.- 2.3.5 Strengthening the Precondition.- 2.4 Program Development.- 2.4.1 Prelude: Correctness of a Loop.- 2.4.2 Linear Search.- 2.4.3 Discussion: Reasoning Figures.- 2.4.4 Bounded Linear Search.- 2.4.5 Discussion.- 2.5 Summary.- 2.6 Semantics.- 2.7 Notes and Suggestions for Further Reading.- 3. A Presentation of Logical Tools.- 3.1 Some Applications of Logic.- 3.1.1 Programming.- 3.1.2 Sums and Unions.- 3.1.3 Chasing Paradoxes Away.- 3.2 Antecedents.- 3.3 The Different Branches of Logic.- 3.3.1 Model Theory.- 3.3.2 Proof Theory.- 3.3.3 Axiomatic Set Theory and Type Theory.- 3.3.4 Computability Theory.- 3.4 Mathematical Reminders.- 3.4.1 Set Notations.- 3.4.2 Logical Operators.- 3.4.3 Relations and Functions.- 3.4.4 Operations.- 3.4.5 Morphisms.- 3.4.6 Numbers.- 3.4.7 Sequences.- 3.5 Well-founded Relations and Ordinals.- 3.5.1 Loop Variant and Well-founded Relation.- 3.5.2 Examples.- 3.5.3 Well-founded Induction.- 3.5.4 Well Orders and Ordinals.- 3.6 Fixed Points.- 3.7 More About Computability.- 3.7.1 Primitive Recursion.- 3.7.2 Recursion, Decidability.- 3.7.3 Partial Recursion, Semi-Decidability.- 3.7.4 A Few Words on Logical Complexity.- 3.8 Notes and Suggestions for Further Reading.- 4. Hoare Logic.- 4.1 Introducing Assertions in Programs.- 4.2 Verification Using Hoare Logic.- 4.2.1 Rules of Hoare Logic.- 4.2.2 Bounded Linear Search Program.- 4.3 Program Calculus.- 4.3.1 Calculation of a Loop.- 4.3.2 Calculation of an Assignment Statement.- 4.3.3 Weakest Precondition.- 4.4 Scope of These Techniques.- 4.5 Notes and Suggestions for Further Reading.- 5. Classical Logic.- 5.1 Propositional Logic.- 5.1.1 Atomic Propositions.- 5.1.2 Syntax of Propositions.- 5.1.3 Interpretation.- 5.2 First-order Predicate Logic.- 5.2.1 Syntax.- 5.2.2 Example of the Table.- 5.2.3 Interpretation.- 5.3 Significant Examples.- 5.3.1 Equational Languages.- 5.3.2 Peano Arithmetic.- 5.4 On Total Functions, Many-sorted Logics.- 5.5 Second-order and Higher-order Logics.- 5.6 Model Theory.- 5.6.1 Definitions.- 5.6.2 Some Results of Model Theory; Limitations of First-Order Logic.- 5.7 Notes and Suggestions for Further Reading.- 6. Set-theoretic Specifications.- 6.1 The Z Notation.- 6.1.1 Schemas.- 6.1.2 Operations.- 6.1.3 Example.- 6.1.4 Relations and Functions.- 6.1.5 Typing.- 6.1.6 Refinements.- 6.1.7 Usage.- 6.2 VDM.- 6.2.1 Origins.- 6.2.2 Typing.- 6.2.3 Operations.- 6.2.4 Functions.- 6.2.5 Three-valued Logic.- 6.2.6 Usage.- 6.3 The B Method.- 6.3.1 Example.- 6.3.2 Abstract Machines.- 6.3.3 Simple Substitutions and Generalized Substitutions.- 6.3.4 The B Refinement Process.- 6.3.5 Modularity.- 6.4 Notes and Suggestions for Further Reading.- 7. Set Theory.- 7.1 Typical Features.- 7.1.1 An Untyped Theory.- 7.1.2 Functions in Set Theory.- 7.1.3 Set-theoretic Operations.- 7.2 Zermelo¡ªFraenkel Axiomatic System.- 7.2.1 Axioms.- 7.2.2 Reconstruction of Usual Set-theoretic Concepts.- 7.2.3 The Original System of Zermelo.- 7.3 Induction.- 7.3.1 Reconstruction of Arithmetic.- 7.3.2 Other Inductive Definitions.- 7.3.3 The Axiom of Separation.- 7.3.4 Separation of a Fixed Point.- 7.3.5 Ordinals.- 7.4 Sets, Abstract Data Types and Polymorphism.- 7.4.1 Trees, Again.- 7.4.2 Algebraic Approach.- 7.4.3 Polymorphism (or Genericity).- 7.4.4 The Abstract Type of Set Operations.- 7.5 Properties of ZF and ZFC.- 7.6 Summary.- 7.7 Notes and Suggestions for Further Reading.- 8. Behavioral Specifications.- 8.1 Unity.- 8.1.1 Execution of a Unity program.- 8.1.2 The Table Example.- 8.1.3 A Protocol Example.- 8.2 Transition Systems.- 8.2.1 Definitions and Notations.- 8.2.2 Examples.- 8.2.3 Behavior of a Transition System.- 8.2.4 Synchronized Product of Transition Systems.- 8.2.5 Stuttering Transitions.- 8.2.6 Transition Systems for Unity.- 8.3 CCS, a Calculus of Communicating Systems.- 8.4 The Synchronous Approach on Reactive Systems.- 8.5 Temporal Logic.- 8.5.1 Temporal Logic and Regular Logic.- 8.5.2 CTL*.- 8.5.3 CTL.- 8.5.4 LTL and PLTL.- 8.5.5 The Temporal Logic of Unity.- 8.5.6 Hennessy¡ªMilner Modalities.- 8.5.7 Mu-calculus.- 8.6 TLA.- 8.7 Verification Tools.- 8.7.1 Deductive Approach.- 8.7.2 Verification by Model Checking.- 8.8 Notes and Suggestions for Further Reading.- 9. Deduction Systems.- 9.1 Hilbert Systems.- 9.2 Natural Deduction.- 9.2.1 Informal Presentation.- 9.2.2 Formal Rules.- 9.2.3 Toward Classical Logic.- 9.2.4 Natural Deduction Presented by Sequents.- 9.2.5 Natural Deduction in Practice.- 9.3 The Sequent Calculus.- 9.3.1 The Rules of the Sequent Calculus.- 9.3.2 Examples.- 9.3.3 Cut Elimination.- 9.4 Applications to Automated Theorem Proving.- 9.4.1 Sequents and Semantical Tableaux.- 9.4.2 From the Cut Rule to Resolution.- 9.4.3 Proofs in Temporal Logic.- 9.5 Beyond First-order Logic.- 9.6 Dijkstra¡ªScholten’s System.- 9.6.1 An Algebraic Approach.- 9.6.2 Displaying the Calculations.- 9.6.3 The Role of Equivalence.- 9.6.4 Comparison with Other Systems.- 9.6.5 Choosing Between Predicates and Sets.- 9.6.6 Uses of Dijkstra¡ªScholten’s System.- 9.7 A Word About Rewriting Systems.- 9.8 Results on Completeness and Decidability.- 9.8.1 Properties of Logics.- 9.8.2 Properties of Theories.- 9.8.3 Impact of These Results.- 9.9 Notes and Suggestions for Further Reading.- 10. Abstract Data Types and Algebraic Specification.- 10.1 Types.- 10.2 Sets as Types.- 10.2.1 Basic Types.- 10.2.2 A First Glance at Dependent Types.- 10.2.3 Type of a Function.- 10.2.4 Type Checking.- 10.2.5 From Sets to Types.- 10.2.6 Towards Abstract Data Types.- 10.2.7 Coercions.- 10.2.8 A Simpler Approach.- 10.2.9 Unions and Sums.- 10.2.10 Summary.- 10.3 Abstract Data Types.- 10.3.1 Sorts, Signatures.- 10.3.2 Axioms.- 10.3.3 First-order and Beyond.- 10.4 Semantics.- 10.5 Example of the Table.- 10.5.1 Signature of Operations.- 10.5.2 Axioms.- 10.6 Rewriting.- 10.7 Notes and Suggestions for Further Reading.- 11. Type Systems and Constructive Logics.- 11.1 Yet Another Concept of a Type.- 11.1.1 Formulas as Types.- 11.1.2 Interpretation.- 11.2 The Lambda-calculus.- 11.2.1 Syntax.- 11.2.2 The Pure A-calculus and the A-calculus with Constants.- 11.2.3 Function and Function.- 11.2.4 Representing Elementary Functions.- 11.2.5 Functionality of ß-reduction.- 11.3 Intuitionistic Logic and Simple Typing.- 11.3.1 Constructive Logics.- 11.3.2 Intuitionistic Logic.- 11.3.3 The Simply Typed A-calculus.- 11.3.4 Curry¡ªHoward Correspondence.- 11.4 Expressive Power of the Simply Typed A-calculus.- 11.4.1 Typing of the Natural Numbers.- 11.4.2 Typing of Booleans.- 11.4.3 Typing of the Identity Function.- 11.4.4 Typing of Pairs, Product of Types.- 11.4.5 Sum Types.- 11.4.6 Paradoxical and Fixed-point Combinators.- 11.4.7 Summary.- 11.5 Second-Order Typing: System F.- 11.5.1 Typing of Regular Structures.- 11.5.2 Systematic Construction of Types.- 11.5.3 Expressive Power and Consistency of System F.- 11.6 Dependent Types.- 11.6.1 Introduction of First-order Variables.- 11.6.2 Sums and Products.- 11.6.3 Specification Based on Dependent Types.- 11.7 Example: Defining Temporal Logic.- 11.8 Towards Linear Logic.- 11.9 Notes and Suggestions for Further Reading.- 12. Using Type Theory.- 12.1 The Calculus of Inductive Constructions.- 12.1.1 Basic Concepts.- 12.1.2 Inductive Types.- 12.1.3 The Table Example.- 12.2 More on Type Theory.- 12.2.1 System Fw.- 12.2.2 The Calculus of Pure Constructions.- 12.2.3 Inductive Definitions.- 12.2.4 Inductive Dependent Types.- 12.2.5 Primitive Recursive Functions.- 12.2.6 Reasoning by Generalized Induction.- 12.2.7 Induction Over a Dependent Type.- 12.2.8 General Purpose Inductive Types.- 12.3 A Program Correct by Construction.- 12.3.1 Programs and Proofs.- 12.3.2 Example: Searching for an Element in a List.- 12.3.3 Searching in an Interval of Integers.- 12.3.4 Program Extraction.- 12.4 On Undefined Expressions.- 12.5 Other Proof Systems Based on Higher-order Logic.- 12.6 Notes and Suggestions for Further Reading.