3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 30
Текст из файла (страница 30)
For example, the factorial proceduredefined above does not satisfy this restriction.The partial and total correctness semantics are defined exactly as in thecase of the recursive programs considered in the previous chapter.Example 5.4. Assume the declaration (5.1) of the factorial procedure.
Thenthe following holds for the main statement F ac(x):• if σ(x) ≥ 0 thenM[[F ac(x)]](σ) = Mtot [[F ac(x)]](σ) = {σ[y := σ(x)!]},• if σ(x) < 0 thenM[[F ac(x)]](σ) = ∅ and Mtot [[F ac(x)]](σ) = {⊥}.⊓⊔Note that the introduced semantics treats properly the case when an actualparameter of a procedure call contains a global variable of the procedure body.To illustrate this point consider the call F ac(y) in a state with σ(y) = 3.Then, as in Example 5.3, we can calculate that the computation starting in< F ac(y), σ > terminates in a final state τ with τ (y) = 6.
So the final valueof y is the factorial of the value of the actual parameter, as desired.Finally, we should point out some particular characteristics of our semantics of block statements in the case when in begin local x̄ := t̄; S end avariable from x̄ appears in t̄. For example, upon termination of the programbegin local x := x + 1; y := x end; begin local x := x + 1; z := x endthe assertion y = z holds. The intuition here is that in each initializationx := x + 1 the second occurrence of x refers to a different variable than thefirst ocurrence of x, namely to the same variable outside the block statement.Therefore y = z holds upon termination. This corresponds with the semanticsof the procedure calls given by the transition axiom (x) when the actualparameters contain formal parameters.
Then this transition axiom generates5.3 Verification157a block statement the initialization statement of which refers on the lefthand side to the formal parameters and on the right-hand side to the actualparameters of the procedure call.As in the previous chapter we now consider syntactic approximations of therecursive programs and express their semantics in terms of these approximations.
The following lemma is a counterpart of the Input/Output Lemma 4.1.As in the previous chapter, we write here D | S when we consider the programS in the context of the set D of procedure declarations. The complicationnow is that in the case of procedure calls variable clashes can arise. We dealwith them in the same way as in the definition of the transition axiom forthe procedure call.Given D = P1 (ū1 ) :: S1 , . .
. , Pn (ūn ) :: Sn and a recursive program S, wedefine the kth syntactic approximation S k of S by induction on k ≥ 0:S 0 = Ω,S k+1 = S[S1k /P1 , . . . , Snk /Pn ],where S[R1 /P1 , . . . , Rn /Pn ] is the result of a simultaneous replacement in Sof each procedure identifier Pi by the statement Ri . For procedure calls thisreplacement is defined byPi (t̄)[R1 /P1 , . . . , Rn /Pn ] ≡ Ri (t̄) ≡ begin local ūi := t̄; Ri end.Furthermore, let Dk abbreviate D = P1 (ū1 ) :: S1k , .
. . , Pn (ūn ) :: Snk and letN stand for M or Mtot . The following lemma collects the properties of Nwe need.Lemma 5.1. (Input/Output)(i) N [[Dk | S]] = N [[S k+1 ]].(ii) N [[D | S]] = N [[D | S[S1 /P1 , . . . , Sn /Pn ]]].In particular, N [[D | Pi (t̄)]] = N [[D | begin local ūi := t̄; Si end]]for i = 1, . .
.,Sn.∞(iii) M[[D | S]] = k=0 M[[S k ]].Proof. See Exercise 5.2.⊓⊔Note that, as in Chapter 4, each S k is a statement without procedure calls.5.3 VerificationThe notions of partial and total correctness of the recursive programs withparameters are defined as in Chapter 4. First, we introduce the following rulethat deals with the block statement:1585 Recursive Programs with ParametersRULE 10: BLOCK{p} x̄ := t̄; S {q}{p} begin local x̄ := t̄; S end {q}where {x̄} ∩ f ree(q) = ∅.Example 5.5.
Let us return to the programbegin local x := x + 1; y := x end; begin local x := x + 1; z := x end.Denote it by S. We prove {true} S {y = z}. It is straightforward to derive{x + 1 = u} x := x + 1; y := x {y = u}.By the above block rule, we then obtain{x + 1 = u} begin local x := x + 1; y := x end {y = u}.Applying next the invariance rule with x + 1 = u and (a trivial instance of)the consequence rule we derive{x + 1 = u} begin local x := x + 1; y := x end {y = u ∧ x + 1 = u}.(5.3)Similarly, we can derive{x + 1 = u} begin local x := x + 1; z := x end {z = u}.Applying to this latter correctness formula the invariance rule with y = uand the consequence rule we obtain{y = u ∧ x + 1 = u} begin local x := x + 1; z := x end {y = z}.(5.4)By the composition rule applied to (5.3) and (5.4), we obtain{x + 1 = u} S {y = z},from which the desired result follows by an application of the ∃-introductionrule (to eliminate the variable u in the precondition), followed by a trivialapplication of the consequence rule.⊓⊔Partial Correctness: Non-recursive ProceduresConsider now partial correctness of recursive programs.
The main issue ishow to deal with the parameters of procedure calls. Therefore, to focus on5.3 Verification159this issue we discuss the parameters of non-recursive procedures first. Thefollowing copy rule shows how to prove correctness of non-recursive methodcalls:{p} begin local ū := t̄; S end {q}{p} P (t̄) {q}where P (ū) :: S ∈ D .Example 5.6. Let D contain the following declarationadd(x) :: sum := sum + x.It is straightforward, using the above block rule, to derive{sum = z} begin local x := 1; sum := sum + x end {sum = z + 1}and, similarly,{sum = z + 1} begin local x := 2; sum := sum + x end {sum = z + 3}.By applying the above copy rule we then derive{sum = z} add(1) {sum = z + 1}and{sum = z + 1} add(2) {sum = z + 3}.We conclude{sum = z} add(1); add(2) {sum = z + 3}using the composition rule.⊓⊔In many cases, however, we can also prove procedure calls correct by instantiating generic procedure calls, instead of proving for each specific call itscorresponding block statement correct.
By a generic call of a procedure P wemean a call of the form P (x̄), where x̄ is a sequence of fresh variables whichrepresent the actual parameters. Instantiation of such calls is then taken careof by the following auxiliary proof rule that refers to the set of proceduredeclarations D :RULE 11: INSTANTIATION{p} P (x̄) {q}{p[x̄ := t̄]} P (t̄) {q[x̄ := t̄]}1605 Recursive Programs with Parameterswhere var(x̄)∩var(D) = var(t̄)∩change(D) = ∅. The set change(D) denotesall the global variables that can be modified by the body of some proceduredeclared by D.Example 5.7. Let again D contain the following declarationadd(x) :: sum := sum + x.In order to prove{sum = z} add(1); add(2) {sum = z + 3}we now introduce the following correctness formula{sum = z} add(y) {sum = z + y}of a generic call add(y). We can derive this correctness formula from{sum = z} begin local x := y; sum := sum + x end {sum = z + y}by an application of the above copy rule. By the instantiation rule, we thenobtain{sum = z} add(1) {sum = z + 1} and {sum = z} add(2) {sum = z + 2},instantiating y by 1 and 2, respectively, in the above correctness formula ofthe generic call add(y).
An application of the substitution rule, replacing zin {sum = z} add(2) {sum = z + 2} by z + 1, followed by an application ofthe consequence rule, then gives us{sum = z + 1} add(2) {sum = z + 3}.We conclude{sum = z} add(1); add(2) {sum = z + 3}using the composition rule.⊓⊔Suppose now that we established {p} S {q} in the sense of partial correctness for a while program S and that S is the body of a procedureP , i.e., that P (ū) :: S is a given procedure declaration. Can we conclude then {p} P (ū) {q}? The answer is of course, ‘no’.
Take for exampleS ≡ u := 1. Then {u = 0} S {u = 1} holds, but the correctness formula{u = 0} P (ū) {u = 1} is not true. In fact, by the semantics of the procedurecalls, {u = 0} P (ū) {u = 0} is true. However, we cannot derive this formulaby an application of the copy rule because the proof rule for block statementsdoes not allow the local variable u to occur (free) in the postcondition. The5.3 Verification161following observation identifies the condition under which the above conclusion does hold.Lemma 5.2. (Transfer) Consider a while program S and a procedure Pdeclared by P (ū) :: S.
Suppose that ⊢ {p} S {q} and var(ū) ∩ change(S) = ∅.Then{p} P (ū) {q}can be proved in the proof system PRP.Proof. Let x̄ be a sequence of simple variables of the same length as ū suchthat var(x̄) ∩ var(p, S, q) = ∅. By the parallel assignment axiom 2′ ,{p[ū := x̄]} ū := x̄ {p ∧ ū = x̄}.Further, by the assumption about ū and the invariance rule,{p ∧ ū = x̄} S {q ∧ ū = x̄},so by the composition rule,{p[ū := x̄]} ū := x̄; S {q ∧ ū = x̄}.But q ∧ ū = x̄ → q[ū := x̄], so by the consequence rule,{p[ū := x̄]} ū := x̄; S {q[ū := x̄]}.Further var(ū) ∩ f ree(q[ū = x̄]) = ∅, so by the block rule 10,{p[ū := x̄]} begin local ū := x̄; S end {q[ū := x̄]}.Hence by the above copy rule,{p[ū := x̄]} P (x̄) {q[ū := x̄]}.Now note that var(x̄)∩var(p, q) = ∅ implies both p[ū := x̄][x̄ := ū] ≡ p andq[ū := x̄][x̄ := ū] ≡ q.
Moreover, by the assumption var(ū) ∩ change(S) = ∅,so by the instantiation rule 11 {p} P (ū) {q}.⊓⊔It should be noted that the use of the instantiation rule is restricted. Itcannot be used to reason about a call P (t̄), where some variables appearingin t̄ are changed by the body of P itself.Example 5.8. Let again D contain the declarationadd(x) :: sum := sum + x.We cannot obtain the correctness formula{sum = z} add(sum) {sum = z + z}1625 Recursive Programs with Parametersby instantiating some assumption about a generic call add(y) because sumis changed by the body of add.⊓⊔Partial Correctness: Recursive ProceduresWhen we deal only with one recursive procedure and use the procedure callas the considered recursive program, the above copy rule needs to be modifiedto{p} P (t̄) {q} ⊢ {p} begin local ū := t̄; S end {q}{p} P (t̄) {q}where D = P (ū) :: S.The provability relation ⊢ here refers to the axioms and proof rules ofthe proof system PW extended with the block rule 10, and appropriatelymodified auxiliary axioms and proof rules introduced in Section 3.8.
Thismodification consists of a reference to the extended set change(S), as definedin Section 4.3. Note that the presence of procedure calls with parametersdoes not affect the definition of change(S).In the case of a program consisting of mutually recursive procedure declarations we have the following generalization of the above rule.RULE 12: RECURSION III{p1 } P1 (t̄1 ) {q1 }, . . .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
