3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 33
Текст из файла (страница 33)
We remark that le ≤ n andm ≤ ri need not hold upon termination. Property P2 implies that the callP artition(n, k) permutes the array section a[m : n] and leaves other elementsof a intact, but actually is a stronger statement involving an interval [x′ : y ′ ]that includes [m : n], so that we can carry out the reasoning about therecursive calls of Quicksort.
Finally, property P3 captures the main effect ofthe call P artition(n, k): the elements of the section a[m : n] are rearrangedinto three parts, those smaller than pi (namely a[m : ri]), those equal topi (namely a[ri + 1 : le − 1]), and those larger than pi (namely a[le : n]).Property PT4 is needed in the termination proof of the Quicksort procedure:it implies that the subsections a[m : ri] and a[le : n] are strictly smaller thanthe section a[m : n].The correctness formulas P1–P3 and PT4 for the procedure callP artition(m, n) immediately follow from the properties P1–P4 and T ofthe while program P ART studied in Section 3.9 (see Exercise 5.8).Auxiliary Proof: Permutation PropertyIn the remainder of this section we use the following abbreviation:5.4 Case Study: Quicksort175J ≡ m = x ∧ n = y.We first extend the permutation property P2 to the procedure Quicksort:Q2{perm(a, a0 , [x′ : y ′ ]) ∧ x′ ≤ x ∧ y ≤ y ′ }Quicksort(x, y){perm(a, a0 , [x′ : y ′ ])}Until further notice the provability symbol ⊢ refers to the proof system PWaugmented with the the block rule, the instantiation rule and the auxiliaryrules A3–A7.The appropriate claim needed for the application of the recursion III ruleis:Claim 1.P1, P2, Q2 ⊢ {perm(a, a0 , [x′ : y ′ ]) ∧ x′ ≤ x < y ≤ y ′ }begin local m, n := x, y; SQ end{perm(a, a0 , [x′ : y ′ ])}.Proof.
In Figure 5.3 a proof outline is given that uses as assumptions thecorrectness formulas P1, P2, and Q2. More specifically, the used correctnessformula about the call of P artition is derived from P1 and P2 by the conjunction rule. In turn, the correctness formulas about the recursive calls ofQuicksort are derived from Q2 by an application of the instantiation ruleand the invariance rule. This concludes the proof of Claim 1.⊓⊔We can now derive Q2 by the recursion rule.
In summary, we have provedP1, P2 ⊢ Q2.Auxiliary Proof: Sorting PropertyWe can now verify that the call Quicksort(x, y) sorts the array sectiona[x : y], soQ3{true} Quicksort(x, y) {sorted(a[x : y])}.The appropriate claim needed for the application of the recursion III rule is:1765 Recursive Programs with Parameters{perm(a, a0 , [x′ : y ′ ]) ∧ x′ ≤ x ∧ y ≤ y ′ }begin local{perm(a, a0 , [x′ : y ′ ]) ∧ x′ ≤ x ∧ y ≤ y ′ }m, n := x, y;{perm(a, a0 , [x′ : y ′ ]) ∧ x′ ≤ x ∧ y ≤ y ′ ∧ J}{perm(a, a0 , [x′ : y ′ ]) ∧ x′ ≤ m ∧ n ≤ y ′ }if m < n then{perm(a, a0 , [x′ : y ′ ]) ∧ x′ ≤ m ∧ n ≤ y ′ }P artition(m, n);{perm(a, a0 , [x′ : y ′ ]) ∧ x′ ≤ m ∧ n ≤ y ′ ∧ ri ≤ n ∧ m ≤ le}begin local{perm(a, a0 , [x′ : y ′ ]) ∧ x′ ≤ m ∧ n ≤ y ′ ∧ ri ≤ n ∧ m ≤ le}v, w := ri, le;{perm(a, a0 , [x′ : y ′ ]) ∧ x′ ≤ m ∧ n ≤ y ′ ∧ v ≤ n ∧ m ≤ w}{perm(a, a0 , [x′ : y ′ ]) ∧ x′ ≤ m ∧ v ≤ y ′ ∧ x′ ≤ w ∧ n ≤ y ′ }Quicksort(m, v);{perm(a, a0 , [x′ : y ′ ]) ∧ x′ ≤ w ∧ n ≤ y ′ }Quicksort(w, n){perm(a, a0 , [x′ : y ′ ])}end{perm(a, a0 , [x′ : y ′ ])}fi{perm(a, a0 , [x′ : y ′ ])}end{perm(a, a0 , [x′ : y ′ ])}Fig.
5.3 Proof outline showing permutation property Q2.Claim 2.P3, Q2, Q3 ⊢ {true}begin local m, n := x, y; SQ end{sorted(a[x : y])}.Proof. In Figure 5.4 a proof outline is given that uses as assumptions thecorrectness formulas P3, Q2, and Q3. In the following we justify the correctness formulas about P artition and the recursive calls of Quicksort usedin this proof outline. In the postcondition of P artition we use the followingabbreviation:K≡ v<w∧( ∀ i ∈ [m : v] : a[i] ≤ pi) ∧( ∀ i ∈ [v + 1 : w − 1] : a[i] = pi) ∧( ∀ i ∈ [w : n] : pi ≤ a[i]).5.4 Case Study: Quicksort177{true}begin local{true}m, n := x, y;{J}if m < n then{J ∧ m < n}P artition(m, n);{J ∧ K[v, w := ri, le]}begin local{J ∧ K[v, w := ri, le]}v, w := ri, le;{J ∧ K}Quicksort(m, v);{sorted(a[m : v]) ∧ J ∧ K}Quicksort(w, n){sorted(a[m : v] ∧ sorted(a[w : n] ∧ J ∧ K}{sorted(a[x : v] ∧ sorted(a[w : y] ∧ K[m, n := x, y]}{sorted(a[x : y])}end{sorted(a[x : y])}fi{sorted(a[x : y])}end{sorted(a[x : y])}Fig.
5.4 Proof outline showing sorting property Q3.Observe that the correctness formula{J} P artition(m, n) {J ∧ K[v, w := ri, le]}is derived from P3 by the invariance rule. Next we verify the correctnessformulas{J ∧ K} Quicksort(m, v) {sorted(a[m : v]) ∧ J ∧ K},and{sorted(a[m : v]) ∧ J ∧ K}Quicksort(w, n){sorted(a[m : v] ∧ sorted(a[w : n] ∧ J ∧ K}.about the recursive calls of Quicksort.Proof of (5.10). By applying the instantiation rule to Q3, we obtain(5.10)(5.11)178A15 Recursive Programs with Parameters{true} Quicksort(m, v) {sorted(a[m : v])}.Moreover, by the invariance axiom, we haveA2{J} Quicksort(m, v) {J}.By applying the instantiation rule to Q2, we then obtain{perm(a, a0 , [x′ : y ′ ]) ∧ x′ ≤ m ∧ v ≤ y ′ }Quicksort(m, v){perm(a, a0 , [x′ : y ′ ])}.Applying next the substitution rule with the substitution [x′ , y ′ := m, v]yields{perm(a, a0 , [m : v]) ∧ m ≤ m ∧ v ≤ v}Quicksort(m, v){perm(a, a0 , [m : v])}.So by a trivial application of the consequence rule, we obtain{a = a0 } Quicksort(m, v) {perm(a, a0 , [m : v])}.We then obtain by an application of the invariance rule{a = a0 ∧ K[a := a0 ]} Quicksort(m, v) {perm(a, a0 , [m : v]) ∧ K[a := a0 ]}.Note now the following implications:K → ∃a0 : (a = a0 ∧ K[a := a0 ]),perm(a, a0 , [m : v]) ∧ K[a := a0 ] → K.So we concludeA3{K} Quicksort(m, v) {K}by the ∃-introduction rule and the consequence rule.
Combining the correctness formulas A1–A3 by the conjunction rule we get (5.10).Proof of (5.11). In a similar way as above, we can prove the correctnessformula{a = a0 } Quicksort(w, n) {perm(a, a0 , [w : n])}.By an application of the invariance rule we obtain{a = a0 ∧ sorted(a0 [m : v]) ∧ v < w}Quicksort(w, n){perm(a, a0 , [w : n]) ∧ sorted(a0 [m : v]) ∧ v < w}.Note now the following implications:5.4 Case Study: Quicksort179v < w ∧ sorted(a[m : v]) → ∃a0 : (a = a0 ∧ sorted(a0 [m : v]) ∧ v < w),(perm(a, a0 , [w : n]) ∧ sorted(a0 [m : v]) ∧ v < w) → sorted(a[m : v]).So we concludeB0{v < w ∧ sorted(a[m : v])} Quicksort(w, n) {sorted(a[m : v])}by the ∃-introduction rule and the consequence rule.
Further, by applyingthe instantiation rule to Q3 we obtainB1{true} Quicksort(w, n) {sorted(a[w : n])}.Next, by the invariance axiom we obtainB2{J} Quicksort(w, m) {J}.Further, using the implicationsK → ∃a0 : (a = a0 ∧ K[a := a0 ]),perm(a, a0 , [w : n]) ∧ K[a := a0 ] → K,we can derive from Q2, in a similar manner as in the proof of A3,B3{K} Quicksort(w, n) {K}.Note that B1–B3 correspond to the properties A1–A3 of the procedure callQuicksort(m, v). Combining the correctness formulas B0–B3 by the conjunction rule and observing that K → v < w holds, we get (5.11).The final application of the consequence rule in the proof outline given inFigure 5.4 is justified by the following crucial implication:sorted(a[x : v]) ∧ sorted(a[w : y]) ∧ K[m, n := x, y] →sorted(a[x : y]).Also note that J ∧ m ≥ n → sorted(a[x : y]), so the implicit else branch isproperly taken care of.
This concludes the proof of Claim 2.⊓⊔We can now derive Q3 by the recursion rule. In summary, we have provedP3, Q2 ⊢ Q3.The proof of partial correctness of Quicksort is now immediate: it sufficesto combine Q2 and Q3 by the conjunction rule. Then after applying thesubstitution rule with the substitution [x′ , y ′ := x, y] and the consequencerule we obtain Q1, or more preciselyP1, P2, P3 ⊢ Q1.1805 Recursive Programs with ParametersTotal CorrectnessTo prove termination, by the decomposition rule discussed in Section 3.3 itsuffices to establishQ4{true} Quicksort(x, y) {true}in the sense of total correctness.
In the proof we rely on the property PT4of P artition:{m < n} P artition(m, n) {m < le ∧ ri < n}.The provability symbol ⊢ refers below to the proof system TW augmentedwith the block rule, the instantiation rule and the auxiliary rules A3–A7. Forthe termination proof of the recursive procedure call Quicksort(x, y) we uset ≡ max(y − x, 0)as the bound function. Since t ≥ 0 holds, the appropriate claim needed forthe application of the recursion IV rule is:Claim 3.PT4, {t < z} Quicksort(x, y) {true} ⊢{t = z} begin local m, n := x, y; SQ end {true}.Proof.In Figure 5.5 a proof outline for total correctness isgiven that uses as assumptions the correctness formulas PT4 and{t < z} Quicksort(x, y) {true}.
In the following we justify the correctnessformulas about P artition and the recursive calls of Quicksort used in thisproof outline. Since m, n, z 6∈ change(D), we deduce from PT4 using theinvariance rule the correctness formula{n − m = z ∧ m < n}P artition(m, n){n − m = z ∧ m < n ∧ ri − m < n − m ∧ n − le < n − m}.(5.12)Consider now the assumption{t < z} Quicksort(x, y) {true}.Since n, w, z 6∈ change(D), the instantiation rule and the invariance rule yield{max(v − m, 0) < z ∧ max(n − w, 0) < z}Quicksort(m, v){max(n − w, 0) < z}and{max(n − w, 0) < z} Quicksort(w, n) {true}.5.4 Case Study: Quicksort181{t = z}begin local{max(y − x, 0) = z}m, n := x, y;{max(n − m, 0) = z}if n < k then{max(n − m, 0) = z ∧ m < n}{n − m = z ∧ m < n}P artition(m, n);{n − m = z ∧ m < n ∧ ri − m < n − m ∧ n − le < n − m}begin local{n − m = z ∧ m < n ∧ ri − m < n − m ∧ n − le < n − m}v, w := ri, le;{n − m = z ∧ m < n ∧ v − m < n − m ∧ n − w < n − m}{max(v − m, 0) < z ∧ max(n − w, 0) < z}Quicksort(m, v);{max(n − w, 0) < z}Quicksort(w, n){true}end{true}fi{true}end{true}Fig.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
