3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 24
Текст из файла (страница 24)
Consider the programS ≡ z := x; x := y; y := z.Prove the correctness formula1223 while Programs{x = x0 ∧ y = y0 } S {x = y0 ∧ y = x0 }in the system PW. What is the intuitive meaning of this formula?3.6. Prove the Soundness Theorem 3.6.3.7. The following “forward” assignment axiom was proposed in Floyd[1967a] for the case of simple variables and in de Bakker [1980] for the caseof subscripted variables:{p} u := t {∃y : (p[u := y] ∧ u = t[u := y])}.(i) Prove its truth. Show that it can be proved in the proof system PW.Show that the assignment axiom can be proved from the above axiomusing the consequence rule.(ii) Show that in general the simple “assignment axiom”{true} u := t {u = t}is not true.
Investigate under which conditions on u and t it becomestrue.3.8. Prove the correctness formula{true} while true do x := x − 1 od {false}in the system PW. Examine where an attempt at proving the same formulain the system TW fails.3.9. Consider the following program S computing the product of two naturalnumbers x and y:S ≡ prod := 0; count := y;while count > 0 doprod := prod + x;count := count − 1od,where x, y, prod, count are integer variables.(i) Exhibit the computation of S starting in a proper state σ with σ(x) = 4and σ(y) = 3.(ii) Prove the correctness formula{x ≥ 0 ∧ y ≥ 0} S {prod = x · y}in the system TW.(iii) State and prove a correctness formula about S expressing that the execution of S does not change the values of the variables x and y.3.12 Exercises123(iv) Determine the weakest precondition wp(S, true).3.10. Fibonacci number Fn is defined inductively as follows:F0 = 0,F1 = 1,Fn = Fn−1 + Fn−2 for n ≥ 2.Extend the assertion language by a function symbol fib of type integer →integer such that for n ≥ 0 the expression f ib(n) denotes Fn .(i) Prove the correctness formula{n ≥ 0} S {x = f ib(n)},whereS ≡ x := 0; y := 1; count := n;while count > 0 doh := y; y := x + y; x := h;count := count − 1odand x, y, n, h, count are all integer variables.(ii) Let a be an array of type integer → integer.
Construct awhile program S ′ with n 6∈ var(S ′ ) such that{n ≥ 0} S ′ {∀(0 ≤ k ≤ n) : a[k] = f ib(k)}is true in the sense of total correctness. Prove this correctness formulain the system TW.3.11. Recall thatif B then S fi ≡ if B then S else skip fi.Show that the following proof rule is sound for partial correctness:{p ∧ B} S {q}, p ∧ ¬B → q{p} if B then S fi {q}3.12. For while programs S and Boolean conditions B let the repeat-loopbe defined as follows:repeat S until B ≡ S; while ¬B do S od.(i) Give the transition axioms or rules specifying the operational semanticsof the repeat-loop.1243 while Programs(ii) Show that the following proof rule is sound for partial correctness:{p} S {q}, q ∧ ¬B → p.{p} repeat S until B {q ∧ B}Give a sound proof rule for total correctness of repeat-loops.(iii) Prove thatN [[repeat repeat S until B1 until B2 ]]= N [[repeat S until B1 ∧ B2 ]].3.13.
Suppose that< S, σ > →∗ < R, τ >,where R 6≡ E. Prove that R ≡ at(T, S) for a subprogram T of S.Hint. Prove by induction on the length of computation that R is a sequentialcomposition of subprograms of S.3.14. Consider the program DIV of Example 3.4 and the assertionq ≡ quo · y + rem = x ∧ 0 ≤ rem < y.Determine the preconditions wlp(DIV, q) and wp(DIV, q).3.15. Prove the Weakest Liberal Precondition Lemma 3.5.Hint.
For (ii) use the Substitution Lemma 2.4.3.16. Prove the Weakest Precondition Lemma 3.6.Hint. For (ii) use the Substitution Lemma 2.4.3.17. Prove the Soundness Theorem 3.7.3.13 Bibliographic RemarksIn this chapter we studied only the simplest class of deterministic programs,namely while programs. This class is the kernel of imperative programminglanguages; in this book it serves as the starting point for investigating recursive, object-oriented, parallel and distributed programs.The approach presented here is usually called Hoare’s logic. It has beensuccessfully extended, in literally hundreds of papers, to handle other programming constructs. The survey paper Apt [1981] should help as a guide tothe history of the first ten years in this vast domain.
The history of programverification is traced in Jones [1992].A reader who is interested in a more detailed treatment of the subject isadvised to read de Bakker [1980], Reynolds [1981], Tucker and Zucker [1988],and/or Nielson and Nielson [2007]. Besides Hoare’s logic other approaches to3.13 Bibliographic Remarks125the verification of while programs also have been developed, for example, onebased on denotational semantics.
An introduction to this approach can befound in Loeckx and Sieber [1987]. This book also provides further pointersto the early literature.The assignment axiom for simple variables is due to Hoare [1969] and forsubscripted variables due to de Bakker [1980]. Different axioms for assignment to subscripted variables are given in Hoare and Wirth [1973], Gries[1978] and Apt [1981]. The composition rule, loop rule and consequence rulesare due to Hoare [1969]. The conditional rule is due to Lauer [1971] wherealso the first soundness proof of (an extension of) the proof system PW isgiven. The loop II rule is motivated by Dijkstra [1982, pages 217–219].The parallel assignment and the failure statements are from Dijkstra[1975].
The failure statement is a special case of the alternative commandthere considered and which we shall study in Chapter 10.The invariance axiom and conjunction rule are due to Gorelick [1975] andthe invariance rule and the ∃-introduction rule are essentially due to Harel[1979].Completeness of the proof system PW is a special case of a completenessresult due to Cook [1978]. The completeness proof of the proof system TWis a modification of an analogous proof by Harel [1979]. In our approach onlyone fixed interpretation of the assertion language is considered.
This is notthe case in Cook [1978] and Harel [1979] where the completeness theoremsrefer to a class of interpretations.Clarke showed in [1979] that for deterministic programs with a powerful ALGOL-like procedure mechanism it is impossible to obtain a completeHoare-style proof system even if —different from this book— only logicalstructures with finite data domains are considered. For more details see Section 5.6.In Zwiers [1989] the auxiliary rules presented in Section 3.8 are calledadaptation rules.
The reason for their name is that they allow us to adapt agiven correctness formula about a program to other pre- and postconditions.Adaptation rules are independent of the syntactic structure of the programs.Hence they can be used to reason about identifiers ranging over programs.Such identifiers appear in the treatment of recursion and in the derivationof programs from specifications. The name “adaptation rule” goes back toHoare [1971a].The program P ART for partitioning an array in Section 3.9 representsthe body of the procedure Partition inside the recursive program Quicksortinvented by Hoare [1961a,1962] (see Chapter 5). Partial correctness of Partition is shown in Foley and Hoare [1971]. An informal proof of terminationof Partition is given in Hoare [1971b] as part of the proof of the programFind by Hoare [1961b].
In Filliâtre [2007] this informal correctness proof isformalized and certified using the interactive theorem prover Coq. Filliâtrefollows Hoare’s proof as closely as possible though does not explain whichproof rules are used. He points out that two assertions used in Hoare [1971b]1263 while Programsare not invariants of the outer loop of Partition but hold only in certainparts of the loop. This explains why our correctness proof of P ART is morecomplicated than the informal argument given in Hoare [1971b]. Also ourbound functions used to show the termination property T are more elaborate than in Hoare [1971b] because the invariants should imply that they arenon-negative. These bound functions are (modulo an offset of 1) exactly asin Filliâtre [2007].The systematic development of correct programs was first described in thebook by Dijkstra [1976].
The approach has been further explained in Gries[1981]. Both Dijkstra and Gries base their work on program developmenton a class of nondeterministic programs called guarded commands which arestudied in Chapter 10.4 Recursive Programs4.14.24.34.44.54.6WSyntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Semantics . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Case Study: Binary Search . . . . . . . . . . . . . . . . . . . . . . . . . . .Exercises . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . .Bibliographic Remarks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .129129132144149150HILE PROGRAMS, DISCUSSED in the previous chapter, are ofcourse extremely limited. Focusing on them allowed us to intro-duce two basic topics which form the subject of this book: semantics andprogram verification. We now proceed by gradually introducing more powerful programming concepts and extending our analysis to them.Every realistic programming language offers some way of structuring theprograms. Historically, the first concept allowing us to do so was procedures.To systematically study their verification we proceed in two steps.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
