This book provides a structured introduction to the verification of sequen tial and concurrent programs. It thus belongs to the area of programming languages but at the same time it is firmly based on mathematical logic. In logic one usually studies fixed syntactic or semantic objects. This is not necessarily the case in the area of program verification. The objects studied here, namely programs, do not have a standard syntax, their semantics can be defined in many different ways, and several approaches to their verification can be contemplated. These differences lead to various difficult design decisions. Even though we restrict our attention here to one programming style - imperative pro gramming - we are still confronted with a veritable cornucopia of pro gramming constructs from which an appropriate selection has to be made. Having studied some of these constructs separately does not yet imply that we understand their combined effect. This book provides a structural introduction to program verification. Sequential programs in the form of deterministic and nondeterministic programs, and concurrent programs in the form of parallel and distributed programs, are considered within the context of their partial and total correctness. While other books have covered verification and semantics of sequential programs, this is the first book to address verification and semantics of structured concurrent programs. The book is appropriate for either a one- or two-semester introductory course on program verification for upper division of undergraduate studies or graduate students. It can also be used as an introduction to operational semantics. Outlines of possible one-semester courses are presented in the preface of the book. Within these chapters, the authors systematically discuss five classes of programs, concentrating on operational semantics, syntax directed assertional proof systems, soundness proofs of the proof systems, program transformations, correctness proofs of the program transformations, and correctness proofs of a substantial example. Each chapter is developed in a systematic and easy-to-understand manner and closes with a list of exercises. The material presented here draws on work which until now was only available in the form of advanced research publications. A large portion of the material is entirely new. This book provides an introduction to the subject which also will lead to current research problems in the areas considered. Front Matter....Pages i-xvi Front Matter....Pages 1-1 Introduction....Pages 3-19 Preliminaries....Pages 20-53 Front Matter....Pages 55-55 Deterministic Programs....Pages 57-105 Nondeterministic Programs....Pages 106-175 Front Matter....Pages 177-177 Disjoint Parallel Programs....Pages 179-206 Parallel Programs with Shared Variables....Pages 207-266 Parallel Programs with Synchronization....Pages 267-324 Front Matter....Pages 325-325 Distributed Programs....Pages 327-416 Back Matter....Pages 417-444
