3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 34
Текст из файла (страница 34)
5.5 Proof outline establishing termination of the Quicksort procedure.The application of the consequence rule preceding the first recursive call ofQuicksort is justified by the following two implications:(n − m = z ∧ m < n ∧ v − m < n − m) → max(v − m, 0) < z,(n − m = z ∧ m < n ∧ n − w < n − m) → max(n − w, 0) < z.This completes the proof of Claim 3.⊓⊔Applying now the simplified version of the recursion IV rule we derive Q4.In summary, we have provedPT4 ⊢ Q4.1825 Recursive Programs with Parameters5.5 Exercises5.1. Call a recursive program proper when its sets of local and globalvariables are disjoint, and safe when for all procedures no formal parameter appears in an actual parameter and for all its block statementsbegin local x̄ := t̄; S end we have var(x̄) ∩ var(t̄) = ∅.Suppose that< S, σ > →∗ < R, τ >,where σ is a proper state. Prove the following two properties of recursiveprograms.(i) If S is proper, then so is R.(ii) If S is safe, then so is R.5.2.
Prove the Input/Output Lemma 5.1.5.3. Prove the Block Lemma 5.4.5.4. Prove the Change and Access Lemma 5.5.5.5. Prove the Soundness Theorem 5.4.5.6. This exercise considers the modularity rule 12 ′ introduced in Section 5.3.(i) Prove that this rule is a derived rule, in the sense that every proof ofpartial correctness that uses it can be converted into a proof that usesthe recursion III rule instead. Conclude that this proof rule is sound inthe sense of partial correctness.(ii) Suggest an analogous modularity proof rule for total correctness.5.7.
Prove the Soundness Theorem 5.5 for the proof system TRP.5.8. Consider the P artition procedure defined in Section 5.5. Prove the correctness formulas P1–P3 and PT4 for the procedure call P artition(m, n)using the properties P1–P4 and T of the while program P ART from Section 3.9 and the Transfer Lemma 5.2.5.9.
Allow the failure statements in the main statements and procedure bodies. Add to the proof systems PRP and TRP the corresponding failure rulesfrom Section 3.7 and prove the counterparts of the Soundness Corollary 5.1and Soundness Theorem 5.5.5.6 Bibliographic RemarksThe usual treatment of parameter mechanisms involves appropriate renamingof local variables to avoid variable clashes, see, e.g., Apt [1981]. The semantics5.6 Bibliographic Remarks183and proof theory of the call-by-value parameter mechanism adopted hereavoids any renaming and seems to be new. Recursion IV rule is a modificationof the corresponding rule from America and de Boer [1990].For other parameter mechanisms like call-by-name (as in ALGOL) or callby-reference (as in Pascal) a renaming of local variables in procedure bodiesis unavoidable to maintain the static scope of variables. In Olderog [1981] aproof system for programs with procedures having call-by-name parametersis presented, where local variables are renamed whenever the block of a procedure body is entered.
This mimicks the copy rule of ALGOL 60, see, e.g.,Grau, Hill, and Langmaack [1967].Clarke investigated programs with a powerful ALGOL-like proceduremechanism where recursive procedures can take procedures as parameters;in Clarke [1979] he showed that for such programs it is impossible to obtaina complete Hoare-style proof system even if —different from this book— onlylogical structures with finite data domains are considered. Clarke’s article initiated an intense research on the question of whether complete Hoare-styleproof systems could be obtained for programs with a restricted ALGOL-likeprocedure mechanism.
For program classes with complete proof systems see,for example, Olderog [1981,1983a,1984] and Damm and Josko [1983]. An interesting survey over these results on completeness of Hoare’s logic can befound in Clarke [1985].The algorithm Quicksort is due to Hoare[1961a,1962].
The first proof ofpartial correctness of Quicksort is given in Foley and Hoare [1971]. Thatproof establishes the permutation and the sorting property simultaneously,in contrast to our modular approach. For dealing with recursive procedures,Foley and Hoare [1971] use proof rules corresponding to our rules for blocks,instantiation, and recursion III rule for the case of one recursive procedure.They also use a so-called adaptation rule of Hoare [1971a] that allows oneto adapt a given correctness formula about a program to other pre- andpostconditions. In our approach we use several auxiliary rules which togetherhave the same effect as the adaptation rule. The expressive power of theadaptation rule has been analyzed in Olderog [1983b].
No proof rule for thetermination of recursive procedures is proposed in Foley and Hoare [1971],only an informal argument is given why Quicksort terminates. In Kaldewaij[1990] a correctness proof of a non-recursive version of Quicksort is given.6 Object-Oriented Programs6.16.26.36.46.56.66.76.86.96.106.11ISyntax . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Assertions . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . .Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Adding Parameters . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Transformation of Object-Oriented Programs . . . . . . . . . .Object Creation . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . .Case Study: Zero Search in Linked List . . . . . . . . . . . . . . .Case Study: Insertion into a Linked List . . . . . . . . . . . . . .Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Bibliographic Remarks . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . .187192197200206211217226232238240N THIS CHAPTER we study the verification of object-oriented programs. We focus on the following main characteristics of objects:• objects possess (and encapsulate) their own local variables,• objects interact via method calls,• objects can be dynamically created.In contrast to the formal parameters of procedures and the local variables ofblock statements which only exist temporarily, the local variables of an object exist permanently. To emphasize the difference between these temporaryvariables and the local variables of an object, the latter are called instancevariables.
The local state of an object is a mapping that assigns values toits instance variables. Each object represents its local state by a pointer to1851866 Object-Oriented Programsit. Encapsulation means that the instance variables of an object cannot bedirectly accessed by other objects; they can be accessed only via method callsof the object.A method call invokes a procedure which is executed by the called object.The execution of a method call thus involves a temporary transfer of controlfrom the local state of the caller object to that of the called object (alsoreferred to by callee).
Upon termination of the method call the control returnsto the local state of the caller. The method calls are the only way to transfercontrol from one object to another.We start in Section 6.1 by defining the syntax of the object-oriented programming language. We first restrict the language to simple method callswhich do not involve parameters. In Section 6.2 we introduce the corresponding operational semantics. This requires an appropriate extension ofthe concept of a state to properly deal with objects and instance variables.In Section 6.3 we introduce the syntax and semantics of the assertionlanguage. Expressions of the programming language only refer to the localstate of the executing object.
We call them local expressions. In order toexpress global properties we introduce in the assertion language a new kindof expression which allow us to navigate through the local object states. Wecall them global expressions.Next, in Section 6.4, we introduce a new assignment axiom for the instancevariables. The rules for partial and total correctness of recursive procedurecalls with parameters (as described in Chapter 5) are naturally extended tomethod calls.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
