3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 6
Текст из файла (страница 6)
The design of the final solution proceededthrough a disquieting series of trials and errors. From this experience it shouldbe clear that an informal justification of programs constructed in such amanner is not sufficient. Instead, one needs a systematic approach to provingcorrectness of programs.Correctness means that certain desirable program properties hold. In thecase of sequential programs, where a control resides at each moment in onlyone point, these properties usually are:1.
Partial correctness, that is, whenever a result is delivered it is correctw.r.t. the task to be solved by the program. For example, upon termination of a sorting program, the input should indeed be sorted. Partialmeans that the program is not guaranteed to terminate and thus delivera result at all.2. Termination. For example, a sorting program should always terminate.3.
Absence of failures. For example, there should be no division by zero andno overflow.In the case of concurrent programs, where control can reside at the sametime in several control points, the above properties are much more difficultto establish. Moreover, as observed before, we are then also interested inestablishing:4. Interference freedom, that is, no component of a parallel program canmanipulate in an undesirable way the variables shared with another component.5. Deadlock freedom, that is, a parallel program does not end up in a situation where all nonterminated components are waiting indefinitely for acondition to become true.121 Introduction6.
Correctness under the fairness assumption. For example, the parallel program ZERO--3 solves the zero search problem only under the assumptionof fairness.A number of approaches to program verification have been proposed andused in the literature. The most common of them is based on operationalreasoning, which is the way we reasoned about the correctness of Solution6. This approach consists of an analysis in terms of the execution sequencesof the given program. For this purpose, an informal understanding of theprogram semantics is used.
While this analysis is often successful in the caseof sequential programs, it is much less so in the case of concurrent programs.The number of possible execution sequences is often forbiddingly large andit is all too easy to overlook one.In this book we pursue a different approach based on axiomatic reasoning.With this approach, we first need a language that makes it possible to express or specify the relevant program properties. We choose here the languageof predicate logic consisting of certain well-formed formulas. Such formulasserve as so-called assertions expressing desirable program states.
From logicwe also use the concept of a proof system consisting of axioms and proofrules that allow us to formally prove that a given program satisfies the desired properties. Such a proof will proceed in a syntax-directed manner byinduction on the structure of the program.The origins of this approach to program verification can be traced backto Turing [1949], but the first constructive efforts should be attributed toFloyd [1967a] and Hoare [1969]. Floyd proposed an axiomatic method forthe verification of flowcharts, and Hoare developed this method further toa syntax-directed approach dealing with while programs.
Hoare’s approachreceived a great deal of attention, and many Hoare-style proof systems dealingwith various programming constructs have been proposed since then. In 1976and 1977, this approach was extended to parallel programs by Owicki andGries [1976a,1976b] and Lamport [1977], and in 1980 and 1981 to distributedprograms by Apt, Francez and de Roever [1980] and Levin and Gries [1981].In 1991 an assertional proof system was introduced by de Boer [1991a] for aparallel object-oriented language called POOL, developed by America [1987].In our book we present a systematic account of the axiomatic approachto program verification. It should be noted that the axiomatic approach asdescribed in the above articles has several limitations:(1) the proof rules are designed only for the a posteriori verification of existingprograms, not for their systematic development;(2) the proof rules reflect only the input/output behavior of programs, notproperties of their finite or infinite executions as they occur, for example,in operating systems;(3) the proof rules cannot deal with fairness.Overcoming limitation (1) has motivated a large research activity on systematic development of programs together with their correctness proofs, ini-1.3 Structure of this Book13tiated by Dijkstra [1976] and extended by many others: see, for example, thebooks by Gries [1981], Backhouse [1986], Kaldewaij [1990], Morgan [1994],Back and von Wright [2008], and for parallel programs by Feijen and vanGasteren [1999] and Misra [2001].The fundamentals of program development are now well understood forsequential programs; we indicate them in Chapters 3 and 10 of this book.Interestingly, the proof rules suggested for the a posteriori verification ofsequential programs remain useful for formulating strategies for program development.Another approach aims at higher-level system development.
The development starts with an abstract system model which is stepwise refined toa detailed model that can form a basis for a correct program. An exampleof such a formal method for modelling and analysis at the system level isEvent-B, see Abrial and Hallerstede [2007].To overcome limitations (2) and (3) one can use the approach based ontemporal logic introduced by Pnueli [1977]. Using temporal logic more general program properties than input/output behavior can be expressed, forexample so-called liveness properties, and the fairness assumption can behandled. However, this approach calls for use of location counters or labels,necessitating an extension of the assertion language and making reconciliation with structured reasoning about programs difficult but not impossible.We do not treat this approach here but refer the reader instead to the booksby Manna and Pnueli [1991,1995].
For dealing with fairness we use transformations based on explicit schedulers.1.3 Structure of this BookThis book presents an approach to program verification based on Hoare-styleproof rules and on program transformations. It is organized around severalclasses of sequential and concurrent programs. This structure enables us toexplain program verification in an incremental fashion and to have fine-tunedverification methods for each class.For the classes of programs we use the following terminology.
In a sequential program the control resides at each moment in only one point. Thesimplest type of sequential program is the deterministic program, where ateach moment the instruction to be executed next is uniquely determined. In aconcurrent program the control can reside at the same time at several controlpoints. Usually, the components of a concurrent program have to exchangesome information in order to achieve a certain common goal. This exchange isknown as communication.
Depending on the mode of communication, we distinguish two types of concurrent programs: parallel programs and distributedprograms. In a parallel program the components communicate by means ofshared variables. The concurrent programs discussed in Section 1.1 are of this141 Introductiontype. Distributed programs are concurrent programs with disjoint componentsthat communicate by explicit message passing.For each class of programs considered in this book the presentation proceeds in a uniform way.
We start with its syntax and then present an operational semantics in the style of Hennessy and Plotkin [1979] and Plotkin[1981,2004]. Next, we introduce Hoare-style proof rules allowing us to verifythe partial and total correctness of programs. Intuitively, partial correctnessmeans delivering correct results; total correctness additionally guarantees termination. Soundness of proposed proof systems is shown on the basis of theprogram semantics. Throughout this book correctness proofs are presentedin the form of proof outlines as proposed by Owicki and Gries [1976a]. Casestudies provide extensive examples of program verification with the proposedproof systems. For some program classes additional topics are discussed, forexample, completeness of the proof systems or program transformations intoother classes of programs.
Each of the subsequent chapters ends with a seriesof exercises and bibliographic remarks.In Chapter 2 we explain the basic notions used in this book to describesyntax, semantics and proof rules of the various program classes.In Chapter 3 we study a simple class of deterministic programs, usually called while programs. These programs form the backbone for all otherprogram classes studied in this book. The verification method explained inthis chapter relies on the use of invariants and bound functions, and is a prerequisite for all subsequent chapters.
We also deal with completeness of theproposed proof systems. Finally, we discuss Dijkstra’s approach [1976] to asystematic program development. It is based on reusing the proof rules in asuitable way.In Chapter 4 we extend the class of programs studied in Chapter 3 byrecursive procedures without parameters. Verifying such recursive programsmakes use of proofs from assumptions (about recursive procedure calls) thatare discharges later on (when the procedure body is considered).In Chapter 5 this class is extended by call-by-value parameters of therecursive procedures.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
