3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 43
Текст из файла (страница 43)
First, we calculateq0 [next := u] ≡ ∀n ≥ 0 : if a[n] 6= a[k] then t(n, u) = a[n + 1] fi,where t(n, u) ≡ if a[n] = this then u else a[n].next fi. Next we observe thatq1 ∧ this = a[k].next ∧ n ≥ 0 implies a[n] 6= this and a[n] 6= this impliest(n, u) = a[n].next. Replacing t(n, u) in q0 [next := u] by a[n].next we obtainq0 itself. From this we conclude(q0 ∧ q1 ∧ this = a[k].next) → q0 [next := u].6.9 Case Study: Insertion into a Linked List237By the assignment axiom for instance variables and the consequence rule, wetherefore derive the correctness formula{q0 ∧ q1 ∧ this = a[k].next} next := u {q0 }.(6.9)Next, we calculateq1 [next := u] ≡ ∀n ≥ 0 : a[n] 6= t(k, u),where t(k, u) ≡ if a[k] = this then u else a[k].next fi. Note that q1 ∧ k ≥0 ∧ this = a[k].next implies a[k] 6= this and a[k] 6= this implies t(k, u) =a[k].next.
Replacing t(k, u) in q1 [next := u] by a[k].next we obtain q1 itself.From this we conclude(q1 ∧ k ≥ 0 ∧ this = a[k].next) → q1 [next := u].By the assignment axiom for instance variables and the consequence rule, wethus derive the correctness formula{q1 ∧ k ≥ 0 ∧ this = a[k].next} next := u {q1 }.(6.10)Finally, we calculateq2 [next := u] ≡ if this = t(k, u) then u else t(k, u).next fi = a[k + 1].As already inferred above, we have that q1 ∧ k ≥ 0 ∧ this = a[k].next impliest(k, u) = a[k].next. Replacing t(k, u) in q2 [next := u] by a[k].next we obtainthe assertionif this = a[k].next then u else a[k].next.next fi = a[k + 1]which is clearly implied by this = a[k].next ∧ u = a[k + 1].
From this weconclude(q1 ∧ k ≥ 0 ∧ this = a[k].next ∧ u = a[k + 1]) → q2 [next := u].By the assignment axiom for instance variables and the consequence rule, wethus derive the correctness formula{q1 ∧ k ≥ 0 ∧ this = a[k].next ∧ u = a[k + 1]} next := u {q2 }.(6.11)Applying the conjunction rule to the correctness formulas (6.9), (6.10) and(6.11) finally gives us the desired result.⊓⊔2386 Object-Oriented Programs6.10 Exercises6.1.
Compute(i) σ[a[0] := 1](y.a[x]) where y, x ∈ V ar and a ∈ IV ar,(ii) σ[x := σ(this)][y := 0](x.y) where x ∈ V ar and y ∈ IV ar,(iii) σ[σ(this) := τ [x := 0]](x), where x ∈ IV ar,(iv) σ(y.next.next).6.2. Compute(i) (z.x)[x := 0],(ii) (z.a[y])[a[0] := 1],(iii) (this.next.next)[next := y].6.3. Prove the Substitution Lemma 6.2.6.4. Given an instance variable x and the method getx to get its value definedbygetx :: r := x,where r is a normal variable, prove{true} y.getx {r = y.x}.6.5. Given the method definitioninc :: count := count + 1,where count is an instance integer variable, prove{up.count = z} up.inc {up.count = z + 1},where z is a normal variable.6.6. Let next be an instance object variable and r be a normal object variable.The following method returns the value of next:getnext :: r := next.Prove{next.next = z}next.getnext; next := r{next = z},where z is a normal object variable.6.7.
We define the method insert byinsert(u) :: u.setnext(next); next := u,where next is an instance object variable, u is a normal object variable andsetnext is defined by6.10 Exercises239setnext(u) :: next := u.Prove{z = next} this.insert(x) {next = x ∧ x.next = z},where x and z are normal object variables.6.8. To compute the sum of the instance integer variables val we used inExample 6.4 a normal integer variable sum, a normal object variable currentthat points to the current object, and two methods, add and move, definedas follows:add :: sum := sum + val,move :: current := next.Then the following main statement S computes the desired sum:S ≡ sum := 0;current := f irst;while current 6= null do current.add; current.move od.Let a be a normal array variable of type integer → object and the assertionsp and q be defined byp ≡ a[0] = f irst∧a[n] = null∧∀i ∈ [0 : n−1] : a[i] 6= null∧a[i].next = a[i+1]andq ≡ sum =n−1Xa[i].i=0Prove {p} S {q} in the sense of both partial and total correctness.6.9.
Prove the Translation Lemma 6.3.6.10. Prove the Correspondence Lemma 6.4.6.11. Prove the Transformation Lemma 6.5.6.12. Prove the Correctness Theorem 6.1.6.13. Prove the Assertion Lemma 6.6.6.14. Prove the Translation Lemma 6.7.6.15. Prove the Translation Lemma 6.8.6.16. Prove the Translation of Correctness Proofs of Statements Lemma 6.9.6.17. Prove the Translation Corollary 6.2.6.18. Prove Lemma 6.10.2406 Object-Oriented Programs6.19. Prove the Substitution for Object Creation Lemma 6.11.6.20. Prove the Conditional Expressions Lemma 6.12.6.21.
Prove Theorem 6.3.6.22. Given the normal array variable a of type integer → object and thenormal integer variable n, let the assertion p be defined byp ≡ ∀i ∈ [0 : n] : ∀j ∈ [0 : n] : if i 6= j then a[i] 6= a[j] fi.Prove{p} n := n + 1; a[n] := new {p}.6.11 Bibliographic RemarksDahl and Nygaard [1966] introduced in the 1960s the first object-orientedprogramming language called Simula. The language Smalltalk introduced inthe 1970s strictly defines all the basic computational concepts in terms ofobjects and method calls. Currently, one of the most popular object-orientedlanguages is Java.The proof theory for recursive method calls presented here is based on deBoer [1991b].
Pierik and de Boer [2005] describe an extension to the typicalobject-oriented features of inheritance and subtyping. There is a large literature on assertional proof methods for object-oriented languages, notablyfor Java. For example, Jacobs [2004] discusses a weakest pre-condition calculus for Java programs with JML annotations. The Java Modeling Language(JML) can be used to specify Java classes and interfaces by adding annotations to Java source files.
An overview of its tools and applications is discussedin Burdy et al. [2005]. In Huisman and Jacobs [2000] a Hoare logic for Javawith abnormal termination caused by failures is described.Object-oriented programs in general give rise to dynamically evolvingpointer structures as they occur in programming languages like Pascal. Thereis a large literature on logics dealing in different ways with the problem ofaliasing. One of the early approaches to reasoning about linked data structures is described in Morris [1982]. A more recent approach is that of separation logic described in Reynolds [2002]. Abadi and Leino [2003] introduce aHoare logic for object-oriented programs based on a global store model whichprovides an explicit treatment of aliasing and object creation in the assertion language.
Banerjee and Naumann [2005] further discuss restrictions onaliasing to ensure encapsulation of classes in an object-oriented programminglanguage with pointers and subtyping.Recent work on assertional methods for object-oriented programming languages by Barnett et al. [2005] focuses on object invariants and a corresponding methodology for modular verification. Müller, Poetzsch-Heffter and6.11 Bibliographic Remarks241Leavens [2006] also introduce a class of invariants which support modularreasoning about complex object structures.There exist a number of tools based on theorem provers which assist in(semi-)automated correctness proofs of object-oriented programs.
In particular, Flanagan et al. [2002] describe ECS/Java (Extended Static Checker forJava) which supports the (semi-)automated verification of annotated Javaprograms. The KeY Approach of Beckert, Hähnle and Schmitt [2007] to theverification of object-oriented software is based on dynamic logic.Part IIIParallel Programs7 Disjoint Parallel Programs7.17.27.37.47.57.6ASyntax . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Case Study: Find Positive Element . . . . . . . . . . . . . . .
. . . .Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Bibliographic Remarks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .247248253261264266S WE HAVE seen in Chapter 1, concurrent programs can be quitedifficult to understand in detail. That is why we introduce and studythem in several stages. In this part of the book we study parallel programs,and in this chapter we investigate disjoint parallelism, the simplest form ofparallelism. Disjointness means here that the component programs have onlyreading access to common variables.Many phenomena of parallel programs can already be explained in thissetting.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
