3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 62
Текст из файла (страница 62)
In fact, it does not matter whichone will be chosen —the final values of the variables twop and threep willalways be the same.35610 Nondeterministic ProgramsThese examples are perhaps somewhat contrived. A more interesting nondeterministic program is presented in Section 10.5.FailuresRecall that an alternative command fails rather than terminates if none ofthe guards evaluates to true. We presented already in Section 3.7 a number ofnatural examples concerning the failure statement that showed the usefulnessof failures.Modeling ConcurrencyNondeterminism arises naturally in the context of parallel programs.
Forexample, upon termination of the programS ≡ [x := 0kx := 1kx := 2]the variable x may have one of the values 1, 2 or 3. Which one depends onthe order in which the three assignments are executed.We can use nondeterministic programs to model this behavior. For example, S can be modeled by the following program:T ≡ turn1 := true; turn2 := true; turn3 := true;do turn1 → x := 0; turn1 := false¤ turn2 → x := 1; turn2 := false¤ turn3 → x := 2; turn3 := falseod.The variables turn1 , turn2 und turn3 are used to model the control flow ofthe parallel program S. Of course, the input/output behavior of S could havebeen modeled by a much simpler program without such extra variables, forexample, byif true → x := 0 ¤ true → x := 1 ¤ true → x := 2 fi.The point is that the transition from S to T can be easily generalized toa transformation of arbitrary parallel programs into nondeterministic ones.(see Section 10.6).10.4 Verification35710.4 VerificationWe now study partial and total correctness of nondeterministic programs.Partial CorrectnessWe first present a proof system PN for partial correctness of nondeterministicprograms.
PN includes axioms 1 and 2 and rules 3 and 6 introduced for PW,the system for partial correctness of while programs. But rules 4 and 5 ofPW are now replaced by:RULE 30: ALTERNATIVE COMMAND{p ∧ Bi } Si {q}, i ∈ {1, . . . , n}{p} if ⊓⊔ni=1 Bi → Si fi {q}RULE 31: REPETITIVE COMMAND{p ∧ Bi } Si {p}, i ∈ {1, . . . , n}Vn{p} do ⊓⊔ni=1 Bi → Si od {p ∧ i=1 ¬Bi }Additionally, as explained in Section 3.8, PN includes the group of axiomsand rules A2–A6.
Summarizing, we use the following proof system.PROOF SYSTEM PN :This system consists of the group of axiomsand rules 1, 2, 3, 6, 30, 31 and A2–A6.Total CorrectnessTo lift PN to a system for total correctness, we have to show absence offailures and absence of divergence. Since failures arise only if none of theguards in an alternative command evaluates to true, their absence is provedby adding a new premise in the rule for alternative commands. Thus weconsider35810 Nondeterministic ProgramsRULE 32: ALTERNATIVE COMMAND IIWnp → i=1 Bi ,{p ∧ Bi } Si {q}, i ∈ {1, .
. . , n}{p} if ⊓⊔ni=1 Bi → Si fi {q}As for while loops, absence of divergence is proved by adding to the repetitive command rule 31 premises dealing with the bound function. Thus weconsiderRULE 33: REPETITIVE COMMAND II{p ∧ Bi } Si {p}, i ∈ {1, . . . , n},{p ∧ Bi ∧ t = z} Si {t < z}, i ∈ {1, .
. . , n},p→t≥0Vn{p} do ⊓⊔ni=1 Bi → Si od {p ∧ i=1 ¬Bi }where t is an integer expression and z is an integer variable not occurring inp, t, Bi or Si for i ∈ {1, . . . , n}.Summarizing, we consider the following proof system TN for total correctness of nondeterministic programs.PROOF SYSTEM TN :This system consists of the group of axioms and rules1, 2, 3, 6, 32, 33 and A3–A6.Again we present correctness proofs in the form of proof outlines.
Thedefinition of proof outlines for nondeterministic programs is analogous tothat for while programs. Thus, in the definition of a proof outline for totalcorrectness, the formation rules about alternative and repetitive commandsare as follows.Let S ∗ and S ∗∗ stand for the program S annotated with assertions andinteger expressions. Then(xiii)Wnp → i=1 Bi ,{p ∧ Bi } Si∗ {q}, i ∈ {1, . .
. , n}{p} if ¤ni=1 Bi → {p ∧ Bi } Si∗ {q} fi {q}10.4 Verification359(xiv){p ∧ Bi } Si∗ {p}, i ∈ {1, . . . , n},{p ∧ Bi ∧ t = z} Si∗∗ {t < z}, i ∈ {1, . . . , n},p→t≥0{inv : p}{bd : t} do ¤ni=1 Bi → {p ∧ Bi } Si∗ {p} od {p ∧Vni=1¬Bi }where t is an integer expression and z is an integer variable not occurring inp, t, Bi or Si for i ∈ {1, . .
. , n}.In proof outlines for partial correctness we drop in (xiii) the first premiseand in (xiv) the premises mentioning the bound function t and {bd : t} inthe conclusion.Example 10.1. The following is a proof outline for total correctness of theprogram GCD mentioned in the beginning of Section 10.3:{x = x0 ∧ y = y0 ∧ x0 > 0 ∧ y0 > 0}{inv : p}{bd : t}do x > y → {p ∧ x > y}x := x − y¤ x < y → {p ∧ x < y}x := y − xod{p ∧ ¬(x > y) ∧ ¬(x < y)}{x = y ∧ y = gcd(x0 , y0 )}.The binary function symbol gcd is to be interpreted as the “greatest commondivisor of.” The fresh variables x0 and y0 used in the pre- and postconditionsrepresent the initial values of x and y.
As an invariant we use herep ≡ gcd(x, y) = gcd(x0 , y0 ) ∧ x > 0 ∧ y > 0and as a bound function t ≡ x + y.⊓⊔SoundnessLet us investigate now the soundness of the proof systems PN and TN fornondeterministic programs. With the definitions as in Chapter 3 we have:Theorem 10.1. (Soundness of PN and TN)(i) The proof system PN is sound for partial correctness of nondeterministicprograms.36010 Nondeterministic Programs(ii) The proof system TN is sound for total correctness of nondeterministicprograms.Proof. It is enough to show that all proof rules are sound under the corresponding notions of correctness.
We leave the details to the reader as allcases are similar to those considered in the proof of the Soundness of PWand TW Theorem 3.1 (see Exercise 10.6).⊓⊔As before, proof outlines {p} S ∗ {q} for partial correctness enjoy the following property: whenever the control of S in a given computation startedin a state satisfying p reaches a point annotated by an assertion, this assertion is true. This intuitive property can be expressed as a Strong SoundnessTheorem about PN analogous to the Strong Soundness Theorem 3.3, but werefrain here from repeating the details.10.5 Case Study: The Welfare Crook ProblemIn this section we generalize the approach of Section 3.10 to the systematicprogram development to the case of nondeterministic programs.
Suppose wewant to find a nondeterministic program R of the formR ≡ T ; do ⊓⊔ni=1 Bi → Si odthat satisfies, for a given precondition r and postcondition q, the correctnessformula{r} R {q}.(10.1)As before, we postulate that for some variables in r and q, say x1 , . . ., xn ,x1 , . . ., xn 6∈ change(R).To prove (10.1), it suffices to find a loop invariant p and a bound function tsatisfying the following five conditions:1.2.3.4.5.p is initially established; that is, {r} T {p} holds;p is a loop invariant; that is, {p ∧ Bi } Si {p}Vfor i ∈ {1, . .
. , n} holds;nupon loop termination q is true; that is, p ∧ i=1 ¬Bi → q;p implies t ≥ 0; that is, p → t ≥ 0;t is decreased with each iteration; that is, {p ∧ Bi ∧ t = z} Si {t < z}for i ∈ {1, . . . , n} holds, where z is a fresh variable.As before, we represent the conditions 1–5 as a proof outline for total correctness:10.5 Case Study: The Welfare Crook Problem361{r}T;{inv : p}{bd : t}do ¤ni=1 Bi → {p ∧ Bi } Si∗ odVn{p ∧ i=1 ¬Bi }{q}.The next step consists of finding an invariant by generalizing the postcondition.We illustrate the development of a nondeterministic program that followsthese steps by solving the following problem due to W. Feijen.
We followhere the exposition of Gries [1981]. Given are three magnetic tapes, eachcontaining a list of different names in alphabetical order. The first containsthe names of people working at IBM Yorktown Heights, the second the namesof students at Columbia University and the third the names of people onwelfare in New York City. Practically speaking, all three lists are endless,so no upper bounds are given. It is known that at least one person is onall three lists. The problem is to develop a program CROOK to locate thealphabetically first such person.Slightly more abstractly, we consider three ordered arrays a, b, c of typeinteger → integer, that is, such that i < j implies a[i] < a[j], and similarlyfor b and c.
We suppose that there exist values iv ≥ 0, jv ≥ 0 and kv ≥ 0such thata[iv] = b[jv] = c[kv]holds, and moreover we suppose that the triple (iv, jv, kv) is the smallestone in the lexicographic ordering among those satisfying this condition. Thevalues iv, jv and kv can be used in the assertions but not in the program.We are supposed to develop a program that computes them.Thus our precondition r is a list of the assumed facts —that a, b, c areordered together with the formal definition of iv, jv and kv. We omit theformal definition.
The postcondition isq ≡ i = iv ∧ j = jv ∧ k = kv,where i, j, k are integer variables of the still to be constructed programCROOK. Additionally we require a, b, c, iv, jv, kv 6∈ change(CROOK).Assuming that the search starts from the beginning of the lists, we arebrought to the following invariant by placing appropriate bounds on i, j andk:p ≡ 0 ≤ i ≤ iv ∧ 0 ≤ j ≤ jv ∧ 0 ≤ k ≤ kv ∧ r.A natural choice for the bound function ist ≡ (iv − i) + (jv − j) + (kv − k).36210 Nondeterministic ProgramsThe invariant is easily established byi := 0; j := 0; k := 0.The simplest ways to decrease the bound functions are the assignments i :=i + 1, j := j + 1 and k := k + 1. In general, it is necessary to increment allthree variables, so we arrive at the following incomplete proof outline:{r}i := 0; j := 0; k := 0;{inv : p}{bd : t}do B1 → {p ∧ B1 } i := i + 1¤ B2 → {p ∧ B2 } j := j + 1¤ B3 → {p ∧ B3 } k := k + 1od{p ∧ ¬B1 ∧ ¬B2 ∧ ¬B3 }{q},where B1 , B2 and B3 are still to be found.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
