Format:
Online-Ressource (XVI, 276p)
,
online resource
Edition:
Springer eBook Collection. Computer Science
ISBN:
9781447100430
Content:
This volume provides a comprehensive introduction to the field of formal methods for students and practitioners. It strikes a careful balance between rigorous exposition of the underlying mathematics and concrete examples of implementations using real-life tools, thus making it easy to grasp the underlying concepts and theories. It does not aim to provide guidelines for using a particular method, or comparisons of different approaches, but rather a conceptual framework that the reader can use to master any given method. It therefore makes an invaluable practical companion to introductory texts on logic and to books dedicated to a particular formal method. Understanding Formal Methods will be of interest to advanced students and engineers who need to learn the basics of this topic, and also professionals who need to broaden their knowledge or bring themselves up-to-date with the latest techniques
Note:
1. Motivation1.1 Some Industrial Applications -- 1.2 What Is a Formal Method? -- 1.3 From Software Engineering to Formal Methods -- 1.4 On Weaknesses of Formal Methods -- 1.5 A Survey of Formal Methods -- 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.4 Program Development -- 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.2 Antecedents -- 3.3 The Different Branches of Logic -- 3.4 Mathematical Reminders -- 3.5 Well-founded Relations and Ordinals -- 3.6 Fixed Points -- 3.7 More About Computability -- 3.8 Notes and Suggestions for Further Reading -- 4. Hoare Logic -- 4.1 Introducing Assertions in Programs -- 4.2 Verification Using Hoare Logic -- 4.3 Program Calculus -- 4.4 Scope of These Techniques -- 4.5 Notes and Suggestions for Further Reading -- 5. Classical Logic -- 5.1 Propositional Logic -- 5.2 First-order Predicate Logic -- 5.3 Significant Examples -- 5.4 On Total Functions, Many-sorted Logics -- 5.5 Second-order and Higher-order Logics -- 5.6 Model Theory -- 5.7 Notes and Suggestions for Further Reading -- 6. Set-theoretic Specifications -- 6.1 The Z Notation -- 6.2 VDM -- 6.3 The B Method -- 6.4 Notes and Suggestions for Further Reading -- 7. Set Theory -- 7.1 Typical Features -- 7.2 Zermelo¡ªFraenkel Axiomatic System -- 7.3 Induction -- 7.4 Sets, Abstract Data Types and Polymorphism -- 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.2 Transition Systems -- 8.3 CCS, a Calculus of Communicating Systems -- 8.4 The Synchronous Approach on Reactive Systems -- 8.5 Temporal Logic -- 8.6 TLA -- 8.7 Verification Tools -- 8.8 Notes and Suggestions for Further Reading -- 9. Deduction Systems -- 9.1 Hilbert Systems -- 9.2 Natural Deduction -- 9.3 The Sequent Calculus -- 9.4 Applications to Automated Theorem Proving -- 9.5 Beyond First-order Logic -- 9.6 Dijkstra¡ªScholten’s System -- 9.7 A Word About Rewriting Systems -- 9.8 Results on Completeness and Decidability -- 9.9 Notes and Suggestions for Further Reading -- 10. Abstract Data Types and Algebraic Specification -- 10.1 Types -- 10.2 Sets as Types -- 10.3 Abstract Data Types -- 10.4 Semantics -- 10.5 Example of the Table -- 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.2 The Lambda-calculus -- 11.3 Intuitionistic Logic and Simple Typing -- 11.4 Expressive Power of the Simply Typed A-calculus -- 11.5 Second-Order Typing: System F -- 11.6 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.2 More on Type Theory -- 12.3 A Program Correct by Construction -- 12.4 On Undefined Expressions -- 12.5 Other Proof Systems Based on Higher-order Logic -- 12.6 Notes and Suggestions for Further Reading.
Additional Edition:
ISBN 9781852332471
Language:
English
DOI:
10.1007/978-1-4471-0043-0
URL:
Volltext
(lizenzpflichtig)
Bookmarklink
