3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 28
Текст из файла (страница 28)
4.4 Proof outline showing partial correctness of the BinSearch procedure.while the second implication holds, sincef irst ≤ last ∧ mid = (f irst + last) div 2 → f irst ≤ mid ≤ last.It remains to clarify two applications of the consequence rules. To dealwith the one used in the then branch of the if -then-else statement notethe following implication that allows us to limit the search to a smaller arraysection:4.4 Case Study: Binary Search(sorted(a[f : l]) ∧ f ≤ m < l ∧ a[m] < val) →(∃x ∈ [m + 1 : l] : a[x] = val ↔ ∃x ∈ [f : l] : a[x] = val).147(4.10)Next, note thatf irst < last → (f irst + last) div 2 + 1 ≤ last,sop ∧ f irst 6= last → p[f := (f + l) div 2 + 1][f irst := (f + l) div 2 + 1].This explains the following sequence of implications:p ∧ mid = (f irst + last) div 2 ∧ f irst 6= last ∧ a[mid] < valp[f := (f + l) div 2 + 1][f irst := (f + l) div 2 + 1]∧ mid = (f + l) div 2 ∧ r1→ p[f := (f + l) div 2 + 1][f irst := mid + 1] ∧ r1→ (p[f := (f + l) div 2 + 1] ∧ r1 )[f irst := mid + 1].→Finally, observe that by (4.10) with m = (f + l) div 2 we get by thedefinition of q and r1q[f := (f + l) div 2 + 1] ∧ r1 → q.This justifies the first application of the consequence rule.
We leave the justification of the second application as Exercise 4.9. This completes the proofof partial correctness.Total CorrectnessTo deal with total correctness we use the proof methodology discussed inthe previous section. We have p → f irst ≤ last, so it suffices to prove{f irst ≤ last} BinSearch {true} in the sense of total correctness using thesimplified form of the recursion II rule.We uset ≡ last − f irstas the bound function. Then f irst ≤ last → t ≥ 0 holds, so it suffices toprove{f irst ≤ last ∧ t < z} BinSearch {true}⊢ {f irst ≤ last ∧ t = z} S {true}.We present the proof in the form of a proof outline that we give in Figure 4.5.
The two applications of the consequence rule used in it are justifiedby the following sequences of implications:1484 Recursive Programs{f irst ≤ last ∧ last − f irst = z}mid := (f irst + last) div 2;{f irst ≤ last ∧ last − f irst = z ∧ mid = (f irst + last) div 2}if f irst 6= lastthen{f irst < last ∧ last − f irst = z ∧ mid = (f irst + last) div 2}if a[mid] < valthen{f irst < last ∧ last − f irst = z ∧ mid = (f irst + last) div 2}{(f irst ≤ last ∧ last − f irst < z)[f irst := mid + 1]}f irst := mid + 1;{f irst ≤ last ∧ last − f irst < z}BinSearch{true}else{f irst < last ∧ last − f irst = z ∧ mid = (f irst + last) div 2}if a[mid] > valthen{f irst < last ∧ last − f irst = z ∧ mid = (f irst + last) div 2}{(f irst ≤ last ∧ last − f irst < z)[last := mid]}last := mid;{f irst ≤ last ∧ last − f irst < z}BinSearch{true}fi{true}fi{true}fi{true}Fig.
4.5 Proof outline showing termination of the BinSearch procedure.f irst < last ∧ last − f irst = z ∧ mid = (f irst + last) div 2→ f irst ≤ mid < last ∧ last − f irst = z→ mid + 1 ≤ last ∧ last − (mid + 1) < zandf irst < last ∧ last − f irst = z ∧ mid = (f irst + last) div 2→ f irst ≤ mid < last ∧ last − f irst = z→ f irst ≤ mid ∧ mid − f irst < z.4.5 Exercises149Further, the Boolean expressions a[mid] < val and a[mid] > val are irrelevantfor the proof, so drop them from the assertions of the proof outline.
(Formally,this step is justified by the last two formation rules for proof outlines.)This concludes the proof of termination.4.5 Exercises4.1. Using recursive procedures we can model the while B do S od loop asfollows:P :: if B then S; P fi.Assume the above declaration.(i) Prove that M[[while B do S od]] = M[[P ]].(ii) Prove that Mtot [[while B do S od]] = Mtot [[P ]].4.2. Let D = P1 :: S1 , . . . , Pn :: Sn .
Prove that Pi 0 = Ω and Pi k+1 = Sik fork ≥ 0.4.3. Prove the Input/Output Lemma 4.1.4.4. Intuitively, for a given set of procedure declarations a procedure is nonrecursive if it does not call itself, possibly through a chain of calls of otherprocedures. Formalize this definition.Hint. Introduce the notion of a call graph in which the nodes are procedureidentifiers and in which a directed arc connects two nodes P and Q if thebody of P contains a call of Q.4.5. Prove the Soundness Theorem 4.1.4.6. Prove the Soundness Theorem 4.3.4.7. Prove the Instantiation Theorem 4.4.4.8.
Prove the Fresh Variable Lemma 4.2.4.9. Consider the BinSearch program studied in Section 4.5. Complete theproof of partial correctness discussed there by justifying the application ofthe consequence rule used in the proof outline of the else branch.4.10. Consider the following iterative version of the BinSearch program studied in Section 4.5:BinSearch ≡ mid := (f irst + last) div 2;while f irst 6= last ∧ a[mid] 6= val doif a[mid] < val1504 Recursive Programsthen f irst := mid + 1else last := midfi;mid := (f irst + last) div 2odProve partial and total correctness of this program w.r.t.
the pre- and postconditions used in Section 4.5.4.11. Allow the failure statements in the main statements and procedurebodies. Add to the proof systems PR and TR the corresponding failure rulesfrom Section 3.7 and prove the counterparts of the Soundness Corollary 4.1and Soundness Corollary 4.2.4.6 Bibliographic RemarksProcedures (with parameters) were initially introduced in the programminglanguage FORTRAN.
However, recursion was not allowed. Recursive procedures were first introduced in ALGOL 60. Their semantics was defined by theso-called copy rule. For the case of parameterless procedures this rule saysthat at runtime a procedure call is treated like the procedure body insertedat the place of call, see, e.g., Grau, Hill, and Langmaack [1967].Historically, reasoning about recursive programs focused initially on recursive program schemes and recursively defined functions, see, e.g., Loeckxand Sieber [1987]. The recursion rule is modelled after the so-called Scottinduction rule that appeared first in the unpublished manuscript Scott andde Bakker [1969].Example 4.4 is taken from Apt [1981]. It is also shown there that the considered proof system for partial correctness is incomplete if in the subsidiaryproofs used in the premises of the recursion rule only the axioms and proofrules of the PW proof system are used.
This clarifies why in Example 4.4and in Section 4.5 we used in these subsidiary proofs the substitution andinvariance rules. Completeness of the resulting proof system for partial correctness is established in Apt [1981]. Recursion II rule is taken from Americaand de Boer [1990], where also the completeness of the proof system TR fortotal correctness is established.5 Recursive Programs with Parameters5.15.25.35.45.55.6NSyntax .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Case Study: Quicksort . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . .Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Bibliographic Remarks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .152154157172182182OW THAT WE understand the semantics and verification of recursive procedures without parameters, we extend our study to thecase of recursive procedures with parameters. The presentation follows theone of the last chapter. In Section 5.1 we introduce the syntax of recursiveprocedures with parameters. We deal here with the most common parametermechanism, namely call-by-value.
To properly capture its meaning we needto introduce a block statement that allows us to distinguish between localand global variables.In Section 5.2 we introduce the operational semantics that appropriatelymodifies the semantics of recursive procedures from the last chapter. Theblock statement is used to define the meaning of procedure calls.
Then, inSection 5.3 we focus on program verification. The approach is a modificationof the approach from the previous chapter, where the additional difficultyconsists of a satisfactory treatment of parameters. Finally, as a case study,we consider in Section 5.5 the correctness of the Quicksort program.1511525 Recursive Programs with Parameters5.1 SyntaxWhen considering recursive procedures with parameters we need to distinguish between local and global variables. To this end, we consider an extension of the syntax of while programs studied in Chapter 3 in which a blockstatement is allowed. It is introduced by the following clause:S ::= begin local x̄ := t̄; S1 end.Informally, a block statement introduces a non-empty sequence of localvariables, all of which are explicitly initialized by means of a parallel assignment, and provides an explicit scope for these local variables.
The preciseexplanation of a scope is more complicated because the block statements canbe nested.Assuming x̄ = x1 , . . ., xk and t̄ = t1 , . . ., tk , each occurrence of a localvariable xi within the statement S1 and not within another block statementthat is a subprogram of S1 refers to the same variable. Each such variablexi is initialized to the expression ti by means of the parallel assignmentx̄ := t̄. Further, given a statement S ′ such that begin local x̄ := t̄; S1 endis a subprogram of S ′ , all occurrences of xi in S ′ outside this block statementrefer to some other variable(s).
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
