3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 31
Текст из файла (страница 31)
, {pn } Pn (t̄n ) {qn } ⊢ {p} S {q},{p1 } P1 (t̄1 ) {q1 }, . . . , {pn } Pn (t̄n ) {qn } ⊢{pi } begin local ūi := t̄i ; Si end {qi }, i ∈ {1, . . ., n}{p} S {q}where Pi (ū1 ) :: Si ∈ D for i ∈ {1, . . ., n}.Note that this rule allows us to introduce an arbitrary set of assumptionsabout specific calls of procedures declared by D. In particular, we do notexclude that Pi ≡ Pj for i 6= j.To deal with recursion in general we modify appropriately the approach ofChapter 4. As in Section 4.3, we modify the auxiliary axioms and proof rulesintroduced in Section 3.8 so that the conditions for specific variables refer tothe extended set change(S).To prove partial correctness of recursive programs with parameters we usethen the following proof system PRP :PROOF SYSTEM PRP :This system consists of the group of axiomsand rules 1–6, 10–12, and A2–A6.5.3 Verification163Thus PRP is obtained by extending the proof system PW by the block rule 10,the instantiation rule 11, the recursion rule 12, and the auxiliary rules A2–A6.Next, we prove a generic invariance property of arbitrary procedure calls.This property states that the values of the actual parameters remain unaffected by a procedure call when none of its variables can be changed withinthe set of procedure declarations D.Lemma 5.3.
(Procedure Call) Suppose that {z̄} ∩ (var(D) ∪ var(t̄)) = ∅and var(t̄) ∩ change(D) = ∅. Then{z̄ = t̄} P (t̄) {z̄ = t̄}can be proved in the proof system PRP.Proof. First note that for each procedure declaration Pi (ū) :: Si from D thecorrectness formula{z̄ = x̄} begin local ūi := x̄i ; Si end {z̄ = x̄},where var(x̄) ∩ var(D) = ∅, holds by the adopted modification of the invariance axiom. This yields by the recursion III rule (no assumptions are neededhere){z̄ = x̄} P (x̄) {z̄ = x̄},from which the conclusion follows by the instantiation axiom.⊓⊔We now use the above observation to reason about a specific recursiveprogram.Example 5.9.
Assume the declaration (5.1) of the factorial procedure. Wefirst prove the correctness formula{x ≥ 0} F ac(x) {y = x!}(5.5)in the proof system PRP. To this end, we introduce the assumption{x ≥ 0} F ac(x) {y = x!}and show that{x ≥ 0} F ac(x) {y = x!} ⊢ {x ≥ 0} begin local u := x; S end {y = x!},whereS ≡ if u = 0 then y := 1 else F ac(u − 1); y := y · u fiis the procedure body of Fac.1645 Recursive Programs with ParametersNote that {x, u} ∩ change(S) = ∅, so we can apply the instantiation ruleto the assumption to obtain{u − 1 ≥ 0} F ac(u − 1) {y = (u − 1)!}and then apply the invariance rule to obtain{x = u ∧ u − 1 ≥ 0} F ac(u − 1) {x = u ∧ y = (u − 1)!}.It is clear how to extend the notion of a proof outline to programs that include procedure calls with parameters and the block statement.
So we presentthe desired proof in the form of a proof outline, given in Figure 5.1. It usesthe last correctness formula as an assumption. Note that the block rule canbe applied here since u 6∈ f ree(y = x!). The desired conclusion (5.5) nowfollows by the simplified form of the recursion III rule.{x ≥ 0}begin local{x ≥ 0}u := x{x = u ∧ u ≥ 0}if u = 0then{x = u ∧ u ≥ 0 ∧ u = 0}{x = u ∧ 1 = u!}y := 1{x = u ∧ y = u!}else{x = u ∧ u ≥ 0 ∧ u 6= 0}{x = u ∧ u − 1 ≥ 0}F ac(u − 1);{x = u ∧ y = (u − 1)!}{x = u ∧ y · u = u!}y := y · u{x = u ∧ y = u!}fi{x = u ∧ y = u!}{y = x!}end{y = x!}Fig. 5.1 Proof outline showing partial correctness of the factorial procedure.5.3 Verification165Additionally, by the generic property established in the Procedure CallLemma 5.3, we have{z = x} F ac(x) {z = x},(5.6)that is, the call F ac(x) does not modify x.
Combining the two correctnessformulas by the conjunction rule we obtain{z = x ∧ x ≥ 0} F ac(x) {z = x ∧ y = x!},which specifies that F ac(x) indeed computes in the variable y the factorialof the original value of x.⊓⊔ModularityIn the example above we combined two correctness formulas derived independently. In some situations it is helpful to reason about procedure calls in amodular way, by first deriving one correctness formula and then using it in aproof of another correctness formula.
The following modification of the abovesimplified version of the recursion III rule illustrates this principle, where welimit ourselves to a two-stage proof and one procedure:RULE 12 ′ : MODULARITY{p0 } P (t̄) {q0 } ⊢ {p0 } begin local ū := t̄; S end {q0 },{p0 } P (t̄) {q0 }, {p} P (s̄) {q} ⊢ {p} begin local ū := s̄; S end {q}{p} P (s̄) {q}where D = P (ū) :: S.So first we derive an auxiliary property, {p0 } P (t̄) {q0 } that we subsequently use in the proof of the ‘main’ property, {p} P (s̄) {q}.
In general,more procedures may be used and an arbitrary ‘chain’ of auxiliary properties may be constructed. We shall illustrate this approach in the case studyconsidered at the end of this chapter.Total CorrectnessTotal correctness of recursive programs is dealt with analogously as in thecase of parameterless procedures. The corresponding proof rule is an appropriate modification of recursion III rule. The provability sign ⊢ refers nowto the proof system TW extended by the auxiliary rules, modified as ex-1665 Recursive Programs with Parametersplained earlier in this section, and the block and instantiation rules. It hasthe following form:RULE 13: RECURSION IV{p1 } P1 (ē1 ) {q1 }, .
. . , {pn } Pn (ēn ) {qn } ⊢ {p} S {q},{p1 ∧ t < z} P1 (ē1 ) {q1 }, . . . , {pn ∧ t < z} Pn (ēn ) {qn } ⊢{pi ∧ t = z} begin local ūi := ēi ; Si end {qi }, i ∈ {1, . . ., n}{p} S {q}where Pi (ūi ) :: Si ∈ D, for i ∈ {1, . . ., n}, and z is an integer variable thatdoes not occur in pi , t, qi and Si for i ∈ {1, . . ., n} and is treated in the proofsas a constant, which means that in these proofs neither the ∃-introductionrule A5 nor the substitution rule A7 is applied to z. In these proofs weallow the axioms and proof rules of the proof system TW extended with theblock rule, the instantiation rule and appropriately modified auxiliary axiomsand proof rules introduced in Section 3.8.
This modification consists of thereference to the extended set change(S), as defined in Section 4.3.To prove total correctness of recursive programs with parameters we usethe following proof system TRP :PROOF SYSTEM TRP :This system consists of the group of axiomsand rules 1–4, 6, 7, 10, 11, 13, and A3–A6.Thus TRP is obtained by extending the proof system TW by the block rule 10,the instantiation rule 11, the recursion rule 13, and the auxiliary rules A3–A6.As before, in the case of one recursive procedure this rule can be simplifiedto{p ∧ t < z} P (ē) {q} ⊢ {p ∧ t = z} begin local ū := ē; S end {q},p→t≥0{p} P (ē) {q}where D = P (ū) :: S and z is an integer variable that does not occur in p, t, qand S and is treated in the proof as a constant.Example 5.10.
To illustrate the use of the simplified rule for total correctness we return to Example 5.9. We proved there the correctness formula{x ≥ 0} F ac(x) {y = x!}5.3 Verification167in the sense of partial correctness, assuming the declaration (5.1) of the factorial procedure.To prove termination it suffices to establish the correctness formula{x ≥ 0} F ac(x) {true}.We chooset≡xas the bound function. Then x ≥ 0 → t ≥ 0.
Assume now{x ≥ 0 ∧ x < z} F ac(x) {true}.We have u 6∈ change(D), so by the instantiation rule{u − 1 ≥ 0 ∧ u − 1 < z} F ac(u − 1) {true}.We use this correctness formula in the proof outline presented in Figure 5.2that establishes that{x ≥ 0 ∧ x < z} F ac(x) {true}⊢ {x ≥ 0 ∧ x = z} begin local u := x; S end {true}.Applying now the simplified form of the recursion IV rule we get thedesired conclusion.⊓⊔SoundnessWe now prove the soundness of the proof system PRP for partial correctnessof recursive programs with parameters.
The establish soundness of the blockrule we need the following lemma.Lemma 5.4. (Block) For all proper states σ and τ ,τ ∈ M[[begin local x̄ := t̄; S end]](σ)implies that for some sequence of values d¯¯ ∈ M[[x̄ := t̄; S]](σ).τ [x̄ := d]⊓⊔Proof. See Exercise 5.3.Theorem 5.1. (Soundness of the Block Rule) Suppose that|= {p} x̄ := t̄; S {q},1685 Recursive Programs with Parameters{x ≥ 0 ∧ x = z}begin local{x ≥ 0 ∧ x = z}u := x{u ≥ 0 ∧ u = z}if u = 0then{u ≥ 0 ∧ u = z ∧ u = 0}{true}y := 1{true}else{u ≥ 0 ∧ u = z ∧ u 6= 0}{u − 1 ≥ 0 ∧ u − 1 < z}F ac(u − 1);{true}y := y · u{true}fi{true}end{true}Fig. 5.2 Proof outline showing termination of the factorial procedure.where {x̄} ∩ f ree(q) = ∅.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
