Understanding Formal Methods

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.