3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 25
Текст из файла (страница 25)
In thischapter we introduce parameterless procedures and in the next chapter procedures with parameters. This allows us to focus first on recursion, an important and powerful concept. To deal with it we need to modify appropriatelythe methods introduced in the previous chapter.We start by defining in Section 4.1 the syntax of programs in the context ofa set of declarations of parameterless recursive procedures. We call such programs recursive programs. In Section 4.2 we extend the semantics introduced1271284 Recursive Programsin Section 3.2 to recursive programs. Thanks to our focus on operationalsemantics, such an extension turns out to be very simple.Verification of recursive programs calls for a non-trivial extension of theapproach introduced in Section 3.3.
In Section 4.3 we deal with partial correctness and total correctness. In each case we introduce proof rules that referin their premises to proofs. Then, as a case study, we consider in Section 4.5the correctness of a binary search program.4.2 Semantics1294.1 SyntaxGiven a set of procedure identifiers, with typical elements P, P1 , . . ., we extendthe syntax of while programs studied in Chapter 3 by the following clause:S ::= P.A procedure identifier used as a subprogram is called a procedure call.
Procedures are defined by declarations of the formP :: S.In this context S is called the procedure body. Recursion refers here to thefact that the procedure body S of P can contain P as a subprogram. Suchoccurrences of P are called recursive calls. From now on we assume a given setof procedure declarations D such that each procedure that appears in D has aunique declaration in D. To keep notation simple we omit the “{ }” bracketswhen writing specific sets of declarations, so we write P1 :: S1 , . . ., Pn :: Sninstead of {P1 :: S1 , . .
., Pn :: Sn }.A recursive program consists of a main statement S built according to thesyntax of this section and a given set D of (recursive) procedure declarations.All procedure calls in the main statement refer to procedures that are declaredin D. If D is clear from the context we refer to the main statement as arecursive program.Example 4.1. Using this syntax the declaration of the proverbial factorialprogram can be written as follows:F ac :: if x = 0 then y := 1 else x := x − 1; F ac; x := x + 1; y := y · x fi.(4.1)A main statement in the context of this declaration is the procedure callF ac.⊓⊔4.2 SemanticsWe define the semantics of recursive programs by extending the transitionsystem for while programs by the following transition axiom:(viii) < P, σ > → < S, σ >, where P :: S ∈ D.This axiom captures the meaning of a procedure call by means of a copyrule, according to which a procedure call is dynamically replaced by thecorresponding procedure body.The concepts introduced in Definition 3.1, in particular that of a computation, extend in an obvious way to the current setting.1304 Recursive ProgramsExample 4.2.
Assume the declaration (4.1) of the factorial program. Thenwe have the following computation of the main statement F ac, where σ is aproper state with σ(x) = 2:→→→→→→→→→→→→→< F ac, σ >< if x = 0 then y := 1 else x := x − 1; F ac;x := x + 1; y := y · x fi, σ >< x := x − 1; F ac; x := x + 1; y := y · x, σ >< F ac; x := x + 1; y := y · x, σ[x := 1] >< if x = 0 then y := 1 else x := x − 1; F ac; x := x + 1; y := y · x fi;x := x + 1; y := y · x, σ[x := 1] >< x := x − 1; F ac; x := x + 1; y := y · x;x := x + 1; y := y · x, σ[x := 1] >< F ac; x := x + 1; y := y · x; x := x + 1; y := y · x, σ[x := 0] >< if x = 0 then y := 1 else x := x − 1; F ac; x := x + 1; y := y · x fi;x := x + 1; y := y · x; x := x + 1; y := y · x, σ[x := 0] >< y := 1; x := x + 1; y := y · x; x := x + 1; y := y · x, σ[x := 0] >< x := x + 1; y := y · x; x := x + 1; y := y · x, σ[y, x := 1, 0] >< y := y · x; x := x + 1; y := y · x, σ[y, x := 1, 1] >< x := x + 1; y := y · x, σ[y, x := 1, 1] >< y := y · x, σ[y := 1] >< E, σ[y := 2] >⊓⊔Definition 4.1.
Recall that we assumed a given set of procedure declarations D. We now extend two input/output semantics originally introducedfor while programs to recursive programs by using the transition relation→ defined by the axioms and rules (i)–(viii):(i) the partial correctness semantics defined byM[[S]](σ) = {τ |< S, σ > →∗ < E, τ >},(ii) the total correctness semantics defined byMtot [[S]](σ) = M[[S]](σ) ∪ {⊥ | S can diverge from σ}.⊓⊔Example 4.3. Assume the declaration (4.1) of the factorial procedure. Thenthe following hold for the main statement F ac:4.2 Semantics131• if σ(x) ≥ 0 thenM[[F ac]](σ) = Mtot [[F ac]](σ) = {σ[y := σ(x)!]},where for n ≥ 0, the expression n! denotes the factorial of n, i.e., 0! = 1and for n > 0, n! = 1 · . .
. · n,• if σ(x) < 0 thenM[[F ac]](σ) = ∅ and Mtot [[F ac]](σ) = {⊥}.⊓⊔Properties of the SemanticsIn the Input/Output Lemma 3.3(v) we expressed the semantics of loops interms of a union of semantics of its finite syntactic approximations. An analogous observation holds for recursive programs. In this lemma we refer todifferent sets of procedure declarations. To avoid confusion we then writeD | S when we consider S in the context of the set D of procedure declarations.Recall that Ω is a while program such that for all proper states σ,M[[Ω]](σ) = ∅. Given a declaration D = P1 :: S1 , .
. . , Pn :: Sn and a recursiveprogram S, we define the kth syntactic approximation S k of S by inductionon 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 inS of each procedure identifier Pi by the statement Ri . Furthermore, let Dkabbreviate P1 :: S1k , .
. . , Pn :: Snk and let N stand for M or Mtot . Thefollowing lemma collects the properties of N we need.Lemma 4.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 ]] = N [[D | Si ]] for i = 1, .
. ., n.S∞(iii) M[[D | S]] = k=0 M[[S k ]].Proof. See Exercise 4.3.⊓⊔Note that each S k is a while statement, that is a program without procedure calls.1324 Recursive Programs4.3 VerificationPartial CorrectnessLet S be the main statement of a recursive program in the context of a setD of procedure declarations. As in the case of while programs we say thatthe correctness formula {p} S {q} is true in the sense of partial correctness,and write |= {p} S {q}, ifM[[S]]([[p]]) ⊆ [[q]].Assuming D = P1 :: S1 , .
. . , Pn :: Sn , in order to prove |= {p} S {q} wefirst proveA ⊢ {p} S {q}for some sequenceA ≡ {p1 } P1 {q1 }, . . . , {pn } Pn {qn }of assumptions. Then to discharge these assumptions we additionally provethat for all i = 1, . . . , nA ⊢ {pi } Si {qi }.We summarize these two steps by the following proof rule:RULE 8: RECURSION{p1 } P1 {q1 }, . .
. , {pn } Pn {qn } ⊢ {p} S {q},{p1 } P1 {q1 }, . . . , {pn } Pn {qn } ⊢ {pi } Si {qi }, i ∈ {1, . . ., n},{p} S {q}where D = P1 :: S1 , . . . , Pn :: Sn .The intuition behind this rule is as follows. Say that a program S is (p, q)correct if {p} S {q} holds in the sense of partial correctness. The secondpremise of the rule states that we can establish for i = 1, .
. . , n the (pi , qi )correctness of the procedure bodies Si from the assumption of the (pi , qi )correctness of the procedure calls Pi , for i = 1, . . . , n. Then we can prove the(pi , qi )-correctness of the procedure calls Pi unconditionally, and thanks tothe first premise establish the (p, q)-correctness of the recursive program S.We still have to clarify the meaning of the ⊢ provability relation thatwe use in the rule premises. In these proofs we allow the axioms and proofrules of the proof system PW, and appropriately modified auxiliary axiomsand proof rules introduced in Section 3.8.
This modification consists of theadjustment of the conditions for specific variables so that they now also refer4.3 Verification133to the assumed set of procedure declarations D. To this end, we first extendthe definition of change(S).Recall that the set change(S) consisted of all simple and array variablesthat can be modified by S. This suggests the following extension of change(S)to recursive programs and sets of procedure declarations:change(P :: S) = change(S),change({P :: S} ∪ D) = change(P :: S) ∪ change(D),change(P ) = ∅.Then we modify the auxiliary axioms and proof rules by adding the restriction that specific variables do not occur in change(D). For example, theinvariance axiom A2 now reads{p} S {p}where f ree(p) ∩ (change(D) ∪ change(S)) = ∅.To prove partial correctness of recursive programs we use the followingproof system PR:PROOF SYSTEM PR :This system consists of the group of axiomsand rules 1–6, 8, and A2–A6.Thus PR is obtained by extending the proof system PW by the recursion rule8 and the auxiliary rules A2–A6 where we use the versions of auxiliary rulesmodified by change(D) as explained above.In the actual proof not all assumptions about procedure calls are needed,only those assumptions that do appear in the procedure body.
In particular,when we deal only with one recursive procedure and use the procedure callas the considered recursive program, the recursion rule can be simplified to{p} P {q} ⊢ {p} S {q}{p} P {q}where D = P :: S.Further, when the procedure P is not recursive, that is, its procedurebody S does not contain any procedure calls, the above rule can be furthersimplified to{p} S {q}{p} P {q}It is straightforward how to extend the concept of a proof outline to thatof a proof outline from a set of assumptions being correctness formulas: wesimply allow each assumption as an additional formation axiom. Now, the1344 Recursive Programspremises of the considered recursion rule and all subsequently introducedrecursion rules consist of the correctness proofs.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
