Logics of Specification Languages (eBook)

Dines Bjørner, Martin C. Henson (Herausgeber)

eBook Download: PDF

2007
XXII, 624 Seiten
Springer Berlin (Verlag)
9783540741077 (ISBN)

Infos

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.

Inhalt

Preface 6
1 Specification Languages 6
2 Structure of Book 10
3 Acknowledgements 11
References 11
Contents 14
List of Contributors 18
Part I Preludium 21
An Overview 22
1 The Book History 22
2 Formal Specification Languages 25
3 The Logics 28
References 31
Part II The Languages 32
Abstract State Machines for the Classroom – The Basics – 33
Introduction 33
I: Intuition and Foundations of ASM 34
1 What Makes ASM so Unique? 34
2 What Kind of Algorithms Do ASM Cover? 36
3 Pseudocode Programs and Their Semantics 41
II: The Formal Framework 44
4 Signatures and Structures 45
5 Sequential Small-Step ASM Programs 48
6 Properties of Sequential Small-Step ASM Programs 53
7 Gurevich’s Theorem 55
III: Extensions 56
8 Sequential Large-Step ASM Algorithms 56
9 Non-deterministic and Reactive ASM 57
10 Distributed ASM 59
11 ASM as a Specification Language 60
12 Conclusion 61
13 Acknowledgements 62
References 62
ASM Indexes 64
A Methodological Guide to the CafeOBJ Logic 171
1 The CafeOBJ Specification Language 171
2 Data Type Specification 174
3 Transitions 194
4 Behavioural Specification 208
5 Institutional Semantics 238
6 Structured Specifications 243
Acknowledgements 254
References 254
CafeOBJ Indexes 257
Casl – the Common Algebraic Specification Language 259
1 Introduction 259
2 Institutions and Logics 261
3 Many-Sorted Basic Specifications 262
4 Subsorted Basic Specifications 269
5 271
Language Constructs 271
6 Structured Specifications 273
7 Architectural Specifications 279
8 Refinement 290
9 Tools 292
10 Case Study 293
11 Conclusion 307
References 308
CASL Indexes 312
Duration Calculus 317
1 Introduction 319
2 Syntax, Semantics and Proof System 324
3 Extensions of Duration Calculus 339
4 Decidability, Undecidability and Model Checking 350
5 Some Links to Related Work 352
References 354
DC Indexes 363
The Logic of the RAISE Specification Language 366
1 Introduction 366
2 The RSL Logic 369
3 The Axiomatic Semantics: A Logic for Definition 382
4 The RSL Proof System: A Logic for Proof 386
5 Case Study 389
6 Conclusions 410
References 412
RAISE Indexes 414
The Specification Language TLA+ 417
1 Introduction 417
2 Example: A Simple Resource Allocator 418
3 TLA: The Temporal Logic of Actions 425
4 Deductive System Verification in TLA 439
5 Formalized Mathematics: The Added Value of TLA 446
6 The Resource Allocator Revisited 450
7 Conclusions 461
References 462
TLA 464
Indexes 464
The Typed Logic of Partial Functions and the Vienna Development Method 468
1 Introduction 468
2 The Vienna Development Method 469
3 A Proof Framework for VDM 479
4 The Typed Logic of Partial Functions 482
5 Theories Supporting VDM-SL 487
6 Three Approaches to Supporting Logic in VDM 492
7 Conclusions and Future Directions 496
References 497
VDM Indexes 500
Z Logic and Its Applications 503
1 Introduction 503
2 Initial Considerations 504
3 The Specification Logic ZC 512
4 Conservative Extensions 518
5 Equational Logic 523
6 Precondition Logic 523
7 Operation Refinement 525
8 Four Equivalent Theories 532
9 The Non-lifted Totalisation 540
10 The Strictly-Lifted Totalisation 545
11 Data Refinement (Forward) 547
12 Four (Forward) Theories 550
13 Three Equivalent Theories 553
14 The Non-lifted Totalisation underlying Data Refinement 559
15 Data Refinement (Backward) 562
16 Four (Backward) Theories 564
17 Four Equivalent Theories 566
18 The Non-lifted Totalisation underlying Data Refinement 571
19 Discussion 575
20 Operation Refinement and Monotonicity in the Schema Calculus 578
21 Distributivity Properties of the Chaotic Completion 591
22 Conclusions 602
23 Acknowledgements 602
References 603
Indexes 606
Part III Postludium 611
Reviews 612
1 Yuri Gurevich: ASM 612
2 Jean-Raymond Abrial: On B and event-B 615
3 Kokichi Futatsugi: Formal Methods and 617
4 Peter D. Mosses: A View of the CASL 620
5 Zhou Chaochen: Duration Calculus 622
6 Klaus Havelund: RAISE in Perspective 624
7 Cliff B. Jones: VDM Postludium” 627
8 Leslie Lamport: The Specification Language TLA 629
9 James C.P. Woodcock: Z Logic and Its Applications 633
10 Closing: Dines Bjørner and Martin C. Henson 636

Produkt-Details

• Erscheint lt. Verlag: 5.12.2007
• Reihe/Serie: Monographs in Theoretical Computer Science. An EATCS Series
• Reihe/Serie: Monographs in Theoretical Computer Science. An EATCS Series
• Zusatzinfo: XXII, 624 p. 69 illus.
• Verlagsort: Berlin
• Sprache: englisch
• Themenwelt: Mathematik / Informatik ► Informatik ► Programmiersprachen / -werkzeuge
• Themenwelt: Mathematik / Informatik ► Informatik ► Software Entwicklung
• Schlagworte: ASM (Abstract State Machines) • Bjørner • Bjørner • CafeOBJ • CASL (Common Algebraic Specification Language) • Duration Calculus • Event-B and B specification language • formal methods • Formal specification languages • Logic • Programming Techniques • Proof rules • RSL (RAIS • RSL (RAISE Specification Language) • Semantics • Software engineering • Syntax • TLA (Temporal Logic of Actions) • VDM (Vienna Development Method) • Z Specification Language
• ISBN-13: 9783540741077 / 9783540741077