Bjørner / Henson / Bjorner Logics of Specification Languages

1. Auflage 2007
ISBN: 978-3-540-74107-7
Verlag: Springer Berlin Heidelberg
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Englisch, 624 Seiten

Reihe: Monographs in Theoretical Computer Science. An EATCS Series

This book presents comprehensive studies on nine specification languages and their logics of reasoning. The editors and authors are authorities on these specification languages and their application. In a unique feature, the book closes with short commentaries on the specification languages written by researchers closely associated with their original development. The book contains extensive references and pointers to future developments.

Autoren/Hrsg.

Bjørner, Dines

Henson, Martin C.

Bjorner, Dines

Inhaltsverzeichnis

1;Preface;6
1.1;1 Specification Languages;6
1.2;2 Structure of Book;10
1.3;3 Acknowledgements;11
1.4;References;11
2;Contents;14
3;List of Contributors;18
4;Part I Preludium;21
4.1;An Overview;22
4.1.1;1 The Book History;22
4.1.2;2 Formal Specification Languages;25
4.1.3;3 The Logics;28
4.1.4;References;31
5;Part II The Languages;32
5.1;Abstract State Machines for the Classroom – The Basics –;33
5.1.1;Introduction;33
5.1.2;I: Intuition and Foundations of ASM;34
5.1.3;1 What Makes ASM so Unique?;34
5.1.4;2 What Kind of Algorithms Do ASM Cover?;36
5.1.5;3 Pseudocode Programs and Their Semantics;41
5.1.6;II: The Formal Framework;44
5.1.7;4 Signatures and Structures;45
5.1.8;5 Sequential Small-Step ASM Programs;48
5.1.9;6 Properties of Sequential Small-Step ASM Programs;53
5.1.10;7 Gurevich’s Theorem;55
5.1.11;III: Extensions;56
5.1.12;8 Sequential Large-Step ASM Algorithms;56
5.1.13;9 Non-deterministic and Reactive ASM;57
5.1.14;10 Distributed ASM;59
5.1.15;11 ASM as a Specification Language;60
5.1.16;12 Conclusion;61
5.1.17;13 Acknowledgements;62
5.1.18;References;62
5.1.19;ASM Indexes;64
5.2;A Methodological Guide to the CafeOBJ Logic;171
5.2.1;1 The CafeOBJ Specification Language;171
5.2.2;2 Data Type Specification;174
5.2.3;3 Transitions;194
5.2.4;4 Behavioural Specification;208
5.2.5;5 Institutional Semantics;238
5.2.6;6 Structured Specifications;243
5.2.7;Acknowledgements;254
5.2.8;References;254
5.2.9;CafeOBJ Indexes;257
5.3;Casl – the Common Algebraic Specification Language;259
5.3.1;1 Introduction;259
5.3.2;2 Institutions and Logics;261
5.3.3;3 Many-Sorted Basic Specifications;262
5.3.4;4 Subsorted Basic Specifications;269
5.3.5;5;271
5.3.6;Language Constructs;271
5.3.7;6 Structured Specifications;273
5.3.8;7 Architectural Specifications;279
5.3.9;8 Refinement;290
5.3.10;9 Tools;292
5.3.11;10 Case Study;293
5.3.12;11 Conclusion;307
5.3.13;References;308
5.3.14;CASL Indexes;312
5.4;Duration Calculus;317
5.4.1;1 Introduction;319
5.4.2;2 Syntax, Semantics and Proof System;324
5.4.3;3 Extensions of Duration Calculus;339
5.4.4;4 Decidability, Undecidability and Model Checking;350
5.4.5;5 Some Links to Related Work;352
5.4.6;References;354
5.4.7;DC Indexes;363
5.5;The Logic of the RAISE Specification Language;366
5.5.1;1 Introduction;366
5.5.2;2 The RSL Logic;369
5.5.3;3 The Axiomatic Semantics: A Logic for Definition;382
5.5.4;4 The RSL Proof System: A Logic for Proof;386
5.5.5;5 Case Study;389
5.5.6;6 Conclusions;410
5.5.7;References;412
5.5.8;RAISE Indexes;414
5.6;The Specification Language TLA+;417
5.6.1;1 Introduction;417
5.6.2;2 Example: A Simple Resource Allocator;418
5.6.3;3 TLA: The Temporal Logic of Actions;425
5.6.4;4 Deductive System Verification in TLA;439
5.6.5;5 Formalized Mathematics: The Added Value of TLA;446
5.6.6;6 The Resource Allocator Revisited;450
5.6.7;7 Conclusions;461
5.6.8;References;462
5.6.9;TLA;464
5.6.10;Indexes;464
5.7;The Typed Logic of Partial Functions and the Vienna Development Method;468
5.7.1;1 Introduction;468
5.7.2;2 The Vienna Development Method;469
5.7.3;3 A Proof Framework for VDM;479
5.7.4;4 The Typed Logic of Partial Functions;482
5.7.5;5 Theories Supporting VDM-SL;487
5.7.6;6 Three Approaches to Supporting Logic in VDM;492
5.7.7;7 Conclusions and Future Directions;496
5.7.8;References;497
5.7.9;VDM Indexes;500
5.8;Z Logic and Its Applications;503
5.8.1;1 Introduction;503
5.8.2;2 Initial Considerations;504
5.8.3;3 The Specification Logic ZC;512
5.8.4;4 Conservative Extensions;518
5.8.5;5 Equational Logic;523
5.8.6;6 Precondition Logic;523
5.8.7;7 Operation Refinement;525
5.8.8;8 Four Equivalent Theories;532
5.8.9;9 The Non-lifted Totalisation;540
5.8.10;10 The Strictly-Lifted Totalisation;545
5.8.11;11 Data Refinement (Forward);547
5.8.12;12 Four (Forward) Theories;550
5.8.13;13 Three Equivalent Theories;553
5.8.14;14 The Non-lifted Totalisation underlying Data Refinement;559
5.8.15;15 Data Refinement (Backward);562
5.8.16;16 Four (Backward) Theories;564
5.8.17;17 Four Equivalent Theories;566
5.8.18;18 The Non-lifted Totalisation underlying Data Refinement;571
5.8.19;19 Discussion;575
5.8.20;20 Operation Refinement and Monotonicity in the Schema Calculus;578
5.8.21;21 Distributivity Properties of the Chaotic Completion;591
5.8.22;22 Conclusions;602
5.8.23;23 Acknowledgements;602
5.8.24;References;603
5.8.25;Indexes;606
6;Part III Postludium;611
6.1;Reviews;612
6.1.1;1 Yuri Gurevich: ASM;612
6.1.2;2 Jean-Raymond Abrial: On B and event-B;615
6.1.3;3 Kokichi Futatsugi: Formal Methods and;617
6.1.4;4 Peter D. Mosses: A View of the CASL;620
6.1.5;5 Zhou Chaochen: Duration Calculus;622
6.1.6;6 Klaus Havelund: RAISE in Perspective;624
6.1.7;7 Cliff B. Jones: VDM Postludium”;627
6.1.8;8 Leslie Lamport: The Specification Language TLA;629
6.1.9;9 James C.P. Woodcock: Z Logic and Its Applications;633
6.1.10;10 Closing: Dines Bjørner and Martin C. Henson;636