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), страница 7

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 an appropriatesemantic 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: objects possess (and encapsulate) their own local variables, objects interact via methodcalls, and objects can be dynamically created.In Chapter 7 we study the simplest form of parallel programs, so-calleddisjoint parallel programs. “Disjoint” means that component programs haveonly reading access to shared variables. As first noted in Hoare [1975], thisrestriction leads to a very simple verification rule.

Disjoint parallel programsprovide a good starting point for understanding general parallel programs1.3 Structure of this Book15considered in Chapters 8 and 9, as well as distributed programs studied inChapter 11.In Chapter 8 we study parallel programs that permit unrestricted use ofshared variables. The semantics of such parallel programs depends on whichparts of the components are considered atomic, that is, not interruptable bythe execution of other components. Verification of such programs is based onthe test of interference freedom due to Owicki and Gries [1976a].

In general,this test is very laborious. However, we also present program transformationsdue to Lipton [1975] allowing us to enlarge the atomic regions within thecomponent programs and thus reduce the number of interference tests.In Chapter 9 we add to the programs of Chapter 8 a programming construct for synchronization. Since the execution of these programs can nowend in a deadlock, their verification also includes a test of deadlock freedom.As typical examples of parallel programs with shared variables and synchronization, we consider solutions to the producer/consumer problem and themutual exclusion problem, which we prove to be correct.In Chapter 10 we return to sequential programs but this time tonondeterministic ones in the form of guarded commands due to Dijkstra[1975,1976]. These programs can be seen as a stepping stone towards distributed programs considered in Chapter 11.

We extend here Dijkstra’s approach to program development to the guarded commands language, theclass of programs for which this method was originally proposed. Finally,we explain how parallel programs can be transformed into equivalent nondeterministic ones although at the price of introducing additional controlvariables.In Chapter 11 we study a class of distributed programs that is a subset ofCommunicating Sequential Processes (CSP) of Hoare [1978,1985]. CSP is thekernel of the programming language OCCAM, see INMOS [1984], developedfor programming distributed transputer systems. We show that programs inthis subset can be transformed into semantically equivalent nondeterministicprograms without extra control variables.

Based on this program transformation we develop proof techniques for distributed programs due to Apt [1986].Finally, in Chapter 12 we consider the issue of fairness. For the sakeof simplicity we limit ourselves to the study of fairness for nondeterministicprograms, as studied in Chapter 10. Our approach, due to Apt and Olderog[1983], again employs program transformations. More specifically, the proofrule allowing us to deal with nondeterministic programs under the assumptionof fairness is developed by means of a program transformation that reducesfair nondeterminism to ordinary nondeterminism.161 Introduction1.4 Automating Program VerificationIn this book we present program verification as an activity requiring insightand calculation.

It is meaningful to ask whether program verification cannotbe carried out automatically. Why not feed a program and its specificationinto a computer and wait for an answer? Unfortunately, the theory of computability tells us that fully automatic verification of program properties isin general an undecidable problem, and therefore impossible to implement.Nevertheless, automating program verification is a topic of intense research.First of all, for the special case of finite-state systems represented by programs that manipulate only variables ranging over finite data types, fullyautomatic program verification is indeed possible. Queille and Sifakis [1981]and Emerson and Clarke [1982] were the first to develop tools that automatically check whether such programs satisfy specifications written in anassertion language based on temporal logic.

In the terminology of logic itis checked whether the program is a model of the specification. Hence thisapproach is called model checking. Essentially, model checking rests on algrorithms for exploring the reachable state space of a program. For furtherdetails we refer to the books by Clarke, Grumberg, and Peled [1999], andby Baier and Katoen [2008]. The book edited by Grumberg and Veith [2008]surveys the achievements of model checking in the past 25 years.The current problems in model checking lie in the so-called state spaceexplosion that occurs if many sequential components with finite state spacesare composed in a concurrent program. Moreover, model checking is alsoconsidering infinite-state systems, for instance represented by programs wheresome variables range over infinite data types. One line of attack is here toapply the concept of abstract interpretation due to Cousot and Cousot [1977a]in order to reduce the original problem to a size where it can be automaticallysolved.

