3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 16
Текст из файла (страница 16)
This rule states that if an assertion p ispreserved with each iteration of the loop while B do S od, then p is trueupon termination of this loop. Therefore p is called a loop invariant.The consequence rule represents the interface between program verificationand logical formulas. It allows us to strengthen the preconditions and weakenthe postconditions of correctness formulas and enables the application ofother proof rules.
In particular, the consequence rule allows us to replace aprecondition or a postcondition by an equivalent assertion.Using the proof system PW we can prove the input/output behavior ofcomposite programs from the input/output behavior of their subprograms.For example, using the composition rule we can deduce correctness formulasabout programs of the form S1 ; S2 from the correctness formulas about S1and S2 . Proof systems with this property are called compositional.Example 3.3.(i) Consider the programS ≡ x := x + 1; y := y + 1.We prove in the system PW the correctness formula{x = y} S {x = y}.To this end we apply the assignment axiom twice.
We start with the lastassignment. By backward substitution we obtain(x = y)[y := y + 1] ≡ x = y + 1;3.3 Verification67so by the assignment axiom{x = y + 1} y := y + 1 {x = y}.By a second backward substitution we obtain(x = y + 1)[x := x + 1] ≡ x + 1 = y + 1;so by the assignment axiom{x + 1 = y + 1} x := x + 1 {x = y + 1}.Combining the above two correctness formulas by the composition rule yields{x + 1 = y + 1} x := x + 1; y := y + 1 {x = y},from which the desired conclusion follows by the consequence rule, sincex = y → x + 1 = y + 1.(ii) Consider now the more complicated programS ≡ x := 1; a[1] := 2; a[x] := xusing subscripted variables.
We prove that after its execution a[1] = 1 holds;that is, we prove in the system PW the correctness formula{true} S {a[1] = 1}.To this end we repeatedly apply the assignment axiom while proceeding“backwards.” Hence, we start with the last assignment:{(a[1] = 1)[a[x] := x]} a[x] := x {a[1] = 1}.By the Identical Substitution Lemma 2.2 we have 1[a[x] := x] ≡ 1.
Thus thesubstitution in the above correctness formula can be evaluated as follows:{if 1 = x then x else a[1] fi = 1} a[x] := x {a[1] = 1}.For the precondition we have the equivalenceif 1 = x then x else a[1] fi = 1 ↔ (x = 1 ∨ a[1] = 1).Sincex = 1 → (x = 1 ∨ a[1] = 1),we can strengthen the precondition by the rule of consequence as follows:{x = 1} a[x] := x {a[1] = 1}.683 while ProgramsNext, consider the second assignment with the postcondition being the precondition of the above correctness formula. We have{(x = 1)[a[1] := 2]} a[1] := 2 {x = 1},which by the Identical Substitution Lemma 2.2 gives{x = 1} a[1] := 2 {x = 1}.Finally, we consider the first assignment:{true} x := 1 {x = 1}.Combining the final correctness formulas obtained for each assignment bytwo applications of the composition rule, we get the desired result.⊓⊔Let us see now how the loop rule rule can be used.
We choose here asan example the first program (written in a textual form) that was formallyverified. This historic event was duly documented in Hoare [1969].Example 3.4. Consider the following program DIV for computing the quotient and remainder of two natural numbers x and y:DIV ≡ quo := 0; rem := x; S0 ,whereS0 ≡ while rem ≥ y do rem := rem − y; quo := quo + 1 od.We wish to show thatif x, y are nonnegative integers and DIV terminates,then quo is the integer quotient and rem is theremainder of x divided by y.(3.2)Thus, using correctness formulas, we wish to show|= {x ≥ 0 ∧ y ≥ 0} DIV {quo · y + rem = x ∧ 0 ≤ rem < y}.(3.3)Note that (3.2) and (3.3) agree because DIV does not change the variables xand y.
Programs that may change x and y can trivially achieve (3.3) withoutsatisfying (3.2). An example is the programx := 0; y := 1; quo := 0; rem := 0.To show (3.3), we prove the correctness formula{x ≥ 0 ∧ y ≥ 0} DIV {quo · y + rem = x ∧ 0 ≤ rem < y}(3.4)3.3 Verification69in the proof system PW. To this end we choose the assertionp ≡ quo · y + rem = x ∧ rem ≥ 0as the loop invariant of S0 . It is obtained from the postcondition of (3.4) bydropping the conjunct rem < y. Intuitively, p describes the relation betweenthe variables of DIV which holds each time the control is in front of the loopS0 .We now prove the following three facts:{x ≥ 0 ∧ y ≥ 0} quo := 0; rem := x {p},(3.5)that is, the program quo := 0; rem := x establishes p;{p ∧ rem ≥ y} rem := rem − y; quo := quo + 1 {p},(3.6)that is, p is indeed a loop invariant of S0 ;p ∧ ¬(rem ≥ y) → quo · y + rem = x ∧ 0 ≤ rem < y,(3.7)that is, upon exit of the loop S0 , p implies the desired assertion.Observe first that we can prove (3.4) from (3.5), (3.6) and (3.7).
Indeed,(3.6) implies, by the loop rule,{p} S0 {p ∧ ¬(rem ≥ y)}.This, together with (3.5), implies, by the composition rule,{x ≥ 0 ∧ y ≥ 0} DIV {p ∧ ¬(rem ≥ y)}.Now, by (3.7), (3.4) holds by an application of the consequence rule.Thus, let us prove now (3.5), (3.6) and (3.7).Re: (3.5). We have{quo · y + x = x ∧ x ≥ 0} rem := x {p}by the assignment axiom. Once more by the assignment axiom{0 · y + x = x ∧ x ≥ 0} quo := 0 {quo · y + x = x ∧ x ≥ 0};so by the composition rule{0 · y + x = x ∧ x ≥ 0} quo := 0; rem := x {p}.On the other hand,x ≥ 0 ∧ y ≥ 0 → 0 · y + x = x ∧ x ≥ 0;703 while Programsso (3.5) holds by the consequence rule.Re: (3.6).
We have{(quo + 1) · y + rem = x ∧ rem ≥ 0} quo := quo + 1 {p}by the assignment axiom. Once more by the assignment axiom{(quo + 1) · y + (rem − y) = x ∧ rem − y ≥ 0}rem := rem − y{(quo + 1) · y + rem = x ∧ rem ≥ 0};so by the composition rule{(quo + 1) · y + (rem − y) = x ∧ rem − y ≥ 0}rem := rem − y; quo := quo + 1{p}.On the other hand,p ∧ rem ≥ y → (quo + 1) · y + (rem − y) = x ∧ rem − y ≥ 0;so (3.6) holds by the consequence rule.Re: (3.7).
Clear.This completes the proof of (3.4).⊓⊔The only step in the above proof that required some creativity was finding the appropriate loop invariant. The remaining steps were straightforwardapplications of the corresponding axioms and proof rules. The form of theassignment axiom makes it easier to deduce a precondition from a postcondition than the other way around; so the proofs of (3.5) and (3.6) proceeded“backwards.” Finally, we did not provide any formal proof of the implicationsused as premises of the consequence rule. Formal proofs of such assertions arealways omitted; we simply rely on an intuitive understanding of their truth.Total CorrectnessIt is important to note that the proof system PW does not allow us to establish termination of programs.
Thus PW is not appropriate for proofs oftotal correctness. Even though we proved in Example 3.4 the correctness formula (3.4), we cannot infer from this fact that program DIV studied thereterminates. In fact, DIV diverges when started in a state in which y is 0.3.3 Verification71Clearly, the only proof rule of PW that introduces the possibility of nontermination is the loop rule, so to deal with total correctness this rule mustbe strengthened.We now introduce the following refinement of the loop rule:RULE 7: LOOP II{p ∧ B} S {p},{p ∧ B ∧ t = z} S {t < z},p →t≥0{p} while B do S od {p ∧ ¬ B}where t is an integer expression and z is an integer variable that does notappear in p, B, t or S.The two additional premises of the rule guarantee termination of the loop.In the second premise, the purpose of z is to retain the initial value of z.
Sincez does not appear in S, it is not changed by S and upon termination of S zindeed holds the initial value of t. By the second premise, t is decreased witheach iteration and by the third premise t is nonnegative if another iterationcan be performed. Thus no infinite computation is possible. Expression t iscalled a bound function of the loop while B do S od.To prove total correctness of while programs we use the following proofsystem TW :PROOF SYSTEM TW :This system consists of the groupof axioms and rules 1–4, 6, 7.Thus TW is obtained from PW by replacing the loop rule (rule 5) by theloop II rule (rule 7).To see an application of the loop II rule, let us reconsider the programDIV studied in Example 3.4.Example 3.5.
We now wish to show thatif x is nonnegative and y is a positive integer, thenS terminates with quo being the integer quotientand rem being the remainder of x divided by y.(3.8)In other words, we wish to show|=tot {x ≥ 0 ∧ y > 0} DIV {quo · y + rem = x ∧ 0 ≤ rem < y}.(3.9)To show (3.9), we prove the correctness formula{x ≥ 0 ∧ y > 0} DIV {quo · y + rem = x ∧ 0 ≤ rem < y}(3.10)723 while Programsin the proof system TW. Note that (3.10) differs from correctness formula(3.4) in Example 3.4 by requiring that initially y > 0. We prove (3.10) by amodification of the proof of (3.4). Letp′ ≡ p ∧ y > 0,be the loop invariant where, as in Example 3.4,p ≡ quo · y + rem = x ∧ rem ≥ 0,and lett ≡ rembe the bound function.
As in the proof given in Example 3.4, to prove (3.10)in the sense of total correctness it is sufficient to establish the following facts:{x ≥ 0 ∧ y > 0} quo := 0; rem := x {p′ },{p′ ∧ rem ≥ y} rem := rem − y; quo := quo + 1 {p′ },{p′ ∧ rem ≥ y ∧ rem = z}rem := rem − y; quo := quo + 1{rem < z}.p′ → rem ≥ 0,′p ∧ ¬(rem ≥ y) → quo · y + rem = x ∧ 0 ≤ rem < y.(3.11)(3.12)(3.13)(3.14)(3.15)By the loop II rule, (3.12), (3.13) and (3.14) imply the correctness formula{p′ } S0 {p′ ∧ ¬(rem ≥ y)}, and the rest of the argument is the same as inExample 3.4.
Proofs of (3.11), (3.12) and (3.15) are analogous to the proofsof (3.5), (3.6) and (3.7) in Example 3.4.To prove (3.13) observe that by the assignment axiom{rem < z} quo := quo + 1 {rem < z}and{(rem − y) < z} rem := rem − y {rem < z}.Butp ∧ y > 0 ∧ rem ≥ y ∧ rem = z → (rem − y) < z,so (3.13) holds by the consequence rule.Finally, (3.14) clearly holds.This concludes the proof.⊓⊔3.3 Verification73DecompositionProof system TW with loop rule II allows us to establish total correctnessof while programs directly. However, sometimes it is more convenient to decompose the proof of total correctness into two separate proofs, one of partialcorrectness and one of termination. More specifically, given a correctness formula {p} S {q}, we first establish its partial correctness, using proof systemPW.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
