Understanding Formal Methods (2003. 290 p. w. 30 figs.)

個数:

Understanding Formal Methods (2003. 290 p. w. 30 figs.)

  • 在庫がございません。海外の書籍取次会社を通じて出版社等からお取り寄せいたします。
    通常6~9週間ほどで発送の見込みですが、商品によってはさらに時間がかかることもございます。
    重要ご説明事項
    1. 納期遅延や、ご入手不能となる場合がございます。
    2. 複数冊ご注文の場合、分割発送となる場合がございます。
    3. 美品のご指定は承りかねます。
  • 【入荷遅延について】
    世界情勢の影響により、海外からお取り寄せとなる洋書・洋古書の入荷が、表示している標準的な納期よりも遅延する場合がございます。
    おそれいりますが、あらかじめご了承くださいますようお願い申し上げます。
  • ◆画像の表紙や帯等は実物とは異なる場合があります。
  • ◆ウェブストアでの洋書販売価格は、弊社店舗等での販売価格とは異なります。
    また、洋書販売価格は、ご注文確定時点での日本円価格となります。
    ご注文確定後に、同じ洋書の販売価格が変動しても、それは反映されません。
  • 製本 Paperback:紙装版/ペーパーバック版/ページ数 290 p.
  • 商品コード 9781852332471

Full Description


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.

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 ss-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.