Then of course the question is whether the answer for the abstractsystem implies the corresponding answer for the concrete system. To solvethis question the approach of abstraction refinement is often pursued wherebytoo coarse abstractions are successively refined, see Clarke et al. [2003] andBall et al. [2002].Related to model checking is the approach of program analysis that aimsat verifying restricted program properties automatically, for instance whethera variable has a certain value at a given control point, see Nielson, Nielsonand Hankin [2004]. Program analysis employs static techniques for computingreliable approximate information about the dynamic behavior of programs.For example, shape analysis is used to establish properties of programs withpointer structures, see Sagiv, Reps and Wilhelm [2002].Another attempt to conquer the problem of state space explosion solutionis to combine automatic program verification with the application of proofrules controlled by a human user —see for example Burch et al.

[1992] andBouajjani et al. [1992]. This shows that even in the context of automatic1.5 Assertional Methods in Practice17program verification a good knowledge of axiomatic verification techniquesas explained in this book is of importance.A second, more general approach to automation is deductive verification.It attempts to verify programs by proofs carried out by means of interactivetheorem provers instead of state space exploration and thus does not needfinite-state abstractions. Deductive verification automates the axiomatic approach to program verification presented in this book. Well-known are theprovers Isabelle/HOL, see Nipkow, Paulson and Wenzel [2002], and PVS, seeOwre and Shankar [2003], both based on higher-order logic.

To apply theseprovers to program verification both the program semantics and the proofsystems are embedded into higher-order logic and then suitable tactics areformalized to reduce the amount of human interaction in the application ofthe proof rules. As far as possible decision procedures are invoked to checkautomatically logical implications needed in the premises of the proof rules.Other theorem provers are based on dynamic logic, see Harel, Kozenand Tiuryn [2000], which extends Hoare’s logic for sequential programs bymodal operators and is closed under logical operators. We mention here theprovers KeY that is used to the verification of object-oriented software writtenin Java, see the book edited by Beckert, Hähnle and Schmitt [2007], KIV(Karlsruhe Interactive Verifier, see Balser et al.

[2000]), and VSE (VerificationSupport Environment, see Stephan et al. [2005]).1.5 Assertional Methods in PracticeTo what extent do the methods of program verification influence today’spractice of correct software construction? Hoare [1996] noted that currentprogramming paradigms build to a large extent on research that started 20years ago. For example, we can observe that the notion of an assertion andthe corresponding programming methods appeared in practice only in recentyears.Meyer [1997] introduced the paradigm of design by contract for the objectoriented programming language Eiffel.

A contract is a specification in theform of assertions (class invariants and pre- and postconditions for eachmethod). The contract is agreed upon before an implementation is developed that satisfies this contract.Design by contract has been carried over to the object-oriented programming language Java by Leavens et al. [2005]. The contracts are written inthe Java Modeling Language JML, which allows the user to specify so-calledrich interfaces of classes and methods that are not yet implemented.

Besidesassertions, JML also incorporates the concept of abstract data specified withthe help of so-called model variables that have to be realized by the implementation using data refinement.181 IntroductionChecking whether an implementation (a program) satisfies a contract isdone either by formal verification using proof rules (as outlined above) or —ina limited way— at runtime. The second approach requires that the assertionsin the contracts are Boolean expressions. Then during each particular run ofthe implementation it is checked automatically whether along this run allassertions of the contract are satisfied.

If an assertion is encountered that isnot satisfied, a failure or exception is raised.As an example of a successful application of verification techniques tospecific programming languages let us mention ESC/Java (Extended StaticChecker for Java) which supports the (semi-)automated verification of annotated Java programs, see Flanagan et al. [2002]. Another example involvesJava Card, a subset of Java dedicated for the programming of Smart Cardsthe programs of which are verified using interactive theorem provers, see vanden Berg, Jacobs and Poll [2001], and Beckert, Hähnle and Schmitt [2007].2 Preliminaries2.12.22.32.42.52.62.72.82.92.10IMathematical Notation . .