دسترسی نامحدود
برای کاربرانی که ثبت نام کرده اند
دانلود کتاب Data Refinement: Model-Oriented Proof Methods and their Comparison
دانلود کتاب پالایش داده ها: روش های اثبات مدل گرا و مقایسه آنها
مشخصات کتاب
Data Refinement: Model-Oriented Proof Methods and their Comparison
ویرایش:
نویسندگان: Willem-Paul de Roever. Kai Engelhardt
سری: Cambridge Tracts in Theoretical Computer Science 47
ISBN (شابک) : 9780511663079, 9780521103503
ناشر: Cambridge University Press
سال نشر: 2008
تعداد صفحات: 436
زبان: English
فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود)
حجم فایل: 17 مگابایت
قیمت کتاب (تومان) : 37,000
در صورت تبدیل فایل کتاب Data Refinement: Model-Oriented Proof Methods and their Comparison به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.
توجه داشته باشید کتاب پالایش داده ها: روش های اثبات مدل گرا و مقایسه آنها نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.
توضیحاتی در مورد کتاب پالایش داده ها: روش های اثبات مدل گرا و مقایسه آنها
هدف این کتاب ارائه مقدمه ای جامع و منظم بر روش مهم و بسیار کاربردی پالایش داده ها و روش های شبیه سازی مورد استفاده برای اثبات درستی آن است. نویسندگان در بخش اول بر اصول کلی مورد نیاز برای اثبات صحت پالایش داده ها تمرکز می کنند. آنها با توضیح مفاهیم اساسی شروع می‌کنند و نشان می‌دهند که اثبات‌های پالایش داده‌ها به شبیه‌سازی اثبات می‌شوند. مباحث Hoare Logic و Refinement Calculus معرفی شده و نظریه ای کلی از شبیه سازی ها ایجاد و مرتبط با آن ها می باشد. دسترسی و درک مطلب به منظور هدایت افراد تازه وارد به منطقه مورد تاکید قرار گرفته است. بخش دوم کتاب شامل بررسی دقیق روش‌های مهم در این زمینه، مانند VDM، و روش‌های ناشی از Abadi & Lamport، Hehner، Lynch و Reynolds، Back's refinement Calculus و Z است. یا ناقص باشند، با مثال‌های متضاد برای کاربردشان، یا همیشه قابل اجرا در هر زمان که پالایش داده‌ها برقرار است. این امر با اثبات، برای اولین بار، نشان می‌دهد که همه این روش‌ها را می‌توان در قالب دو مفهوم ساده توصیف و تحلیل کرد: شبیه‌سازی رو به جلو و عقب. این کتاب خودکفا است، از سطح پیشرفته لیسانس می‌گذرد و خواننده را در روش‌های اثبات شبیه‌سازی به وضعیت هنر می‌برد.
توضیحاتی درمورد کتاب به خارجی
The goal of this book is to provide a comprehensive and systematic introduction to the important and highly applicable method of data refinement and the simulation methods used for proving its correctness. The authors concentrate in the first part on the general principles needed to prove data refinement correct. They begin with an explanation of the fundamental notions, showing that data refinement proofs reduce to proving simulation. The topics of Hoare Logic and the Refinement Calculus are introduced and a general theory of simulations is developed and related to them. Accessibility and comprehension are emphasized in order to guide newcomers to the area. The book's second part contains a detailed survey of important methods in this field, such as VDM, and the methods due to Abadi & Lamport, Hehner, Lynch and Reynolds, Back's refinement calculus and Z. All these methods are carefully analysed, and shown to be either imcomplete, with counterexamples to their application, or to be always applicable whenever data refinement holds. This is shown by proving, for the first time, that all these methods can be described and analyzed in terms of two simple notions: forward and backward simulation. The book is self-contained, going from advanced undergraduate level and taking the reader to the state of the art in methods for proving simulation.
فهرست مطالب
Cover......Page 1
Frontmatter......Page 2
Contents......Page 6
Preface......Page 9
Part I - Theory......Page 14
1.1 Goal and Motivation......Page 15
1.2 Introduction to Data Refinement......Page 17
1.3 Historical Background......Page 30
2.1 Introducing Simulation......Page 32
2.2 Soundness and (In)completeness of Simulation......Page 35
2.3 Data Invariants, Abstraction Relations, and Normal Variables......Page 38
2.4 Towards a Syntactic Characterization of Simulation......Page 47
2.5 Historical Background......Page 59
3.1 Partial Orders and Monotonicity......Page 62
3.2 Binary Relations......Page 63
3.3 Recursion and Termination --- the [GREEK SMALL LETTER MU]-Calculus......Page 68
3.4 Relational Semantics of Recursion --- the Continuous [GREEK SMALL LETTER MU]-Calculus......Page 69
3.5 Reasoning about Termination --- the Monotone [GREEK SMALL LETTER MU]-Calculus......Page 75
3.6 Historical Background......Page 84
4 - Properties of Simulation......Page 86
4.1 Composing Simulation Diagrams......Page 87
4.2 Implications between Simulations......Page 90
4.3 Data Invariants and Totality of Abstraction Relations......Page 93
4.4 Soundness of Simulation......Page 94
4.5 Maximal Data Types......Page 95
4.6 Completeness......Page 96
4.7 Historical Background......Page 100
5 - Notation and Semantics......Page 103
5.1 Introduction......Page 104
5.2 Predicates......Page 106
5.3 Programs......Page 121
5.4 Relational Terms......Page 125
5.5 Correctness Formulae......Page 128
5.6 Historical Background......Page 132
6 - A Hoare Logic......Page 134
6.1 Proof System......Page 135
6.2 Soundness and (Relative) Completeness......Page 141
6.3 Historical Background......Page 143
7 - Simulation and Hoare Logic......Page 145
7.2 L-simulation in Hoare Logic......Page 146
7.3 L[MINUS SIGN]1 -simulation in Hoare Logic......Page 156
7.5 Historical Background......Page 157
8 - An Extension to Total Correctness......Page 159
8.1 Semantic Model and Basic Fixed Point Theory......Page 161
8.2 Interpretation Functions for Total Correctness......Page 173
8.3 Historical Background......Page 191
9.1 Simulation......Page 194
9.2 An L-Simulation Theorem for Total Correctness......Page 202
9.3 Historical Background......Page 206
10 - Refinement Calculus......Page 207
10.1 Lattice-theoretical Framework......Page 209
10.2 Predicate Transformer Semantics......Page 219
10.3 Predicate Transformers and Data Refinement......Page 228
10.4 Predicate Transformers and Partial Correctness......Page 236
10.5 Historical Background......Page 247
Picture Gallery......Page 249
Part II - Applications......Page 268
11.1 Introduction......Page 270
Running Examnle: Finding Paths in Directed Graohs......Page 271
Analysis of Data Refinement à la Reynolds......Page 285
Historical Background......Page 300
12.1 Introduction......Page 302
12.2 Example: Dictionary......Page 304
12.3 Analysis of Data Refinement in VDM......Page 314
12.4 Historical Background......Page 328
13 - Z, Hehner's Method, and Back's Refinement Calculus......Page 330
13.1 Z......Page 331
13.2 Hehner's Method for Data Refinement......Page 340
13.3 Back's Refinement Calculus......Page 345
14 - Refinement Methods due to Abadi and Lamport and to Lynch......Page 353
14.1 Auxiliary Variables and Refinement Mappings......Page 354
14.2 Possibilities Mappings......Page 371
14.3 Historical Background......Page 374
Appendix A - An Introduction to Hoare Logic......Page 376
Appendix B - A Primer on Ordinals and Transfinite Induction......Page 400
Appendix C - Notational Convention......Page 407
Appendix D - Precedences......Page 415
Bibliography......Page 417
Index......Page 432
