| Preface | p. ix |
| Introduction and Overview | p. 1 |
| Introduction | p. 2 |
| Central Questions | p. 2 |
| Structure of this Chapter | p. 2 |
| Basic Concepts of Concurrency | p. 3 |
| Why Concurrent Programs Should be Proved Correct | p. 8 |
| The Approach of this Book | p. 33 |
| Compositionality | p. 46 |
| From Noncomp. to Comp. Proof Methods - a historical perspective | p. 62 |
| The Inductive Assertion Method | p. 71 |
| Floyd's Inductive Assertion Method for Transition Diagrams | p. 72 |
| Objectives of Part II | p. 72 |
| Structure of this Chapter | p. 75 |
| Sequential Transition Diagrams and Systems | p. 76 |
| Specification and Correctness Statements | p. 82 |
| A Proof Method for Partial Correctness | p. 88 |
| Soundness | p. 92 |
| Semantic Completeness of the Inductive Assertion Method | p. 93 |
| Proving Convergence | p. 98 |
| Proving Absence of Runtime Errors | p. 104 |
| Historical Notes | p. 111 |
| The Inductive Assertion Method for Shared-Variable Concurrency | p. 119 |
| Objective and Structure of this Chapter | p. 119 |
| A Characterisation of Concurrent Execution | p. 121 |
| Is this Characterisation of Concurrent Execution Justified? | p. 132 |
| The Generalisation of Floyd's Approach to Nondeterministic Interleavings | p. 134 |
| Concurrent Transition Systems with Shared Variables | p. 137 |
| Proving Convergence for Shared-Variable Concurrency | p. 188 |
| Proving Deadlock Freedom | p. 203 |
| Proving Absence of Runtime Errors | p. 206 |
| Historical Notes | p. 208 |
| The Inductive Assertion Method for Synchronous Message Passing | p. 221 |
| Objective and Introduction | p. 221 |
| Structure of this Chapter | p. 223 |
| Syntax and Semantics of Synchronous Transition Diagrams | p. 223 |
| Proof Methods for Partial Correctness | p. 227 |
| Semantic Completeness | p. 249 |
| Technical Note: Modifications Towards Compositionality | p. 264 |
| A Modular Method for Proving Convergence | p. 269 |
| Verifying Deadlock Freedom | p. 277 |
| Proving Absence of Runtime Errors | p. 279 |
| Historical Notes | p. 282 |
| Expressibility and Relative Completeness | p. 291 |
| Objective | p. 291 |
| Structure of this Chapter | p. 292 |
| Syntactic Notions | p. 292 |
| Partial Correctness of Syntactic Transition Diagrams | p. 298 |
| Relative Completeness of Floyd's Inductive Assertion Method | p. 300 |
| Relative Completeness of the Method of Owicki & Gries | p. 309 |
| Relative Completeness of the Method of Apt, Francez & de Roever | p. 312 |
| Historical Notes | p. 316 |
| Picture Gallery | p. 319 |
| Compositional Methods based on Assertion Networks | p. 353 |
| Introduction to Compositional Reasoning | p. 354 |
| Motivation | p. 354 |
| Introduction to Part III and to this Chapter | p. 356 |
| Assume-Guarantee-based Reasoning | p. 359 |
| Assumption-Commitment-based Reasoning | p. 361 |
| Rely-Guarantee-based Reasoning | p. 363 |
| Compositional Proof Methods: Synchronous Message Passing | p. 367 |
| Objective and Introduction | p. 367 |
| Structure of the Chapter | p. 368 |
| Top-level Synchronous Message Passing | p. 369 |
| A Compositional Proof Method for Nested Parallelism | p. 379 |
| Assumption-Commitment-based Reasoning | p. 397 |
| Historical Notes | p. 429 |
| Compositional Proof Methods: Shared-Variable Concurrency | p. 438 |
| Introduction and Overview | p. 438 |
| Concurrent Transition Diagrams | p. 439 |
| Top-Level Shared-Variable Concurrency | p. 440 |
| The Rely-Guarantee Method | p. 447 |
| Historical Notes | p. 479 |
| Hoare Logic | p. 487 |
| A Proof System for Sequential Programs Using Hoare Triples | p. 488 |
| Introduction and Overview of Hoare Logics | p. 488 |
| Structure of this Chapter | p. 497 |
| Syntax and Informal Meaning of GCL+ Programs | p. 498 |
| Semantics of GCL+ | p. 501 |
| A Proof System for GCL+ Programs | p. 506 |
| Soundness and Relative Completeness | p. 511 |
| Proof Outlines | p. 517 |
| Alternative Definitions of Proof Outlines | p. 521 |
| Examples of Verification during Program Development | p. 522 |
| Historical Notes | p. 526 |
| A Hoare Logic for Shared-Variable Concurrency | p. 531 |
| Introduction and Overview | p. 531 |
| Syntax and Informal Meaning of SVL Programs | p. 532 |
| Semantics of SVL+ | p. 537 |
| A Proof System for SVL Programs | p. 540 |
| An Extended Example: Concurrent Garbage Collection | p. 563 |
| Completeness of the Owicki & Gries Method | p. 584 |
| A Hoare Logic for Synchronous Message Passing | p. 600 |
| Structure of this Chapter | p. 600 |
| Syntax and Informal Meaning of DML Programs | p. 601 |
| Semantics of DML | p. 606 |
| A Hoare Logic for Synchronous Message Passing | p. 608 |
| Soundness and Relative Completeness of this Hoare Logic | p. 630 |
| Technical Note: Modifications Towards Compositionality | p. 638 |
| Layered Design | p. 653 |
| Transformational Design and Hoare Logic | p. 654 |
| Introduction and Overview | p. 654 |
| Structure of this Chapter | p. 660 |
| Syntax and Informal Meaning of SVL++ Programs | p. 660 |
| The Semantics of SVL++ Programs | p. 662 |
| Partial Orders and Temporal Logic | p. 663 |
| The Communication-Closed-Layers Laws | p. 676 |
| The Two-Phase Commit Protocol | p. 688 |
| Assertion-Based Program Transformations | p. 694 |
| Loop Distribution | p. 696 |
| Set-partitioning Revisited | p. 700 |
| Historical Notes | p. 704 |
| Bibliography | p. 710 |
| Glossary of Symbols | p. 747 |
| Index | p. 761 |
| Table of Contents provided by Ingram. All Rights Reserved. |
