Logics of specification languages

By a specification language we understand a formal system of syntax, semantics and proof rules. The syntax and semantics define a language; the proof rules define a proof system. Specifications are expressions in the language, and reasoning over properties of these specifications is done within the proof system. 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. Dedicated chapters address: the use of ASM (Abstract State Machines) in the classroom; the Event-B modelling method; a methodological guide to CafeOBJ logic; CASL, the Common Algebraic Specification Language; the Duration Calculus; the logic of the RAISE specification language (RSL); the specification language TLA+; the typed logic of partial functions and the Vienna Development Method (VDM); and Z logic and its applications. Each chapter is self-contained, with references, and symbol and concept indexes. Finally, in a unique feature, the book closes with short commentaries on the specification languages written by researchers closely associated with their original development.

With extensive references and pointers to future developments, this book will be of interest to researchers and graduate students engaged with formal specification languages.

Dines Bjørner and Martin C. HensonWolfgang ReisigDominique Cansell and Dominique MéryRăzvan DiaconescuT. Mossakowski and A. Haxthausen and D. Sannella and A. TarleckiMichael R. HansenChris George and Anne E. HaxthausenStephan MerzJohn S. FitzgeraldM C Henson and M Deutsch and S ReevesDines Bjørner and Martin HensonYuri GurevichJean-Raymond AbrialKokichi FutatsugiPeter D. MossesZhou ChaochenKlaus HavelundCliff B. JonesLeslie LamportJames C.P. WoodcockDines Bjørner and Martin C. Henson

Preface	p. VII
1 Specification Languages	p. VII
2 Structure of Book	p. XI
3 Acknowledgements	p. XII
References	p. XII
Part I Preludium
An Overview	p. 3
1 The Book History	p. 3
2 Formal Specification Languages	p. 6
3 The Logics	p. 9
References	p. 12
Part II The Languages
Abstract State Machines for the Classroom	p. 15
I Intuition and Foundations of ASM	p. 16
1 What Makes ASM so Unique?	p. 16
2 What Kind of Algorithms Do ASM Cover?	p. 18
3 Pseudocode Programs and Their Semantics	p. 23
II The Formal Framework	p. 26
4 Signatures and Structures	p. 27
5 Sequential Small-Step ASM Programs	p. 30
6 Properties of Sequential Small-Step ASM Programs	p. 35
7 Gurevich's Theorem	p. 37
III Extensions	p. 38
8 Sequential Large-Step ASM Algorithms	p. 38
9 Non-deterministic and Reactive ASM	p. 39
10 Distributed ASM	p. 41
11 ASM as a Specification Language	p. 42
12 Conclusion	p. 43
13 Acknowledgements	p. 44
References	p. 44
ASM Indexes	p. 46
The event-B Modelling Method: Concepts and Case Studies	p. 47
1 Introduction	p. 47
2 The B Language	p. 50
3 B Models	p. 62
4 Sequential Algorithms	p. 77
5 Combining Coordination and Refinement for Sorting	p. 93
6 Spanning-tree Algorithms	p. 112
7 Design of Distributed Algorithms by Refinement	p. 124
8 Conclusion	p. 142
References	p. 145
Event B Indexes	p. 150
A Methodological Guide to the CafeOBJ Logic	p. 153
1 The CafeOBJ Specification Language	p. 153
2 Data Type Specification	p. 156
3 Transitions	p. 176
4 Behavioural Specification	p. 190
5 Institutional Semantics	p. 220
6 Structured Specifications	p. 225
Acknowledgement	p. 236
References	p. 236
CafeOBJ Indexes	p. 239
Casl - the Common Algebraic Specification Language	p. 241
1 Introduction	p. 241
2 Institutions and Logics	p. 243
3 Many-Sorted Basic Specifications	p. 244
4 Subsorted Basic Specifications	p. 251
5 Casl Language Constructs	p. 253
6 Structured Specifications	p. 255
7 Architectural Specifications	p. 261
8 Refinement	p. 272
9 Tools	p. 274
10 Case Study	p. 275
11 Conclusion	p. 289
References	p. 290
CASL Indexes	p. 294
Duration Calculus	p. 299
1 Introduction	p. 301
2 Syntax, Semantics and Proof System	p. 306
3 Extensions of Duration Calculus	p. 321
4 Decidability, Undecidability and Model Checking	p. 332
5 Some Links to Related Work	p. 334
References	p. 336
DC Indexes	p. 345
The Logic of the RAISE Specification Language	p. 349
1 Introduction	p. 349
2 The RSL Logic	p. 352
3 The Axiomatic Semantics: A Logic for Definition	p. 365
4 The RSL Proof System: A Logic for Proof	p. 369
5 Case Study	p. 372
6 Conclusions	p. 393
References	p. 395
RAISE Indexes	p. 397
The Specification Language TLA +	p. 401
1 Introduction	p. 401
2 Example: A Simple Resource Allocator	p. 402
3 TLA: The Temporal Logic of Actions	p. 409
4 Deductive System Verification in TLA	p. 423
5 Formalized Mathematics: The Added Value of TLA +	p. 430
6 The Resource Allocator Revisited	p. 434
7 Conclusions	p. 445
References	p. 446
TLA + Indexes	p. 448
The Typed Logic of Partial Functions and the Vienna Development Method	p. 453
1 Introduction	p. 453
2 The Vienna Development Method	p. 454
3 A Proof Framework for VDM	p. 464
4 The Typed Logic of Partial Functions	p. 467
5 Theories Supporting VDM-SL	p. 472
6 Three Approaches to Supporting Logic in VDM	p. 477
7 Conclusions and Future Directions	p. 481
References	p. 482
VDM Indexes	p. 485
Z Logic and Its Applications	p. 489
1 Introduction	p. 489
2 Initial Considerations	p. 490
3 The Specification Logic Zc	p. 498
4 Conservative Extensions	p. 504
5 Equational Logic	p. 509
6 Precondition Logic	p. 509
7 Operation Refinement	p. 511
8 Four Equivalent Theories	p. 518
9 The Non-lifted Totalisation	p. 526
10 The Strictly-Lifted Totalisation	p. 531
11 Data Refinement (Forward)	p. 533
12 Four (Forward) Theories	p. 536
13 Three Equivalent Theories	p. 539
14 The Non-lifted Totalisation underlying Data Refinement	p. 545
15 Data Refinement (Backward)	p. 548
16 Four (Backward) Theories	p. 550
17 Four Equivalent Theories	p. 552
18 The Non-lifted Totalisation underlying Data Refinement	p. 557
19 Discussion	p. 561
20 Operation Refinement and Monotonicity in the Schema Calculus	p. 564
21 Distributivity Properties of the Chaotic Completion	p. 577
22 Conclusions	p. 588
23 Acknowledgements	p. 588
References	p. 589
Part III Postludium
Reviews	p. 599
1 ASM	p. 599
2 On B and event-B	p. 602
3 Formal Methods and CafeOBJ	p. 604
4 A View of the CASL	p. 607
5 Duration Calculus	p. 609
6 RAISE in Perspective	p. 611
7 VDM "Postludium"	p. 614
8 The Specification Language TLA +	p. 616
9 Z Logic and Its Applications	p. 620
10 Closing	p. 623

Available:*

On Order

Summary

Summary

Table of Contents