Foundations of computing : system development with set theory and logic

著者

• Scheurer, Thierry

書誌事項

Foundations of computing : system development with set theory and logic

Thierry Scheurer

（International computer science series）

Addison-Wesley, c1994

注記

Includes bibliographical references (p. 647-648) and index

内容説明・目次

内容説明

Set theory and logic are the twin pillars of computing science. Their mastery is an essential part of the software engineer's education. This book provides a clear introduction to the key ideas of these two subjects and shows how they can be applied successfully in formal system development. Highlights of the book include: * A presentation of set theory as a modelling language of universal applicability * A wealth of practical examples demonstrating the remarkable simplicity and naturalness of set theory as a description tool * A description of logic as a formal language, and as a simple way of introducing the key concepts of formal syntax, semantics and deduction calculus * A practical methodology of system development based on set theory and illustrated by several substantial case studies The book starts from first principles and requires no prior knowledge of mathematics. It will be equally valuable for students of computing science and software engineers wishing to develop the skills required to apply formal methods successfully.

目次

• Table of Contents Preface List of Symbols Part 1 Overview Prologue Chapter 1 A View of System Development 1.1 On Systems and Computers 1.1A Computing: a New Perspective 1.1B General Problem Solving 1.1C Radical Novelties 1.1D Computers and General Problem Solving 1.2 Universal Features of Systems 1.2A Structure 1.2B Taxonomy 1.2C Modules: Components and Interfaces 1.2D Notation 1.2E Transformation 1.2F Establishment: Specification and Analysis 1.3 System Development with Set Theory and Logic 1.3A Introduction to Set Theory 1.3B Induction and Recursion 1.3C Formal Notation and Symbolic Logic 1.3D The Practice of Model Establishment Part 2 Set Theory and Induction Chapter 2 Sets and Basic Set Operations 2.1 Basic Definitions 2.1A The Concept of Set 2.1B Defining and Denoting Sets 2.1C Identifiers 2.1D Equivalent Definitions 2.1E On the Caution Required in Defining Sets 2.1F Three Fundamental Features of Sets 2.1G Membership and Inclusion 2.1H Special Sets and Set Cardinality 2.1I Principle of Extensionality 2.1J On the Method of Abstraction Exercises 2.2 Basic Set Operations 2.2A Pair 2.2B Union 2.2C Intersection 2.2D Relative Complement 2.2E Disjointness and Related Operations 2.2F Powerset 2.2G Application Exercises 2.3 Properties of Basic Set Operations 2.3A Commutativity and Associativity 2.3B Distributivity and De Morgan's Laws 2.3C Laws of the Empty Set, Idempotence and Absorption 2.3D Laws of Inclusion 2.3E Properties of Operations on Disjoint Sets Exercises 2.4 Review of Notation 2.4A Example 2.4B Variables, Functions and Predicates 2.4C Logical Connective Symbols 2.4D Quantifiers 2.4E Punctuation 2.4F Introducing Names 2.5 Variants of Set Theory 2.5A Russell's Paradox and Classes 2.5B Set Theory as a Modelling Language 2.5C Naive versus Axiomatic Set Theory Chapter 3 Relations and Functions 3.1 Couples, Cartesian Product and Disjoint Union 3.1A Couples 3.1B Cartesian Product 3.1C Disjoint Union 3.1D Exercises 3.2 Relations 3.2A The Concept of a Relation 3.2B Examples of Relations 3.2 C Some Derived Features of a Relation 3.2D Basic Categories of Relations 3.2E Class Relations AT Exercises 3.3 Functions 3.3A The Concept of a Function 3.3B Examples of Functions 3.3C Basic Categories of Functions Exercises 3.4 Fundamental Applications of Functions AT 3.4A Characteristic Functions of Subsets and Relations 3.4B Equivalence between Relations and Functions 3.4C Families and Bags 3.4D Families of Sets and Partitions 3.4E Distributed Functions Exercises 3.5 n-ary Relations and Functions 3.5A n-tuples 3.5B n-ary Cartesian Product 3.5C n-ary Disjoint Union 3.5D n-ary Relations 3.5E Examples of n-ary Relations 3.5F n-ary Functions 3.5G Examples of n-ary Functions 3.5H Nullary Functions and n-ary Operations 3.5I n-ary Class Relations and Functions AT Exercises 3.6 Operations on Relations and Functions AT 3.6A Operations Returning Sets of Relations 3.6B Composition of Relations and Functions 3.6C Restrictions and Overriding 3.6D Identity and Inclusion Functions 3.6E Opposites and Inverses Exercises Chapter 2.3Induction and Recursion 2.3-1 1 Peanos Postulates for Natural Numbers 3 A Deriving Peanos Postulates 3 B Significance of Peanos Postulates 7 C Inductive Sets with Respect to 0 and S 7 D A Concrete Definition of Natural NumbersAT 9 E Exercises 10 2 Proof by Induction 13 A Proposition P(n)
• Example 13 B Proof by Induction: Theorem and Method 13 C Example of a Proof by Induction 15 D Alternative Application of the Induction Principle 16 E Second Induction Principle 17 F Exercises 17 3 Simple Recursion 19 A Example of a Simply Recursive Function 19 B Simple Recursion Theorem 21 C Variant of the Simple Recursion Theorem 26 D Inductive Constructions 27 E Defining Arithmetic Operations in NatAT 28 F Exercises 30 4 Structural Induction 33 A Example of a Structural Inductive Construction 33 B General Definition of Structural Induction 36 C Parse Trees 38 D Second Example 39 E Construction Sequences 41 F Proof by Structural Induction 42 G Exercises 44 5 Free Inductive Sets
• General Recursion Theorem 46 A Free Inductive Sets 46 B Structural Recursion
• Example 2.3-48 C General Recursion Theorem 51 D Second Variant of the General Recursion TheoremAT 53 E Exercises 54 Part 3 Symbolic Logic Chapter 3.1Introduction to Symbolic Logic 3.1-1 1 Knowledge and Deductive Reasoning 1 A Two Features of Scientific Knowledge 1 B The Nature of Deductive Reasoning 1 2 Logic 4 A Purpose of Logic 4 B Logic versus Symbolic Logic 4 C Propositional Logic versus Predicate Logic 5 D Exercises 6 Chapter 3.2Propositional Logic 3.2-1 1 Syntax of Propositional Logic 2 A Alphabet 2 B Informal Definition of Well-formed Formulas 3 C Formal Definition of Well-formed FormulasAT 4 D Exercises 6 2 Semantics of Propositional Logic 8 A Recursive Definition of the Semantic Function M 8 B Example 10 C Well-definedness of M 12 D Exercises 14 3 Tautological Implication 15 A Truth Tables 15 B Satisfiability 16 C Definition of Tautological Implication 17 D Tautologies 19 E Exercises 20 4 Fundamental Tautologies and Applications 23 A A Catalogue 23 B Substitution 24 C Equivalent Languages 26 D Applications 27 E Exercises 28 Chapter 3.3First-order Predicate Logic 3.3-1 1 Introduction 2 A Limitations of Propositional Logic 2 B Requirements to Be Met by First-order Logic 3 C Exercises 5 2 Syntax of First-order Logic 3.3-6 A Alphabet 6 B Well-formed Expressions 8 C Formal Definition of Well-formed ExpressionsAT 10 D Unique Readability of Wfes 12 E Free and Bound Variables 15 F Exercises 18 3 Semantics of First-order Logic 21 A Interpretation 22 B Semantic Function of Well-formed Expressions 23 C Example 26 D A TheoremAT 29 E Exercises 30 4 Logical Implication 32 A Model and Satisfiability 32 B Definition of Logical Implication 32 C Examples of Valid Formulas 34 D Exercises 35 Chapter 3.4Formal Deduction in First-order Logic 3.4-1 1 Formal Deduction 1 A Outline of a Formal Deduction System 2 B Generation of Formal Theorems 3 C Logical Axioms 4 D Fundamental Properties of FDS 7 E Inductive ConstructionsAT 8 F Exercises 11 2 Fundamental Metatheorems 13 A Subset and Transitivity Properties of |- 14 B Deduction Theorem and Corollaries 16 C Generalization Theorem 19 D Exercises 20 3 Natural Deduction and Further Metatheorems 24 A Proof Format 25 B Substitutivity of Equivalence 30 C Alphabetic Variants 31 D Universal Instantiation and Existential Theorems 36 E Equality 38 F Exercises 40 Chapter 3.5Formal Proofs in Set Theory 3.5-1 1 Axiomatic Set Theory (AST) 2 A Language of AST 2 B Interpretation of AST 3 C Seven Axioms of AST 4 D Defining Predicates and Functions 6 E Exercises 9 2 Some Formal Proofs in AST 11 A Three Simple Proofs 11 B Uniqueness of the Empty Set 13 C Union of Two Sets 3.5- 17 D Exercises 21 Part 4 Feature Notation, Lists and Trees Chapter 4.1Complex Models and Feature Notation 4.1-1 1 Complex Models, Lists and Trees 1 A Concrete Example of a Complex Model 2 B An Approach to Lists and Related Objects 3 C An Approach to Trees and Related Objects 8 D A General Class of Complex ModelsAT 12 2 Feature Notation for Complex Models 16 A Basic Notation 17 B Discussion and Further Examples 19 C Feature Names 21 D Implied Tree Structure 22 3 Model Establishment and Feature NotationAT 25 A Taxonomy of Features 25 B Principle of Minimal Specification 28 C Specification of Relations
• Secondary Features 29 D Extension and Specialization 31 Chapter 4.2Families and Lists 4.2-1 1 Families 3 A Definition of Family 3 B Families with ParameterAT 4 C Distributed FamiliesAT 5 2 Lists 7 A Unvalued Lists 7 B Basic Secondary Features of Lists 9 C Basic Order Properties of Lists 10 D Trichotomy Law 13 3 Basic Operations on Lists 14 A Initialization Operations 14 B Concatenation and Split Operations 15 C Insert and Remove 19 D Isomorphism and Base ConversionAT 23 4 Valued Lists and Related Operations 27 A Valued Lists 27 B Initialization Operations 30 C Concatenation and Split Operations 31 D Insert and Remove 33 E Resetting a Value 34 F Isomorphism and Base ConversionAT 35 5 Pointed Lists and Related Operations 37 A Pointed Lists 37 B Navigation Operations 41 C List Transformation Operations 4.2-44 Chapter 4.3Forests and Trees 4.3-1 1 Pure Forests and Trees 4 A Definition of Forests and Trees 4 B Basic Secondary Features of Forests 7 C Order Properties of Forests 9 D Quadrichotomy LawAT 12 E Three Sets of Subobjects of F : ForestAT 14 2 Operations on Forests and Trees 16 A Basic Operations 16 B Isomorphism and Base Set ConversionAT 19 3 Ordered Forests and Trees 23 A Definition of Ordered Forests and Trees 23 B Secondary Features of Ordered Forests 25 C Operations on Ordered Forests and Trees 27 D Isomorphism and Base Set ConversionAT 30 4 Valued (Ordered) Forests and Trees 31 A Valued Forests and Trees 31 B Operations on Valued Forests and Trees 33 C Valued Ordered Forests and Trees 35 D Operations on Finite Valued Ordered Forests and Trees 36 E Isomorphism and Base Set ConversionAT 38 5 Pointed Trees 40 A The Class TreePtd0 of Pointed Trees 40 B Navigation Operations in TreePtd0 41 C Tree Transformation Operations 43 Part 5 Application Case Studies Chapter 5.1Introduction to Applications 5.1-1 1 Aim of Part 5 1 2 Simple Applications 3 A An Evolving Set Model 3 B An Evolving Dictionary Model 4 3 Advanced Applications 5 A A Tree Editor 5 B A Resource Allocation Model 7 Chapter 5.2An Evolving Set Model 5.2-1 1 Introduction 1 2 Model Definition 3 A Application Domain and Objects 3 B Example: a Concrete Book Stock 4 3 Operations on SetStates 5 A Definitions 5 B Example: Book Stock Operations 7 4 Parametrized Version of the ModelAT 8 A Objects 8 B Operations 9 Chapter 5.3An Evolving Dictionary Model 5.3-1 1 Introduction 1 2 Model Definition: Objects 4 A Instances of Dictionaries 4 B Example: a Telephone Directory 5 C Formal Definition of a Dictionary 6 3 Operations on Dictionaries 7 A Dictionary Transformation Operations 7 B Retrieve Operations 9 4 Commands, Errors and Reports 12 A General Definition of Commands 12 B Dictionary Transformation Commands 14 C Retrieve Commands 15 Chapter 5.4A Tree Editor (TEd) 5.4-1 1 Introduction 1 2 Pointed Trees in TEd: the Class TreePtd1 3 A Definition of TreePtd1 3 B Secondary Features of TreePtd1 5 3 Navigation Operations in TEd 9 A Group Nav1 9 B Group Nav2 14 C Further Nav2 OperationsAT 16 4 Tree Transformation Operations in TEd 17 A Initialization 17 B General Insertion and Removal 18 C Point Insertion and Value Update 20 5 The Tree Editor as an Interactive System 23 A Introduction 23 B Full State Description 24 C Input, Output and Internal Variables 25 D Commands and Error Handling 26 E Details of TEd Commands 29 Chapter 5.5A General Resource Allocation Model (ResAll) 5.5-1 1 Introduction 1 A Resource Allocation Systems 1 B Aim of Chapter 3 C General Remarks 3 2 Core Model: Tasks and Resources 5 A Constant Features 5 B Variable Features 8 C Secondary Core Features 12 D Further Implications of the Core Model 14 3 Core Operations 16 A Initialization 16 B Task Operations 18 C Resource Operations 20 D Resource Allocation Operations 22 4 Agents and Authority 25 A Constant Features 25 B Agent Features 26 C Agent and Core Features 27 5 Agent-extended Operations 30 A Initialization 30 B Task Operations 31 C Other Operations 35 6 New Agent-related Operations 37 A User Operations 37 B Employee Operations 39 C Authority Level Operations 40 7 Decisions, Errors and Reports 42 A Error Handling 42 B Reports 43 C Extended Operations 44 D Query Operations 47 Special Symbols Sym-1 Bibliography Bib-1

「Nielsen BookData」 より

詳細情報

• NII書誌ID(NCID): BA24125762
• ISBN:
  • 0201544296
• LCCN: 94016315
• 出版国コード: uk
• タイトル言語コード: eng
• 本文言語コード: eng
• 出版地: Wokingham, England ; Reading, Mass.
• ページ数/冊数: xxiv, 668 p.
• 大きさ: 24 cm
• 分類:
  • LCC : QA76.9.S88
  • DC20 : 004.2/1
• 件名:
  • LCSH : System design
  • LCSH : Set theory
  • LCSH : Logic, Symbolic and mathematical
• 親書誌ID:
  • BA00203522