3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 22
Текст из файла (страница 22)
This proves property P0.Proof of Property P1The initial parallel assignment to le and ri in P ART establishes the assertionsri ≤ n and m ≤ le. We noticed already that ri ≤ n and m ≤ le are invariantsof the inner loops of P ART . Also the final if statement of P ART with its3.9 Case Study: Partitioning an Array105parallel assignment to le and ri preserves ri ≤ n and m ≤ le. These informalarguments can be easily combined into a formal proof of property P1.Proof of Property P2By a global invariant of a program S we mean an assertion GI for whichthere exists a standard proof outline{p} S ∗ {q}for partial correctness such that for every used assertion r (including p andq) the implicationr → GIholds.
Thus the assertions used in the proof outline are equivalent or strongerthan GI. This may be needed to establish GI inside the proof outline.Consider now the permutation property, i.e., that P ART permutes theelements of the array a but leaves a unchanged outside an interval [x′ :y ′ ] containing [m : n]. Its definition uses the assertion perm(a, a0 , [x′ : y ′ ])defined in (3.40):GI ≡ x′ ≤ m ∧ n ≤ y ′ ∧ perm(a, a0 , [x′ : y ′ ]).Since le, ri 6∈ var(GI), we conclude by the previous results on loop invariantsthat GI and hence m ≤ le ∧ ri ≤ n ∧ GI are invariants of both inner loops.Thus the proof outline presented in Figure 3.2 shows that GI is a globalinvariant of P ART . Thus we have verified property P2 in the sense of partialcorrectness.Proof of Property P3To show the partition property P3 we consider the assertion (3.43), i.e.,I3 ≡ a[m : le − 1] ≤ pi ≤ a[ri + 1 : n].The proof outline for partial correctness given in Figure 3.3 shows that{true} P ART {I3 ∧ le > ri}holds.
Note that after the initialization I3 is trivially satisfied because thetwo intervals [m : le − 1] and [ri + 1 : n] are empty for le = m and ri = n, andconsequently, the two universal quantifications in the expanded definition1063 while Programs{GI}pi := a[f ];{GI}le, ri := m, n;{inv : m ≤ le ∧ ri ≤ n ∧ GI}while le ≤ ri do{inv : m ≤ le ∧ ri ≤ n ∧ GI}while a[le] < pi dole := le + 1od;{inv : m ≤ le ∧ ri ≤ n ∧ GI}while pi < a[ri] dori := ri − 1od;{m ≤ le ∧ ri ≤ n ∧ GI}if le ≤ ri then{m ≤ le ∧ ri ≤ n ∧ GI ∧ le ≤ ri}{m ≤ le ≤ n ∧ m ≤ ri ≤ n ∧ GI}swap(a[le], a[ri]);{m ≤ le ∧ ri ≤ n ∧ GI}{m ≤ le + 1 ∧ ri − 1 ≤ n ∧ GI}le, ri := le + 1, ri − 1{m ≤ le ∧ ri ≤ n ∧ GI}fi{m ≤ le ∧ ri ≤ n ∧ GI}od{m ≤ le ∧ ri ≤ n ∧ GI}Fig.
3.2 Proof outline establishing property P2 of P ART .of (3.43) are vacuously true. Further note that I3 ∧ le > ri implies thepostcondition of P3. This proves P3.3.9 Case Study: Partitioning an Array107{true}pi := a[f ];{true}le, ri := m, n;{le = m ∧ ri = n}{inv : I3}while le ≤ ri do{inv : I3}while a[le] < pi dole := le + 1od;{inv : I3 ∧ pi ≤ a[le]}while pi < a[ri] dori := ri − 1od;{I3 ∧ a[ri] ≤ pi ≤ a[le]}if le ≤ ri then{I3 ∧ a[ri] ≤ pi ≤ a[le]}swap(a[le], a[ri]);{I3 ∧ a[le] ≤ pi ≤ a[ri]}{a[m : le] ≤ pi ≤ a[ri : n]}le, ri := le + 1, ri − 1;{I3}fi{I3}od{I3 ∧ le > ri}Fig. 3.3 Proof outline establishing property P3 of P ART .Proof of Property P4To prove property P4 and to prepare ourselves for the termination proof ofP ART we need to establish more loop invariants.
DefineI1 ≡ m ≤ n ∧ m ≤ le ∧ ri ≤ n,I ≡ I1 ∧ A(le) ∧ B(ri),1083 while Programswhere we recall thatA(le) ≡ ∃ i ∈ [le : n] : pi ≤ a[i],B(ri) ≡ ∃ j ∈ [m : ri] : a[j] ≤ pi.Then we have the following proof outlines for partial correctness.(1) For the initial part of P ART we prove:{m ≤ f ≤ n}pi := a[f ];{m ≤ f ≤ n ∧ pi = a[f ]}le, ri := m, n;{m ≤ f ≤ n ∧ pi = a[f ] ∧ le = m ∧ ri = n}{I}(2) For the two inner loops of P ART we notice by the previous results onloop invariants that I and I ∧ pi ≤ a[le] are invariants of the first andsecond inner loop, respectively:{inv : I}while a[le] < pi dole := le + 1od;{inv : I ∧ pi ≤ a[le]}while pi < a[ri] dori := ri − 1od{I1 ∧ A(le) ∧ B(ri) ∧ a[ri] ≤ pi ≤ a[le]}(3) For the case le < ri of the body of the final if statement of P ART weprove:{le < ri ∧ I1 ∧ A(le) ∧ B(ri) ∧ a[ri] ≤ pi ≤ a[le]}swap(a[le], a[ri]);{le < ri ∧ I1 ∧ A(le) ∧ B(ri) ∧ a[le] ≤ pi ≤ a[ri]}{I1 ∧ A(le + 1) ∧ B(ri − 1)}le, ri := le + 1, ri − 1{I1 ∧ A(le) ∧ B(ri)}{I1 ∧ ((A(le) ∧ B(ri)) ∨ m ≤ le − 1 = ri + 1 ≤ n)}3.9 Case Study: Partitioning an Array109(4) For the case le = ri of the body of the final if statement of P ART weprove:{le = ri ∧ I1 ∧ A(le) ∧ B(ri) ∧ a[ri] ≤ pi ≤ a[le]}{m ≤ le = ri ≤ n ∧ I1}swap(a[le], a[ri]);{m ≤ le = ri ≤ n ∧ I1}le, ri := le + 1, ri − 1{m ≤ le − 1 = ri + 1 ≤ n ∧ I1}{I1 ∧ ((A(le) ∧ B(ri)) ∨ m ≤ le − 1 = ri + 1 ≤ n)}(5) Combining (3) and (4) with the disjunction rule A3, we establish thefollowing correctness formula:{le ≤ ri ∧ I1 ∧ A(le) ∧ B(ri) ∧ a[ri] ≤ pi ≤ a[le]}swap(a[le], a[ri]);le, ri := le + 1, ri − 1{I1 ∧ ((A(le) ∧ B(ri)) ∨ m ≤ le − 1 = ri + 1 ≤ n)}(6) From (5) we obtain for the if statement:{I1 ∧ A(le) ∧ B(ri) ∧ a[ri] ≤ pi ≤ a[le]}if le ≤ ri then{le ≤ ri ∧ I1 ∧ A(le) ∧ B(ri) ∧ a[ri] ≤ pi ≤ a[le]}swap(a[le], a[ri]);le, ri := le + 1, ri − 1{I1 ∧ ((A(le) ∧ B(ri)) ∨ m ≤ le − 1 = ri + 1 ≤ n)}fi{I1 ∧ ((A(le) ∧ B(ri)) ∨ m ≤ le − 1 = ri + 1 ≤ n)}Note that by the following chain of implicationsI1 ∧ A(le) ∧ B(ri) ∧ a[ri] ≤ pi ≤ a[le] ∧ le > ri→ I1 ∧ A(le) ∧ B(ri)→ I1 ∧ ((A(le) ∧ B(ri)) ∨ m ≤ le − 1 = ri + 1 ≤ n),the implicit else branch is properly taken care of.(7) Finally, we show thatle > ri ∧ ((m ≤ le − 1 = ri + 1 ≤ n) ∨ (m ≤ le ≤ n ∧ m ≤ ri ≤ n))implies the postcondition of P4, i.e.,m < le ∧ ri < n.1103 while ProgramsIf m ≤ le − 1 = ri + 1 ≤ n we have the implicationsm ≤ le − 1 → m < le and ri + 1 ≤ n → ri < mIf m ≤ le ≤ n ∧ m ≤ ri ≤ n we calculatem< {m ≤ ri}−ri≤ {le > ri}leandri< {le > ri}le≤ {le ≤ n}n.Now we combine (1), (2) and (6) with (3.42) and (7) to arrive at the overallproof outline for P ART given in Figure 3.4.
Thus we have verified propertyP4 in the sense of partial correctness.TerminationTo prove the termination propertyT{m ≤ f ≤ n} P ART {true}we reuse the invariants established for the three loops in the proof outlineof Figure 3.4 and add appropriate bound functions. For the first and secondinner loops we taket1 ≡ n − le and t2 ≡ ri − m,respectively, and for the outer loop we chooset ≡ ri − le + n + 2 − m.Let us first consider the two inner loops. Recall that I ≡ I1 ∧ A(le) ∧ B(ri).By (3.42), we obtain I → t1 ≥ 0 and I → t2 ≥ 0. Thus it remains to beshown that each iteration of the inner loops decreases the value of the boundfunctions. But this is obvious since le is incremented and ri is decremented,respectively, whereas m and n do not change.More subtle is the argument for the outer loop.
Note thatI1 ∧ ((A(le) ∧ B(ri)) ∨ m ≤ le − 1 = ri + 1 ≤ n) → t ≥ 0because on the one hand A(le) ∧ B(ri) implies ri−le ≥ m−n and thus t ≥ 2,and on the other hand I1 ∧ m ≤ le − 1 = ri + 1 ≤ n implies t = n − m ≥ 0.3.9 Case Study: Partitioning an Array111{m ≤ f ≤ n}pi := a[f ];le, ri := m, n;{I1 ∧ A(le) ∧ B(ri)}{inv : I1 ∧ ((A(le) ∧ B(ri)) ∨ m ≤ le − 1 = ri + 1 ≤ n)}while le ≤ ri do{I1 ∧ A(le) ∧ B(ri) ∧ le ≤ ri}{inv : I1 ∧ A(le) ∧ B(ri)}while a[le] < pi dole := le + 1od;{inv : I1 ∧ A(le) ∧ B(ri) ∧ pi ≤ a[le]}while pi < a[ri] dori := ri − 1od;{I1 ∧ A(le) ∧ B(ri) ∧ a[ri] ≤ pi ≤ a[le]}if le ≤ ri thenswap(a[le], a[ri]);le, ri := le + 1, ri − 1fi{I1 ∧ ((A(le) ∧ B(ri)) ∨ m ≤ le − 1 = ri + 1 ≤ n)}od{I1 ∧ ((A(le) ∧ B(ri)) ∨ m ≤ le − 1 = ri + 1 ≤ n) ∧ le > ri}{le > ri ∧ ((m ≤ le − 1 = ri + 1 ≤ n) ∨ (m ≤ le ≤ n ∧ m ≤ ri ≤ n))}{m < le ∧ ri < n}Fig.
3.4 Proof outline establishing property P4 of P ART .To see that the value of t decreases in each iteration of the outer loop, wefirst give an informal argument. If upon termination of the two inner loopsthe condition le ≤ ri holds, the value of t decreases thanks to the parallelassignment le, ri := le + 1, ri − 1 inside the conditional statement. If le > riholds instead, one of the inner loops must have been executed (because atthe entrance of the outer loop body le ≤ ri was true), thus incrementing leor decrementing ri.Formally, we use the following proof outline for total correctness for thefirst part of the body of the outer loop:{t = z ∧ le ≤ ri ∧ I}1123 while Programs{t = z ∧ z ≥ n + 2 − m ∧ I}{inv : t ≤ z ∧ z ≥ n + 2 − m ∧ I} {bd : t1 }while a[le] < pi do{t ≤ z ∧ z ≥ n + 2 − m ∧ I ∧ a[le] < pi}le := le + 1{t ≤ z ∧ z ≥ n + 2 − m ∧ I}od;{inv : t ≤ z ∧ z ≥ n + 2 − m ∧ I} {bd : t2 }while pi < a[ri] do{t ≤ z ∧ z ≥ n + 2 − m ∧ I ∧ pi < a[ri]}ri := ri − 1{t ≤ z ∧ z ≥ n + 2 − m ∧ I}od;{t ≤ z ∧ z ≥ n + 2 − m}For the subsequent if statement we distinguish the cases le ≤ ri and le > ri.In the first case we continue with the following proof outline:{le ≤ ri ∧ t ≤ z ∧ z ≥ n + 2 − m}if le ≤ ri then{t ≤ z}swap(a[le], a[ri]);{t ≤ z}le, ri := le + 1, ri − 1{t < z}else{le ≤ ri ∧ t ≤ z ∧ z ≥ n + 2 − m ∧ le > ri}{false}skip{t < z}fi{t < z}For the clarity of the argument we made the else branch of the if statementvisible.
In the second case we use the following proof outline:{le > ri ∧ t ≤ z ∧ z ≥ n + 2 − m}{le > ri ∧ t < n + 2 − m ≤ z}if le ≤ ri then{le > ri ∧ t < n + 2 − m ≤ z ∧ le ≤ ri}3.10 Systematic Development of Correct Programs113{false}swap(a[le], a[ri]);{false}le, ri := le + 1, ri − 1{t < z}else{t < z}skip{t < z}fi{t < z}The disjunction rule A3 applied to the above cases yields{t ≤ z ∧ z ≥ n + 2 − m} if . . . fi {t < z},which by the composition rule completes the proof that the value of t decreases in each iteration of the outer loop. To summarize, the proof outlinein Figure 3.5 establishes the total correctness result T.3.10 Systematic Development of Correct ProgramsWe now discuss an approach of Dijkstra [1976] allowing us to develop programs together with their correctness proofs.
To this end, we make use of theproof system TW to guide us in the construction of a program. We followhere the exposition of Gries [1982]. All correctness formulas are supposed tohold in the sense of total correctness.The main issue in Dijkstra’s approach is the development of loops.
Supposewe want to find a program R of the formR ≡ T ; while B do S odthat satisfies, for a given precondition r and postcondition q, the correctnessformula{r} R {q}.(3.44)To avoid trivial solutions for R (cf. the comment after (3.3) in Example 3.4),we usually postulate that some variables in r and q, say x1 , . . ., xn , may notbe modified by R. Thus we requirex1 , .
. ., xn 6∈ change(R).1143 while Programs{m ≤ f ≤ n}pi := a[f ];le, ri := m, n;{inv : I1 ∧ ((A(le) ∧ B(ri)) ∨ m ≤ le − 1 = ri + 1 ≤ n)}{bd : t}while le ≤ ri do{inv : I}{bd : t1 }while a[le] < pi dole := le + 1od;{inv : I}{bd : t2 }while pi < a[ri] dori := ri − 1od;if le ≤ ri thenswap(a[le], a[ri]);le, ri := le + 1, ri − 1;fiod{true}Fig. 3.5 Proof outline establishing the termination property T of P ART .To prove (3.44), it is sufficient to find a loop invariant p and a bound functiont satisfying the following conditions:1.2.3.4.5.p is initially established; that is, {r} T {p} holds;p is a loop invariant; that is, {p ∧ B} S {p} holds;upon loop termination q is true; that is, p ∧ ¬B → q;p implies t ≥ 0; that is, p → t ≥ 0;t is decreased with each iteration; that is, {p ∧ B ∧ t = z} S {t < z}holds where z is a fresh variable.Conditions 1–5 can be conveniently presented by the following proof outline for total correctness:{r}T;{inv : p}{bd : t}while B do{p ∧ B}S3.10 Systematic Development of Correct Programs115{p}od{p ∧ ¬B}{q}Now, when only r and q are known, the first step in finding R consists offinding a loop invariant.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
