3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 17
Текст из файла (страница 17)
Then, to show termination it suffices to prove the simpler correctnessformula {p} S {true} using proof system TW.These two different proofs can be combined into one using the followinggeneral proof rule for total correctness:RULE A1: DECOMPOSITION⊢p {p} S {q},⊢t {p} S {true}{p} S {q}where the provability signs ⊢p and ⊢t refer to proof systems for partial andtotal correctness for the considered program S, respectively.In this chapter we refer to the proof systems PW and TW for while programs.
However, the decomposition rule will also be used for other classes ofprograms. We refrain from presenting a simpler correctness proof of Example 3.5 using this decomposition rule until Section 3.4, where we introducethe concept of a proof outline.SoundnessWe have just established:⊢P W {x ≥ 0 ∧ y ≥ 0} DIV {quo · y + rem = x ∧ 0 ≤ rem < y}and⊢T W {x ≥ 0 ∧ y > 0} DIV {quo · y + rem = x ∧ 0 ≤ rem < y}.However, our goal was to show|= {x ≥ 0 ∧ y ≥ 0} DIV {quo · y + rem = x ∧ 0 ≤ rem < y}and|=tot {x ≥ 0 ∧ y > 0} DIV {quo · y + rem = x ∧ 0 ≤ rem < y}.743 while ProgramsThis goal is reached if we can show that provability of a correctness formulain the proof systems PW and TW implies its truth.
In the terminology oflogic this property is called soundness of a proof system.Definition 3.4. Let G be a proof system allowing us to prove correctnessformulas about programs in a certain class C. We say that G is sound forpartial correctness of programs in C if for all correctness formulas {p} S {q}about programs in C⊢G {p} S {q} implies |= {p} S {q},and G is sound for total correctness of programs in C if for all correctnessformulas {p} S {q} about programs in C⊢G {p} S {q} implies |=tot {p} S {q}.When the class of programs C is clear from the context, we omit the referenceto it.⊓⊔We now wish to establish the following result.Theorem 3.1. (Soundness of PW and TW)(i) The proof system PW is sound for partial correctness of while programs.(ii) The proof system TW is sound for total correctness of while programs.To prove this theorem it is sufficient to reason about each axiom and proofrule of PW and TW separately.
For each axiom we show that it is true and foreach proof rule we show that it is sound, that is, that the truth of its premisesimplies the truth of its conclusion. This motivates the following definition.Definition 3.5. A proof rule of the formϕ1 , . . ., ϕkϕk+1is called sound for partial (total) correctness (of programs in a class C) if thetruth of ϕ1 , . . ., ϕk in the sense of partial (total) correctness implies the truthof ϕk+1 in the sense of partial (total) correctness.If some of the formulas ϕi are assertions then we identify their truth inthe sense of partial (total) correctness with the truth in the usual sense (seeSection 2.6).⊓⊔We now come to the proof of the Soundness Theorem 3.1.Proof. Due to the form of the proof systems PW and TW, it is sufficientto prove that all axioms of PW (TW) are true in the sense of partial (total)3.3 Verification75correctness and that all proof rules of PW (TW) are sound for partial (total)correctness.
Then the result follows by the induction on the length of proofs.We consider all axioms and proof rules in turn.SKIPClearly N [[skip]]([[p]]) = [[p]] for any assertion p, so the skip axiom is true inthe sense of partial (total) correctness.ASSIGNMENTLet p be an assertion. By the Substitution Lemma 2.4 and transition axiom(ii), whenever N [[u := t]](σ) = {τ }, thenσ |= p[u := t] iff τ |= p.This implies N [[u := t]]([[p[u := t]]]) ⊆ [[p]], so the assignment axiom is true inthe sense of partial (total) correctness.COMPOSITIONSuppose thatN [[S1 ]]([[p]]) ⊆ [[r]]andN [[S2 ]]([[r]]) ⊆ [[q]].Then by the monotonicity of N [[S2 ]] (the Input/Output Lemma 3.3(i))N [[S2 ]](N [[S1 ]]([[p]])) ⊆ N [[S2 ]]([[r]]) ⊆ [[q]].But by the Input/Output Lemma 3.3(ii)N [[S1 ; S2 ]]([[p]]) = N [[S2 ]](N [[S1 ]]([[p]]));soN [[S1 ; S2 ]]([[p]]) ⊆ [[q]].Thus the composition rule is sound for partial (total) correctness.CONDITIONALSuppose thatN [[S1 ]]([[p ∧ B]]) ⊆ [[q]]andN [[S2 ]]([[p ∧ ¬B]]) ⊆ [[q]].By the Input/Output Lemma 3.3(iv)763 while ProgramsN [[if B then S1 else S2 fi]]([[p]])= N [[S1 ]]([[p ∧ B]]) ∪ N [[S2 ]]([[p ∧ ¬B]]);soN [[if B then S1 else S2 fi]]([[p]]) ⊆ [[q]].Thus the conditional rule is sound for partial (total) correctness.LOOPSuppose now that for some assertion pM[[S]]([[p ∧ B]]) ⊆ [[p]].(3.16)We prove by induction that for all k ≥ 0M[[(while B do S od)k ]]([[p]]) ⊆ [[p ∧ ¬B]].The case k = 0 is clear.
Suppose the claim holds for some k > 0. ThenM[[(while B do S od)k+1 ]]([[p]])={definition of (while B do S od)k+1 }M[[if B then S; (while B do S od)k else skip fi]]([[p]])={Input/Output Lemma 3.3(iv)}M[[S; (while B do S od)k ]]([[p ∧ B]]) ∪ M[[skip]]([[p ∧ ¬B]]){Input/Output Lemma 3.3(ii) and semantics of skip}M[[(while B do S od)k ]](M[[S]]([[p ∧ B]])) ∪ [[p ∧ ¬B]]⊆{(3.16) and monotonicity of M[[(while B do S od)k ]]}=M[[(while B do S od)k ]]([[p]]) ∪ [[p ∧ ¬B]]⊆{induction hypothesis}[[p ∧ ¬B]].This proves the induction step.
Thus∞[M[[(while B do S od)k ]]([[p]]) ⊆ [[p ∧ ¬B]].k=0But by the Input/Output Lemma 3.3(v)M[[while B do S od]] =∞[M[[(while B do S od)k ]];k=0soM[[while B do S od]]([[p]]) ⊆ [[p ∧ ¬B]].3.3 Verification77Thus the loop rule is sound for partial correctness.CONSEQUENCESuppose thatp → p1 , N [[S]]([[p1 ]]) ⊆ [[q1 ]], and q1 → q.Then, by the Meaning of Assertion Lemma 2.1, the inclusions [[p]] ⊆ [[p1 ]] and[[q1 ]] ⊆ [[q]] hold; so by the monotonicity of N [[S]],N [[S]]([[p]]) ⊆ N [[S]]([[p1 ]]) ⊆ [[q1 ]] ⊆ [[q]].Thus the consequence rule is sound for partial (total) correctness.LOOP IISuppose thatMtot [[S]]([[p ∧ B]]) ⊆ [[p]],(3.17)Mtot [[S]]([[p ∧ B ∧ t = z]]) ⊆ [[t < z]],(3.18)p → t ≥ 0,(3.19)andwhere z is an integer variable that does not occur in p, B, t or S. We showthen that⊥ 6∈ Mtot [[T ]]([[p]]),(3.20)where T ≡ while B do S od.Suppose otherwise.
Then there exists an infinite computation of T startingin a state σ such that σ |= p. By (3.19) σ |= t ≥ 0, so σ(t) ≥ 0. Choose nowan infinite computation ξ of T starting in a state σ such that σ |= p for whichthis value σ(t) is minimal. Since ξ is infinite, σ |= B; so σ |= p ∧ B.Let τ = σ[z := σ(t)].
Thus τ agrees with σ on all variables except z towhich it assigns the value σ(t). Thenτ (t)={assumption about z, Coincidence Lemma 2.3(i)}σ(t)={definition of τ }τ (z);so τ |= t = z. Moreover, also by the assumption about z, τ |= p ∧ B, sinceσ |= p ∧ B. Thusτ |= p ∧ B ∧ t = z.(3.21)By the monotonicity of Mtot , (3.17) and (3.18) implyMtot [[S]][[p ∧ B ∧ t = z]] ⊆ [[p ∧ t < z]],783 while Programssince [[p ∧ B ∧ t = z]] ⊆ [[p ∧ B]]. Thus by (3.21) for some state σ 1< S, τ > →∗ < E, σ 1 >(3.22)σ 1 |= p ∧ t < z.(3.23)andAlso, by (3.21) and the definition of semantics < T, τ > → < S; T, τ >; soby (3.22) < T, τ > →∗ < T, σ 1 >. But by the choice of τ and the Change andAccess Lemma 3.4(ii) T diverges from τ ; so by the Determinism Lemma 3.1it also diverges from σ 1 .Moreover,σ 1 (t)< {(3.23)}σ 1 (z)= {(3.22), Change and Access Lemma 3.4(i) andassumption about z}τ (z)={definition of τ }σ(t).This contradicts the choice of σ and proves (3.20).Finally, by (3.17) M[[S]]([[p ∧ B]]) ⊆ [[p]]; so by the soundness of the looprule for partial correctness M[[T ]]([[p]]) ⊆ [[p ∧ ¬B]].
But (3.20) means thatMtot [[T ]]([[p]]) = M[[T ]]([[p]]);soMtot [[T ]]([[p]]) ⊆ [[p ∧ ¬B]].Thus the loop II rule is sound for total correctness.⊓⊔Our primary goal in this book is to verify programs, that is, to prove thetruth of certain correctness formulas. The use of certain proof systems isonly a means of achieving this goal. Therefore we often apply proof rules toreason directly about the truth of correctness formulas.
This is justified bythe corresponding soundness theorems.Thus, in arguments such as: “by (the truth of) assignment axiom we have|= {x + 1 = y + 1} x := x + 1 {x = y + 1}and|= {x = y + 1} y := y + 1 {x = y};so by (the soundness of) the composition and consequence rules we obtain3.4 Proof Outlines79|= {x = y} x := x + 1; y := y + 1 {x = y}, ”we omit the statements enclosed in brackets.3.4 Proof OutlinesFormal proofs are tedious to follow. We are not accustomed to following aline of reasoning presented in small formal steps. A better solution consistsof a logical organization of the proof with the main steps isolated. The proofcan then be seen on a different level.In the case of correctness proofs of while programs, a possible strategy liesin using the fact that they are structured.
The proof rules follow the syntaxof the programs; so the structure of the program can be used to structurethe correctness proof. We can simply present the proof by giving a programwith assertions interleaved at appropriate places.Partial CorrectnessExample 3.6. Let us reconsider the integer division program studied in Example 3.4. We present the correctness formulas (3.5), (3.6) and (3.7) in thefollowing form:{x ≥ 0 ∧ y ≥ 0}quo := 0; rem := x;{inv : p}while rem ≥ y do{p ∧ rem ≥ y}rem := rem − y; quo := quo + 1od{p ∧ rem < y}{quo · y + rem = x ∧ 0 ≤ rem < y},wherep ≡ quo · y + rem = x ∧ rem ≥ 0.The keyword inv is used here to label the loop invariant.
Two adjacent assertions {q1 }{q2 } stand for the fact that the implication q1 → q2 is true.The proofs of (3.5), (3.6) and (3.7) can also be presented in such a form.For example, here is the proof of (3.5):803 while Programs{x ≥ 0 ∧ y ≥ 0}{0 · y + x = x ∧ x ≥ 0}quo := 0{quo · y + x = x ∧ x ≥ 0}rem := x{p}.⊓⊔This type of proof presentation is simpler to study and analyze than theone we used so far.
Introduced in Owicki and Gries [1976a], it is called a proofoutline. It is formally defined as follows.Definition 3.6. (Proof Outline: Partial Correctness) Let S ∗ stand forthe program S interspersed, or as we say annotated, with assertions, some ofthem labeled by the keyword inv. We define the notion of a proof outline forpartial correctness inductively by the following formation axioms and rules.A formation axiom ϕ should be read here as a statement: ϕ is a proofoutline (for partial correctness).
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
