Z : An Introduction to Formal Methods (2 SUB)

個数:
  • ポイントキャンペーン

Z : An Introduction to Formal Methods (2 SUB)

  • 提携先の海外書籍取次会社に在庫がございます。通常2週間で発送いたします。
    重要ご説明事項
    1. 納期遅延や、ご入手不能となる場合が若干ございます。
    2. 複数冊ご注文の場合、分割発送となる場合がございます。
    3. 美品のご指定は承りかねます。
  • ≪洋書のご注文につきまして≫ 「海外取次在庫あり」および「国内仕入れ先からお取り寄せいたします」表示の商品でも、納期の目安期間内にお届けできないことがございます。あらかじめご了承ください。

  • 製本 Paperback:紙装版/ペーパーバック版
  • 言語 ENG
  • 商品コード 9780471939733
  • DDC分類 005.12

Full Description


Offers a thorough and comprehensive tutorial introduction to Z. Uses standard notation with practical exercises and clear descriptions and explanations. Contains information on how to relate Z specifications to actual program code and is enhanced to reflect the most current language standards.

Table of Contents

Preface                                            xv
Acknowledgements xix
I Tutorial 1 (122)
Introduction 3 (6)
What is Z? 3 (2)
Specification Foretaste 5 (2)
Numbers 7 (2)
First-order Logic 9 (22)
Propositional Calculus 9 (14)
Introduction 9 (1)
Truth-functional Connectives and Constant 10 (5)
Formulas
Model-theory 15 (4)
Useful Laws 19 (4)
Predicate Calculus 23 (5)
Introduction 23 (1)
Types 24 (1)
Declarations 24 (1)
Quantifiers 25 (2)
Term-Forming Operators 27 (1)
Exercises 28 (3)
Set Theory 31 (10)
Ways of Making Sets 31 (2)
Enumeration 31 (1)
Set Comprehension 32 (1)
Relations between Sets (and their Members) 33 (1)
Membership and Equality 33 (1)
Subset 33 (1)
Some Special Sets 34 (1)
Empty Sets 34 (1)
Power Sets 35 (1)
Operations on Sets 35 (3)
Union 35 (1)
Intersection 35 (1)
Difference 36 (1)
Symmetric Difference 36 (2)
Useful Laws 38 (1)
Generalized Union and Intersection 38 (1)
Exercises 38 (3)
Internal Telephone Directory 41 (30)
Introduction 41 (1)
Cartesian Products and Relations 42 (1)
The State Space 43 (5)
The Domain of a Relation 45 (1)
The Range of a Relation 45 (1)
The Union of Two Relations 46 (1)
Schemas 46 (2)
Adding an Entry to the Database 48 (7)
The First Account 48 (1)
Schema Operations 49 (4)
A Concise Specification 53 (1)
Dealing with Errors 53 (1)
The Total Specification 54 (1)
Interrogating the Database by Person 55 (2)
The Image of a Relation 55 (1)
Specifying the Operation 56 (1)
Interrogating the Database by Number 57 (2)
Relational Inversion 58 (1)
Specifying the Operation 58 (1)
Removing an Entry from the Database 59 (1)
Someone Joining the University 60 (1)
Someone Leaving the University 60 (2)
Domain Restriction 60 (1)
Domain Anti-restriction 61 (1)
Specifying the Operation 62 (1)
Specifying a User-Interface 62 (2)
Presenting a Formal Specification 64 (5)
Definition Before Use 64 (1)
The Format of a Sequential System 65 (3)
Combining Z and Descriptive Text 68 (1)
Conventions for Identifiers 68 (1)
Exercises 69 (2)
More about Relations and Schemas 71 (20)
Relations 71 (6)
Composition 71 (1)
Identity, Powers and Closures 72 (2)
Range Restriction and Anti-restriction 74 (2)
Overriding 76 (1)
Schemas 77 (11)
Horizontal Form 77 (1)
Renaming 78 (1)
Hiding 79 (1)
Composition 79 (5)
Piping 84 (2)
As Types 86 (1)
The θ Operator 87 (1)
Exercises 88 (3)
Functions 91 (6)
Introduction 91 (1)
Specifying a Weather Map 91 (2)
Introduction 91 (1)
Updating the Weather Map 92 (1)
Looking up the temperature of a Region 93 (1)
Constrained Functions 93 (2)
Introduction 93 (1)
Potentially Non-finite Functions 94 (1)
Finite Functions 94 (1)
Function Definition 95 (1)
Enumeration 95 (1)
Set Comprehension 95 (1)
The lambda;-notation 95 (1)
Modelling Arrays 96 (1)
Sequences 97 (6)
Fundamental Ideas 97 (1)
Defining Sequences 97 (1)
Sequence Manipulating Functions 98 (3)
Exercises 101(2)
Bags 103(12)
Introduction 103(1)
Bag Manipulating Functions 103(2)
A specification of Sorting 105(1)
The Specification of a Vending Machine 106(9)
Introduction 106(2)
Pricing Goods 108(1)
Acceptable Coins 109(1)
Restocking 109(2)
Buying 111(3)
Profit Taking 114(1)
Free Types 115(8)
Introduction 115(1)
Lists as a Free Type 115(1)
Specifying Sequence Proofs 116(4)
Introduction 116(3)
The Specifications 119(1)
The Formal Treatment of Free Types 120(3)
II Methods of Reasoning 123(98)
Formal Proof 125(26)
Propositional Calculus 125(15)
Introduction 125(3)
Notational Conventions 128(1)
Themata 128(2)
Start Sequents and Proofs 130(3)
Derived Thematic Rules 133(4)
Further Examples of Proofs 137(3)
Soundness and Completeness 140(1)
Predicate Calculus 140(8)
Introduction 140(1)
Quantifier Rules 140(2)
Examples of Proofs 142(4)
Useful Laws 146(2)
Theorems, Sequents and Themata 148(2)
Exercises 150(1)
Rigorous Proof 151(10)
Introduction 151(1)
Reasoning about Sets 151(5)
Reasoning about Tuples 156(1)
Mathematical Induction 157(1)
Induction for Sequences 158(1)
Exercises 159(2)
Immanent Reasoning 161(10)
Introduction 161(1)
Specifying a Classroom 161(1)
Schemas and Formulas 162(1)
The Initialization Proof Obligation 163(1)
Constructing Theories about Specifications 164(1)
Investigating Preconditions 165(3)
Totally 168(1)
Operation Refinement 169(2)
Reification and Decomposition 171(18)
Introduction 171(1)
Modelling Sets by Sequences 172(8)
Correctness of Operation Modelling 173(3)
Modelling Set Intersection 176(2)
Modelling Set Difference 178(2)
Reification and Decomposition using Schemas 180(9)
Introduction 180(1)
Example Specification and Design 180(1)
Relating Specification and Design 181(1)
Correctness of Design 181(5)
General Correctness of Design 186(3)
Floyd-Hoare Logic 189(14)
Introduction 189(1)
Hoare Triples 190(1)
Start Sequents and Themata 191(5)
Introduction 191(1)
Structural Rules 191(1)
The skip Command 192(1)
Substitution 192(1)
Assignment 192(1)
Sequencing 193(1)
The while-loop 194(1)
The Conditional 195(1)
The for-loop 195(1)
Total Correctness 196(1)
Using Mathematical Variables 196(1)
Verification Conditions 197(3)
Introduction 197(1)
The skip Command 198(1)
Assignment 198(1)
The Conditional 198(1)
Sequencing 199(1)
The while-loop 199(1)
The for-loop 199(1)
An Example 200(1)
Conclusion 200(3)
Getting to Program Code 203(18)
The Transformation Recipe 203(1)
Modelling a Simple Bank Account 204(4)
Adding Messages 206(2)
A Sales Database 208(11)
Informal Account 208(1)
The State Space 209(1)
The Operations 210(3)
The User-interface 213(2)
Calculating Preconditions 215(1)
The Implementation 215(4)
Conclusion 219(2)
III Case Studies 221(48)
Two Small Case Studies 223(10)
The Bill of Materials Problem 223(5)
Introduction 223(1)
Representing the Database 223(1)
Specifying Parts Explosion 224(1)
Another Specification 225(3)
A route Planner 228(5)
Introduction 228(2)
The State Space 230(1)
The Operations 230(3)
Wing's Library Problem 233(22)
Introduction 233(1)
Basic Types and User-defined Sets 234(1)
The State of the System 235(3)
The Operations 238(17)
Checking Out and Returning Copies of Books 238(5)
Adding and Removing Copies of Books 243(6)
Interrogating the Library Database 249(6)
Partial Specification of a Text-editor 255(14)
Introduction 255(1)
Basic Types 255(1)
The State Space 256(1)
The Operations 256(6)
Operations to the Left of the Cursor 256(3)
Operations to the Right of the Cursor 259(3)
The Doc2 State 262(4)
Promoting Doc1 Operations to Doc2 Ones 265(1)
The Doc 3 Model 266(2)
Putting a Window on the Unbounded Display 266(2)
Conclusion 268(1)
IV Specification Animation 269(10)
Animation using Miranda 271(8)
Introduction 271(1)
The Animation 271(8)
Overall Structure 271(1)
Basic Types 271(1)
The State Space 272(1)
The Initial State 273(1)
The Operations 273(2)
The Miranda Script 275(4)
V Reference Manual 279(30)
Methods of Definition 281(4)
Axiomatic Description 281(1)
Generic Definition 282(1)
Schema Definition 283(2)
Formal Definitions 285(14)
Sets 285(2)
Relations between Sets 285(1)
Operators on Sets 285(1)
Generalized Union and Intersection 286(1)
Finite Sets 286(1)
Smallest and Largest Elements 287(1)
Relations 287(3)
Introduction 287(1)
Domains and Ranges 287(1)
Inversion 288(1)
Domain Restriction and Anti-restriction 288(1)
Range Restriction and Anti-restriction 288(1)
Composition 289(1)
Image 289(1)
Interation and Closures 289(1)
Overriding 290(1)
Functions 290(2)
Possibly Non-finite Functions 290(2)
Finite Functions 292(1)
Lambda Abstraction 292(1)
Sequences 292(3)
Basic Definitions 292(1)
Sequence Constructors 292(1)
Sequence Destructors 293(1)
Reversing a Sequence 294(1)
Disjointness and Partitioning 294(1)
Bags 295(4)
Basic Definitions 295(1)
Bag Manipulating Operators 295(4)
Rules and Obligations 299(10)
First-order Logic 299(4)
Start Sequents 299(1)
Themata 299(4)
Reasoning about Sets 303(1)
Reasoning about Tuples 304(1)
Floyd-Hoare Logic 304(1)
Induction 305(1)
Mathematical Induction 305(1)
Induction for Sequences 306(1)
Proof Obligations for Refinement 306(3)
Operation Refinement 306(1)
Data Refinement 307(2)
VI Appendices 309(48)
A Variable Conventions 311(2)
B Answers to Exercises 313(20)
C Glossary of Terms 333(18)
D Glossary of Symbols 351(6)
Bibliography 357(6)
Index 363