3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 26
Текст из файла (страница 26)
We present them as proofoutlines from a set of assumptions. These assumptions are correctness formulas about the calls of the considered procedures.We illustrate this proof presentation by returning to the factorial program.Example 4.4. Assume the declaration (4.1) of the factorial program. Weprove the correctness formula{z = x ∧ x ≥ 0} F ac {z = x ∧ y = x!}in the proof system PR.
The assertion z = x is used both in the pre- andpostcondition to prove that the call of Fac does not modify the value of xupon termination. (Without it the postcondition y = x! could be triviallyachieved by setting both x and y to 1.)To this end, we introduce the assumption{z = x ∧ x ≥ 0} F ac {z = x ∧ y = x!}and show that{z = x ∧ x ≥ 0} F ac {z = x ∧ y = x!}⊢ {z = x ∧ x ≥ 0} S {z = x ∧ y = x!},whereS ≡ if x = 0 then y := 1 else x := x − 1; F ac; x := x + 1; y := y · x fiis the procedure body of Fac.First we apply the substitution rule to the assumption and obtain{z − 1 = x ∧ x ≥ 0} F ac {z − 1 = x ∧ y = x!}.The proof that uses this assumption can now be presented in the form of aproof outline that we give in Figure 4.1.
The desired conclusion now followsby the simplified form of the recursion rule.⊓⊔Total CorrectnessWe say that the correctness formula {p} S {q} is true in the sense of totalcorrectness, and write |=tot {p} S {q}, ifMtot [[S]]([[p]]) ⊆ [[q]].4.3 Verification135{z = x ∧ x ≥ 0}if x = 0then{z = x ∧ x ≥ 0 ∧ x = 0}{z = x ∧ 1 = x!}y := 1{z = x ∧ y = x!}else{z = x ∧ x ≥ 0 ∧ x 6= 0}{z − 1 = x − 1 ∧ x − 1 ≥ 0}x := x − 1;{z − 1 = x ∧ x ≥ 0}F ac;{z − 1 = x ∧ y = x!}x := x + 1;{z − 1 = x − 1 ∧ y = (x − 1)!}{z − 1 = x − 1 ∧ y · x = x!}y := y · x{z − 1 = x − 1 ∧ y = x!}{z = x ∧ y = x!}fi{z = x ∧ y = x!}Fig. 4.1 Proof outline showing partial correctness of the factorial procedure.In this subsection the provability sign ⊢ refers to the proof system for totalcorrectness that consists of the proof system TW extended by the appropriately modified auxiliary rules introduced in Section 3.8.Let D = P1 :: S1 , .
. . , Pn :: Sn . In order to prove |=tot {P } S {q} we firstproveA ⊢ {p}S{q}for some sequenceA ≡ {p1 } P1 {q1 }, . . . , {pn } Pn {qn }of assumptions. In order to discharge these assumptions we additionally provethat for i = 1, . . . , n{p1 ∧ t < z} P1 {q1 }, . . . , {pn ∧ t < z} Pn {qn } ⊢ {pi ∧ t = z} Si {qi }andpi → t ≥ 01364 Recursive Programshold. Here t is an integer expression and z a fresh integer variable which istreated in the proofs{p1 ∧ t < z} P1 {q1 }, . . . , {pn ∧ t < z} Pn {qn } ⊢ {pi ∧ t = z} Si {qi },for i = 1, .
. . , n, as a constant, which means that in these proofs neither the∃-introduction rule nor the substitution rule of Section 3.8 is applied to z.The expression t plays the role analogous to the bound function of a loop.We summarize these steps as the following proof rule:RULE 9: RECURSION II{p1 } P1 {q1 }, .
. . , {pn } Pn {qn } ⊢ {p} S {q},{p1 ∧ t < z} P1 {q1 }, . . . , {pn ∧ t < z} Pn {qn } ⊢{pi ∧ t = z} Si {qi }, i ∈ {1, . . ., n},pi → t ≥ 0, i ∈ {1, . . ., n}{p} S {q}where D = P1 :: S1 , . . . , Pn :: Sn and z is an integer variable that does notoccur in pi , t, qi and Si for i ∈ {1, . . ., n} and is treated in the proofs as aconstant, which means that in these proofs neither the ∃-introduction ruleA5 nor the substitution rule A7 is applied to z.The intuition behind this rule is as follows.
Say that a program S is (p, q, t)correct if {p} S {q} holds in the sense of total correctness, with at most tprocedure calls in each computation starting in a proper state satisfying p,where t ≥ 0.The second premise of the rule states that we can establish for i = 1, . . . , nthe (pi , qi , t)-correctness of the procedure bodies Si from the assumption ofthe (pi , qi , z)-correctness of the procedure calls Pi , for i = 1, . . . , n, where z <t. Then, thanks to the last premise, we can prove unconditionally {pi } Pi {qi }in the sense of total correctness, for i = 1, .
. . , n, and thanks to the firstpremise, {p} S {q} in the sense of total correctness.To prove total correctness of recursive programs we use the following proofsystem TR:PROOF SYSTEM TR :This system consists of the group of axiomsand rules 1–4, 6, 7, 9, and A3–A6.Thus TR is obtained by extending proof system TW by the recursion II rule(rule 9) and the auxiliary rules A3–A6.Again, when we deal only with one recursive procedure and use the procedure call as the statement in the considered recursive program, this rule can4.3 Verification137be simplified to{p ∧ t < z} P {q} ⊢ {p ∧ t = z} S {q},p→t≥0{p} P {q}where D = P :: S and z is treated in the proof as a constant.DecompositionAs for while programs it is sometimes more convenient to decompose theproof of total correctness of a recursive program into two separate proofs, oneof partial correctness and one of termination.
Formally, this can be done usingthe decomposition rule A1 introduced in Section 3.3, but with the provabilitysigns ⊢p and ⊢t referring to the proof systems PR and TR, respectively.Example 4.5. We apply the decomposition rule A1 to the factorial programstudied in Example 4.4. Assume the declaration (4.1) of the factorial program.To prove the correctness formula{z = x ∧ x ≥ 0} F ac {z = x ∧ y = x!}(4.2)in the sense of total correctness, we build upon the fact that we proved italready in the sense of partial correctness.Therefore we only need to establish termination. To this end, it suffices toprove the correctness formula{x ≥ 0} F ac {true}(4.3)in the proof system TR. We chooset≡xas the bound function. The proof outline presented in Figure 4.2 then showsthat{x ≥ 0 ∧ x < z} F ac {true} ⊢ {x ≥ 0 ∧ x = z} S {true}holds.
Applying now the simplified form of the recursion II rule we get (4.3).By the consequence rule, we obtain {z = x ∧ x ≥ 0} F ac {true}, as requiredby the decomposition rule to establish (4.2).⊓⊔1384 Recursive Programs{x ≥ 0 ∧ x = z}if x = 0then{x ≥ 0 ∧ x = z ∧ x = 0}{true}y := 1{true}else{x ≥ 0 ∧ x = z ∧ x 6= 0}{x − 1 ≥ 0 ∧ x − 1 < z}x := x − 1;{x ≥ 0 ∧ x < z}F ac;{true}x := x + 1;{true}y := y · x{true}fi{true}Fig.
4.2 Proof outline showing termination of the factorial procedure.DiscussionLet us clarify now the restrictions used in the recursion II rule. The followingexample explains why the restrictions we imposed on the integer variable zare necessary.Example 4.6. Consider the trivially non-terminating recursive proceduredeclared byP :: P.We first show that when we are allowed to existentially quantify the variablez, we can prove {x ≥ 0} P {true} in the sense of total correctness, whichis obviously wrong. Indeed, take as the bound function t simply the integervariable x.
Thenx ≥ 0 → t ≥ 0.Next we show{x ≥ 0 ∧ x < z} P {true} ⊢ {x ≥ 0 ∧ x = z} P {true}.Using the ∃-introduction rule A5 of Section 3.8 we existentially quantify zand obtain from the assumption the correctness formula4.3 Verification139{∃z : (x ≥ 0 ∧ x < z)} P {true}.But the precondition ∃z : (x ≥ 0 ∧ x < z) is equivalent to x ≥ 0, so by theconsequence rule we derive{x ≥ 0} P {true}.Using the consequence rule again we can strengthen the precondition andobtain{x ≥ 0 ∧ x = z} P {true}.Now we apply the simplified form of the recursion II rule and obtain{x ≥ 0} P {true}.In a similar way we can show that we must not apply the substitutionrule A7 of Section 3.8 to the variable z. Indeed, substituting in the aboveassumption {x ≥ 0 ∧ x < z} P {true} the variable z by x + 1 (note that theapplication condition {x, z}∩var(P ) = ∅ of the substitution rule is satisfied),we obtain{x ≥ 0 ∧ x < x + 1} P {true}.Since x ≥ 0 ∧ x = z → x ≥ 0 ∧ x < x + 1, we obtain by the consequence rule{x ≥ 0 ∧ x = z} P {true},⊓⊔as above.SoundnessWe now establish soundness of the recursion rule and as a consequence thatof the proof system PR in the sense of partial correctness.
Below we write{p1 } P1 {q1 }, . . . , {pn } Pn {qn } |= {p} S {q}when the following holds:for all sets of procedure declarations Dif |= {pi } Pi {qi }, for i = 1, . . . , n, then |= {p} S {q}.We shall need the following strengthening of the Soundness Theorem 3.1(i).Recall that the provability sign ⊢ refers to the proof system PW extendedby the appropriately modified auxiliary axioms and proof rules introduced inSection 3.8.Theorem 4.1. (Soundness of Proofs from Assumptions){p1 } P1 {q1 }, . .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
