3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010).pdf)

Krzysztof R. AptFrank S. de BoerErnst-Rüdiger OlderogVerification ofSequential and ConcurrentProgramsThird, Extended EditionSpringerPrefaceCOMPUTER PROGRAMS ARE by now indispensable parts of systems that we use or rely on in our daily lives. Numerous examples include booking terminals in travel agencies, automatic tellermachines, ever more sophisticated services based on telecommunication, signaling systems for cars and trains, luggage handling systems at airports orautomatic pilots in airplanes.For the customers of travel agencies and banks and for the passengers oftrains and airplanes the proper functioning and safety of these systems is ofparamount importance.

Money orders should reflect the right bank accountsand airplanes should stay on the desired route. Therefore the underlyingcomputer programs should work correctly; that is they should satisfy theirrequirements. A challenge for computer science is to develop methods thatensure program correctness.Common to the applications mentioned above is that the computer programs have to coordinate a number of system components that can workconcurrently, for example the terminals in the individual travel agencies accessing a central database or the sensors and signals used in a distributedrailway signaling system.

So to be able to verify such programs we need tohave at our disposal methods that allow us to deal with correctness of concurrent programs, as well.Structure of This BookThe aim of this book is to provide a systematic exposition of one of themost common approaches to program verification. This approach is usuallycalled assertional, because it relies on the use of assertions that are attachedto program control points.

Starting from a simple class of sequential pro-ixxPrefacegrams, known as while programs, we proceed in a systematic manner in twodirections:• to more complex classes of sequential programs including recursive procedures and objects, and• to concurrent programs, both parallel and distributed.We consider here sequential programs in the form of deterministic andnondeterministic programs, and concurrent programs in the form of parallel and distributed programs. Deterministic programs cover while programs,recursive programs, and a simple class of object-oriented programs.

Nondeterministic programs are used to analyze concurrent programs and the conceptof fairness by means of program transformations. Parallel programs consistof several sequential components that can access shared memory. By contrast, distributed programs consist of components with local memory thatcan communicate only by sending and receiving messages.For each of these classes of programs their input/output behavior in thesense of so-called partial and total correctness is studied. For the verificationof these correctness properties an axiomatic approach involving assertions isused.

This approach was initiated by Hoare in 1969 for deterministic programs and extended by various researchers to other classes of programs. It iscombined here with the use of program transformations.For each class of programs a uniform presentation is provided. After defining the syntax we introduce a structured operational semantics as originallyproposed by Hennessy and Plotkin in 1979 and further developed by Plotkinin 1981. Then proof systems for the verification of partial and total correctness are introduced, which are formally justified in the correspondingsoundness theorems.The use of these proof systems is demonstrated with the help of case studies. In particular, solutions to classical problems such as producer/consumerand mutual exclusion are formally verified.

Each chapter concludes with alist of exercises and bibliographic remarks.The exposition assumes elementary knowledge of programming languagesand logic. Therefore this book belongs to the area of programming languagesbut at the same time it is firmly based on mathematical logic.

All prerequisitesare provided in the preparatory Chapter 2 of Part I.In Part II of the book we study deterministic programs. In Chapter 3Hoare’s approach to program verification is explained for while programs.Next, we move to the more ambitious structuring concepts of recursive andobject-oriented programs. First, parameterless recursive procedures are studied in Chapter 4, and then call-by-value parameters are added in Chapter 5. These two chapters are taken as preparations to study a class ofobject-oriented programs in Chapter 6. This chapter is based on the workof the second author initiated in 1990, but the presentation is entirely new.In Part III of the book we study parallel programs with shared variables.Since these are much more difficult to deal with than sequential programs,Prefacexithey are introduced in a stepwise manner in Chapters 7, 8, and 9.

We baseour presentation on the approach by Owicki and Gries originally proposed in1976 and on an extension of it by the authors dealing with total correctness.In Part IV we turn to nondeterministic and distributed programs. Nondeterministic sequential programs are studied in Chapter 10. The presentationis based on the work of Dijkstra from 1976 and Gries from 1981. The studyof this class of programs also serves as a preparation for dealing with distributed programs in Chapter 11. The verification method presented thereis based on a transformation of distributed programs into nondeterministicones proposed by the first author in 1986.

In Chapter 12 the issue of fairnessis studied in the framework of nondeterministic programs. The approach isbased on the method of explicit schedulers developed by the first and thirdauthors in 1983.Teaching from This BookThis book is appropriate for either a one- or two-semester introductory courseon program verification for upper division undergraduate studies or for graduate studies.In the first lecture the zero search example in Chapter 1 should be discussed.

This example demonstrates which subtle errors can arise during thedesign of parallel programs. Next we recommend moving on to Chapter 3on while programs and before each of the sections on syntax, semantics andverification, to refer to the corresponding sections of the preparatory Chapter 2.After Chapter 3 there are three natural alternatives to continue. The firstalternative is to proceed with more ambitious classes of sequential programs,i.e., recursive programs in Chapters 4 and 5 and then object-oriented programs in Chapter 6. The second alternative is to proceed immediately toparallel programs in Chapters 7, 8, and 9. The third alternative is to moveimmediately to nondeterministic programs in Chapter 10 and then to distributed programs in Chapter 11.

We remark that one section of Chapter 10can be studied only after the chapters on parallel programs.Chapter 12 on fairness covers a more advanced topic and can be usedduring specialized seminars. Of course, it is also possible to follow the chaptersin the sequential order as they are presented in the book.This text may also be used as an introduction to operational semantics.We present below outlines of possible one-semester courses that can be taughtusing this book. The dependencies of the chapters are shown in Fig.

0.1.xiiPrefaceFig. 0.1 Dependencies of chapters. In Chapter 10 only Section 10.6 depends onChapter 9.Changes in the Third EditionThe present, third edition of this book comes with a new co-author, FrankS. de Boer, and with an additional topic that for many years has been at theheart of his research: verification of object-oriented programs. Since this isa notoriously difficult topic, we approach it in a stepwise manner and in asetting where the notational complexity is kept at a minimum. This designdecision has led us to add three new chapters to our book.• In Chapter 4 we introduce a class of recursive programs that extends deterministic programs by parameterless procedures.

Verifying such programsmakes use of proofs from assumptions (about calls of recursive procedures)that are discharged later on.• In Chapter 5 this class is extended to the recursive procedures with call-byvalue parameters. Semantically, this necessitates the concept of a stack forstoring the values of the actual parameters of recursively called procedures.We capture this concept by using a block statement and a correspondingsemantic transition rule that models the desired stack behavior implicitly.• In Chapter 6 object-oriented programs are studied in a minimal settingwhere we focus on the following main characteristics of objects: they pos-Prefacexiiisess (and encapsulate) their own local variables and interact via methodcalls, and objects can be dynamically created.To integrate these new chapters into the original text, we made variouschanges in the preceding Chapters 2 and 3.

For example, in Chapter 3 parallelassignments and failure statements are introduced, and a correctness proofof a program for partitioning an array is given as a preparation for the casestudy of the Quicksort algorithm in Chapter 5. Also, in Chapter 10 thetransformation of parallel programs into nondeterministic programs is nowdefined in a formal way. Also the references have been updated.AcknowledgmentsThe authors of this book have collaborated, often together with other colleagues, on the topic of program verification since 1979.