Verification of Sequential and Concurrent Programs

by Apt, Krzysztof R.; Boer, Frank S. De; Olderog, Ernst-Rudiger

• ISBN13: 9781848827448
• ISBN10: 184882744X
• Edition: 3rd
• Format: Hardcover
• Copyright: 2009-10-01
• Publisher: Springer-Nature New York Inc

Summary

This widely anticipated third edition provides a systematic exploration of one of the most common approaches to program verification, known as the assertional approach. This approach is applied to deterministic and nondeterministic sequential programs of varying complexity, together with both parallel and distributed concurrent programs. The expanded content also includes coverage of the verification of object-oriented programs. For each class of programs, the authors introduce proof systems for the verification of partial and total correctness, justified formally in corresponding soundness theorems. Case studies supplied throughout the book demonstrate the use of the proof systems and formally verify solutions to classical problems, such as producer/consumer and mutual exclusion. This modern update of a classic, reader-friendly textbook is perfect for an introductory course on program verification for advanced undergraduate or graduate students. Outlines for possible courses are suggested in the Preface.

Table of Contents

Endorsements	p. v
Foreword	p. vii
Preface	p. ix
Outlines of One-semester Courses	p. xiv
In the Beginning
Introduction	p. 3
An Example of a Concurrent Program	p. 4
Solution 1	p. 4
Solution 2	p. 5
Solution 3	p. 6
Solution 4	p. 8
Solution 5	p. 9
Solution 6	p. 10
Program Correctness	p. 11
Structure of this Book	p. 13
Automating Program Verification	p. 16
Assertional Methods in Practice	p. 17
Preliminaries	p. 19
Mathematical Notation	p. 21
Sets	p. 21
Tuples	p. 22
Relations	p. 23
Functions	p. 23
Sequences	p. 24
Strings	p. 25
Proofs	p. 26
Induction	p. 27
Grammars	p. 29
Typed Expressions	p. 29
Types	p. 29
Variables	p. 30
Constants	p. 30
Expressions	p. 31
Subscripted Variables	p. 32
Semantics of Expressions	p. 32
Fixed Structure	p. 33
States	p. 34
Definition of the Semantics	p. 35
Updates of States	p. 36
Formal Proof Systems	p. 38
Assertions	p. 39
Semantics of Assertions	p. 41
Substitution	p. 42
Substitution Lemma	p. 47
Exercises	p. 50
Bibliographic Remarks	p. 51
Deterministic Programs
while Programs	p. 55
Syntax	p. 57
Semantics	p. 58
Properties of Semantics	p. 62
Verification	p. 63
Partial Correctness	p. 65
Total Correctness	p. 70
Decomposition	p. 73
Soundness	p. 73
Proof Outlines	p. 79
Partial Correctness	p. 79
Total Correctness	p. 83
Completeness	p. 85
Parallel Assignment	p. 91
Failure Statement	p. 94
Auxiliary Axioms and Rules	p. 97
Case Study: Partitioning an Array	p. 99
Systematic Development of Correct Programs	p. 113
Summation Problem	p. 115
Case Study: Minimum-Sum Section Problem	p. 116
Exercises	p. 121
Bibliographic Remarks	p. 124
Recursive Programs	p. 127
Syntax	p. 129
Semantics	p. 129
Properties of the Semantics	p. 131
Verification	p. 132
Partial Correctness	p. 132
Total Correctness	p. 134
Decomposition	p. 137
Discussion	p. 138
Soundness	p. 139
Case Study: Binary Search	p. 144
Partial Correctness	p. 145
Total Correctness	p. 147
Exercises	p. 149
Bibliographic Remarks	p. 150
Recursive Programs with Parameters	p. 151
Syntax	p. 152
Semantics	p. 154
Verification	p. 157
Partial Correctness: Non-recursive Procedures	p. 158
Partial Correctness: Recursive Procedures	p. 162
Modularity	p. 165
Total Correctness	p. 165
Soundness	p. 167
Case Study: Quicksort	p. 172
Formal Problem Specification	p. 173
Properties of Partition	p. 173
Auxiliary Proof: Permutation Property	p. 174
Auxiliary Proof: Sorting Property	p. 175
Total Correctness	p. 180
Exercises	p. 182
Bibliographic Remarks	p. 182
Object-Oriented Programs	p. 185
Syntax	p. 187
Local Expressions	p. 187
Statements and Programs	p. 188
Semantics	p. 192
Semantics of Local Expressions	p. 192
Updates of States	p. 194
Semantics of Statements and Programs	p. 195
Assertions	p. 197
Substitution	p. 199
Verification	p. 200
Partial Correctness	p. 201
Total Correctness	p. 204
Adding Parameters	p. 206
Semantics	p. 207
Partial Correctness	p. 208
Total Correctness	p. 210
Transformation of Object-Oriented Programs	p. 211
Soundness	p. 214
Object Creation	p. 217
Semantics	p. 218
Assertions	p. 219
Verification	p. 223
Soundness	p. 225
Case Study: Zero Search in Linked List	p. 226
Partial Correctness	p. 226
Total Correctness	p. 229
Case Study: Insertion into a Linked List	p. 232
Exercises	p. 238
Bibliographic Remarks	p. 240
Parallel Programs
Disjoint Parallel Programs	p. 245
Syntax	p. 247
Semantics	p. 248
Determinism	p. 249
Sequentialization	p. 252
Verification	p. 253
Parallel Composition	p. 254
Auxiliary Variables	p. 256
Soundness	p. 259
Case Study: Find Positive Element	p. 261
Exercises	p. 264
Bibliographic Remarks	p. 266
Parallel Programs with Shared Variables	p. 267
Access to Shared Variables	p. 269
Syntax	p. 270
Semantics	p. 271
Atomicity	p. 272
Verification: Partial Correctness	p. 274
Component Programs	p. 274
No Compositionality of Input/Output Behavior	p. 275
Parallel Composition: Interference Freedom	p. 276
Auxiliary Variables Needed	p. 279
Soundness	p. 282
Verification: Total Correctness	p. 284
Component Programs	p. 284
Parallel Composition: Interference Freedom	p. 286
Soundness	p. 288
Discussion	p. 289
Case Study: Find Positive Element More Quickly	p. 291
Allowing More Points of Interference	p. 294
Case Study: Parallel Zero Search	p. 299
Simplifying the program	p. 299
Proving partial correctness	p. 300
Exercises	p. 303
Bibliographic Remarks	p. 305
Parallel Programs with Synchronization	p. 307
Syntax	p. 309
Semantics	p. 310
Verification	p. 311
Partial Correctness	p. 311
Weak Total Correctness	p. 313
Total Correctness	p. 314
Soundness	p. 316
Case Study: Producer/Consumer Problem	p. 319
Case Study: The Mutual Exclusion Problem	p. 324
Problem Formulation	p. 324
Verification	p. 326
A Busy Wait Solution	p. 327
A Solution Using Semaphores	p. 331
Allowing More Points of Interference	p. 334
Case Study: Synchronized Zero Search	p. 335
Simplifying the Program	p. 336
Decomposing Total Correctness	p. 337
Proving Termination	p. 337
Proving Partial Correctness	p. 342
Exercises	p. 344
Bibliographic Remarks	p. 345
Nondeterministic and Distributed Programs
Nondeterministic Programs	p. 349
Syntax	p. 351
Semantics	p. 352
Properties of Semantics	p. 353
Why Are Nondeterministic Programs Useful?	p. 354
Symmetry	p. 355
Nondeterminism	p. 355
Failures	p. 356
Modeling Concurrency	p. 356
Verification	p. 357
Partial Correctness	p. 357
Total Correctness	p. 357
Soundness	p. 359
Case Study: The Welfare Crook Problem	p. 360
Transformation of Parallel Programs	p. 363
Exercises	p. 368
Bibliographic Remarks	p. 370
Distributed Programs	p. 373
Syntax	p. 375
Sequential Processes	p. 375
Distributed Programs	p. 376
Semantics	p. 380
Transformation into Nondeterministic Programs	p. 382
Semantic Relationship Between S and T(S)	p. 382
Proof of the Sequentialization Theorem	p. 385
Verification	p. 390
Partial Correctness	p. 390
Weak Total Correctness	p. 391
Total Correctness	p. 391
Proof Systems	p. 392
Soundness	p. 393
Case Study: A Transmission Problem	p. 396
Decomposing Total Correctness	p. 397
Proving Partial Correctness	p. 397
Proving Absence of Failures and of Divergence	p. 399
Proving Deadlock Freedom	p. 400
Exercises	p. 402
Bibliographic Remarks	p. 405
Fairness	p. 407
The Concept of Fairness	p. 409
Selections and Runs	p. 410
Fair Nondeterminism Semantics	p. 412
Transformational Semantics	p. 413
Well-Founded Structures	p. 413
Random Assignment	p. 414
Semantics	p. 415
Verification	p. 415
Schedulers	p. 419
The Scheduler FAIR	p. 421
The Scheduler RORO	p. 424
The Scheduler QUEUE	p. 426
Transformation	p. 427
Verification	p. 430
Total Correctness	p. 430
Soundness	p. 438
Case Study: Zero Search	p. 442
Case Study: Asynchronous Fixed Point Computation	p. 446
Exercises	p. 452
Bibliographic Remarks	p. 455
Semantics	p. 457
Axioms and Proof Rules	p. 459
Proof Systems	p. 471
Proof Outlines	p. 475
References	p. 477
Index	p. 491
Author Index	p. 497
Symbol Index	p. 501
Table of Contents provided by Ingram. All Rights Reserved.