3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 21
Текст из файла (страница 21)
(So alternatively we can write var(z̄) for({z̄}.)Axiom A2 is true for partial correctness for all programs considered in thisbook and rules A3–A7 are sound for both partial and total correctness forall programs considered in this book. To state this property we refer belowto an arbitrary program S, with the understanding that semantics N [[S]] ofsuch a program S is a function3.9 Case Study: Partitioning an Array99N [[S]] : Σ → P(Σ ∪ {⊥, fail, ∆})that satisfies the Change and Access Lemma 3.4. This lemma holds for allprograms considered in this book and any semantics.Theorem 3.7. (Soundness of Auxiliary Axioms and Rules)(i) Axiom A2 is true for partial correctness of arbitrary programs.(ii) Proof rules A3–A7 are sound for partial correctness of arbitrary programs.(iii) Proof rules A3–A7 are sound for total correctness of arbitrary programs.Proof. See Exercise 3.17.⊓⊔Clearly, other auxiliary rules can be introduced but we do not need themuntil Chapter 11 where some new auxiliary rules are helpful.3.9 Case Study: Partitioning an ArrayIn this section we investigate the problem of partitioning an array.
It wasoriginally formulated and solved by Hoare [1962] as part of his algorithmQuicksort, which we shall study later in Chapter 5. Consider an array a oftype integer → integer and integer variables m, f, n such that m ≤ f ≤ nholds. The task is to construct a program P ART that permutes the elementsin the array section a[m : n] and computes values of the three variables pi, leand ri standing for pivot, left and right elements such that upon terminationof P ART the following holds:• pi is the initial value of a[f ],• le > ri and the array section a[m : n] is partitioned into three subsectionsof elements,– those with values of at most pi (namely a[m : ri]),– those equal to pi (namely a[ri + 1 : le − 1]), and– those with values of at least pi (namely a[le : n]),see Figure 3.1,• the sizes of the subsections a[m : ri] and a[le : n] are strictly smaller thanthe size of the section a[m : n], i.e., ri − m < n − m and n − le < n − m.To illustrate the input/output behaviour of P ART we give two examples.1.
First consider as input the array sectiona[m : n] = (2, 3, 7, 1, 4, 5, 4, 8, 9, 7)1003 while ProgramsFig. 3.1 Array section a[m : n] partitioned into three subsections.with m = 1, n = 10 and f = 7. Then P ART computes the valuesle = 6, ri = 4 and pi = 4, and permutes the array section using the pivotelement pi into a[m : n] = (2, 3, 4, 1, 4, 5, 7, 8, 9, 7).
Thus the array sectionis partitioned into a[m : ri] = (2, 3, 4, 1), a[ri + 1 : le − 1] = (4), anda[le : n] = (5, 7, 8, 9, 7).2. Second consider as input the array section a[m : n] = (5, 6, 7, 9, 8) withm = 2, n = 6 and f = 2. Then P ART computes the values le = 2, ri = 1and pi = 5, and in this example leaves the array section unchanged asa[m : n] = (5, 6, 7, 9, 8) using the pivot element pi. In contrast to the firstexample, ri < m holds.
So the value of ri lies outside the interval [m : n]and the subsection a[m : ri] is empty. Thus the array section is partitionedinto a[m : ri] = (), a[ri + 1 : le − 1] = (5), and a[le : n] = (6, 7, 9, 8).To formalize the permutation property of P ART , we consider an array βof type integer → integer which will store a bijection on N and an interval[x : y] and require that β leaves a unchanged outside this interval. Thisis expressed by the following bijection property that uses β and the integervariables x and y as parameters:bij(β, x, y) ≡ β is a bijection on N ∧ ∀ i 6∈ [x : y] : β[i] = i,where β is a bijection on N if β is surjective and injective on N , i.e., if(∀y ∈ N ∃x ∈ N : β(x) = y) ∧ ∀x1 , x2 ∈ N : (x1 6= x2 → β(x1 ) 6= β(x2 )).Note that the following implications hold:bij(β, x, y) → ∀ i ∈ [x : y] : β[i] ∈ [x : y],(3.38)bij(β, x, y) ∧ x′ ≤ x ∧ y ≤ y ′ → bij(β, x′ , y ′ ).(3.39)Implication (3.38) states that β permutes all elements of interval [x : y] onlyinside that interval.
Implication (3.39) states that the bijection property ispreserved when the interval in enlarged.We use β to compare the array a with an array a0 of the same type asa that freezes the initial value of a. By quantifying over β, we obtain thedesired permutation property:3.9 Case Study: Partitioning an Array101perm(a, a0 , [x : y]) ≡ ∃ β : (bij(β, x, y) ∧ ∀ i : a[i] = a0 [β[i]]).
(3.40)Altogether, the program P ART should satisfy the correctness formula{m ≤ f ≤ n ∧ a = a0 }P ART{perm(a, a0 , [m : n]) ∧(3.41)pi = a0 [f ] ∧ le > ri ∧( ∀ i ∈ [m : ri] : a[i] ≤ pi) ∧( ∀ i ∈ [ri + 1 : le − 1] : a[i] = pi) ∧( ∀ i ∈ [le : n] : pi ≤ a[i]) ∧ri − m < n − m ∧ n − le < n − m}in the sense of total correctness, where m, f, n, a0 6∈ change(P ART ).The following program is from Foley and Hoare [1971] except that forconvenience we use parallel assigments.P ART ≡ pi := a[f ];le, ri := m, n;while le ≤ ri dowhile a[le] < pi dole := le + 1od;while pi < a[ri] dori := ri − 1od;if le ≤ ri thenswap(a[le], a[ri]);le, ri := le + 1, ri − 1fiodHere for two given simple or subscripted variables u and v the programswap(u, v) is used to swap the values of u and v. So we stipulate that thecorrectness formula{x = u ∧ y = v} swap(u, v) {x = v ∧ y = u}holds in the sense of partial and total correctness, where x and y are freshvariables.To prove (3.41) in a modular fashion, we shall first prove the followingpartial correctness properties P0–P4 separately:1023 while ProgramsP0{a = a0 } P ART {pi = a0 [f ]},P1{true} P ART {ri ≤ n ∧ m ≤ le},P2{x′ ≤ m ∧ n ≤ y ′ ∧ perm(a, a0 , [x′ : y ′ ])}P ART{x′ ≤ m ∧ n ≤ y ′ ∧ perm(a, a0 , [x′ : y ′ ])},P3{true}P ART{ le > ri ∧( ∀ i ∈ [m : ri] : a[i] ≤ pi) ∧( ∀ i ∈ [ri + 1 : le − 1] : a[i] = pi) ∧( ∀ i ∈ [le : n] : pi ≤ a[i])},P4{m ≤ f ≤ n} P ART {m < le ∧ ri < n}.Property P0 expresses that upon termination pi holds the initial values ofthe array element a[f ].
Property P1 states bounds for ri and le. We remarkthat le ≤ n and m ≤ ri need not hold upon termination. Note that propertyP2 implies by the substitution rule A7 with the substitution [x′ , y ′ := m, n]and the consequence rule{perm(a, a0 , [m : n])} P ART {perm(a, a0 , [m : n])}.Since a = a0 → perm(a, a0 , [m : n]), a further application of the consequencerule yields{a = a0 } P ART {perm(a, a0 , [m : n])}.Thus P ART permutes the array section a[m : n] and leaves other elementsof a unchanged. The more general formulation in P2 will be helpful whenproving the correctness of the Quicksort procedure in Chapter 5. PropertyP3 formalizes the partition property of P ART . Note that the postconditionof property P4 is equivalent tori − m < n − m ∧ n − le < n − m,which is needed in the termination proof of the Quicksort procedure: it statesthat the subsections a[m : ri] and a[le : n] are strictly smaller that the sectiona[m : n].By the conjunction rule, we deduce (3.41) in the sense of partial correctness from P0, the above consequence of P2, P3, and P4.
Then to provetermination of P ART we show thatT{m ≤ f ≤ n} P ART {true}3.9 Case Study: Partitioning an Array103holds in the sense of total correctness. By the decomposition rule A1, thisyields (3.41) in the sense of total correctness, as desired.Thus it remains to prove P0–P4 and T.Preparatory Loop InvariantsWe first establish some invariants of the inner loops in P ART .
For the firstinner loop• any assertion p with le 6∈ f ree(p),• m ≤ le,• A(le) ≡ ∃ i ∈ [le : n] : pi ≤ a[i]are invariants. For the second inner loop• any assertion q with ri 6∈ f ree(q),• ri ≤ n,• B(ri) ≡ ∃ j ∈ [m : ri] : a[j] ≤ piare invariants. The claims about p and q are obvious. The checks for m ≤ leand ri ≤ n are also straightforward.
The remaining two invariant propertiesare established by the following two proof outlines for partial correctness:{inv : A(le)}while a[le] < pi do{A(le) ∧ a[le] < pi}{A(le + 1)}le := le + 1{A(le)}od{A(le)}{inv : B(ri)}while pi < a[ri] do{B(ri) ∧ pi < a[ri]}{B(ri − 1)}ri := ri − 1{B(ri)}od{B(ri)}Note that the implicationsA(le) → le ≤ n and B(ri) → m ≤ ri(3.42)hold. Thus A(le) ∧ B(ri) → ri − le ≥ m − n.Further, for both inner loops the assertionI3 ≡ a[m : le − 1] ≤ pi ≤ a[ri + 1 : n],which is a shorthand for∀ i ∈ [m : le − 1] : a[i] ≤ pi ∧ ∀ i ∈ [ri + 1 : n] : pi ≤ a[i],(3.43)1043 while Programsis an invariant, as the following proof outline for partial correctness shows:{inv : I3}while a[le] < pi do{I3 ∧ a[le] < pi}{a[m : le] ≤ pi ≤ a[ri + 1 : n]}le := le + 1{I3}od;{inv : I3}while pi < a[ri] do{I3 ∧ pi < a[ri]}{a[m : le − 1] ≤ pi ≤ a[ri : n]}ri := ri − 1{I3}od{I3}From these invariants further invariants can be obtained by conjunction.Proof of Property P0Clearly, the inital assignment satisfies{a = a0 } pi := a[f ] {pi = a0 [f ]}.Since there are no further assigments to the variable pi in P ART , and a0 6∈change(P ART ), the correctness formula{a = a0 } P ART {pi = a0 [f ]}holds in the sense of partial correctness.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
