3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 81
Текст из файла (страница 81)
, n}.B Axioms and Proof RulesRULE 39 ′ : FAIR REPETITION (IDENTICAL GUARDS)(1′ ) {p ∧ B} Si {p}, i ∈ {1, . . . , n},(2′ ) {p ∧ B ∧ z̄ ≥ 0 ∧ ∃zi ≥ 0 : t[zj := zj + 1]j6=i = α}Si{t < α}, i ∈ {1, . . . , n},(3′ ) p ∧ z̄ ≥ 0 → t ∈ W(4′ ) {p} do ¤ni=1 B → Si od {p ∧ ¬B}where conditions (i)–(v) of Rule 39 hold.467468B Axioms and Proof RulesAuxiliary Axioms and RulesRULE A1: DECOMPOSITION⊢p {p} S {q},⊢t {p} S {true}{p} S {q}where the provability signs ⊢p and ⊢t refer to proof systems for partial andtotal correctness for the considered program S, respectively.AXIOM A2: INVARIANCE{p} S {p}where f ree(p) ∩ change(S) = ∅.RULE A3: DISJUNCTION{p} S {q}, {r} S {q}{p ∨ r} S {q}RULE A4: CONJUNCTION{p1 } S {q1 }, {p2 } S {q2 }{p1 ∧ p2 } S {q1 ∧ q2 }RULE A5: ∃-INTRODUCTION{p} S {q}{∃x : p} S {q}where x does not occur in S or in f ree(q).RULE A6: INVARIANCE{r} S {q}{p ∧ r} S {p ∧ q}where f ree(p) ∩ change(S) = ∅.B Axioms and Proof Rules469RULE A7: SUBSTITUTION{p} S {q}{p[z̄ := t̄]} S {q[z̄ := t̄]}where ({z̄} ∩ var(S)) ∪ (var(t̄) ∩ change(S)) = ∅.RULE A8:I1 and I2 are global invariant relative to pI1 ∧ I2 is a global invariant relative to pRULE A9:I is a global invariant relative to p,{p} S {q}{p} S {I ∧ q}470B Axioms and Proof RulesAppendix C Proof SystemsFor the various classes of programs studied in this book the following proofsystems for partial and total correctness were introduced.while ProgramsPROOF SYSTEM PW :This system consists of the groupof axioms and rules 1–6.PROOF SYSTEM TW :This system consists of the groupof axioms and rules 1–4, 6, 7.Recursive ProgramsPROOF SYSTEM PR :This system consists of the group of axiomsand rules 1–6, 8, and A2–A6.PROOF SYSTEM TR :This system consists of the group of axiomsand rules 1–4, 6, 7, 9, and A3–A6.471472C Proof SystemsRecursive Programs with ParametersPROOF SYSTEM PRP :This system consists of the group of axiomsand rules 1–6, 10, 11, 12, and A2–A6.PROOF SYSTEM TRP :This system consists of the group of axiomsand rules 1–4, 6, 7, 10, 11, 13, and A3–A6.Object-Oriented ProgramsPROOF SYSTEM PO :This system consists of the group of axiomsand rules 1–6, 10, 14–16, and A2–A6.PROOF SYSTEM TO :This system consists of the group of axiomsand rules 1–4, 6, 7, 10, 14, 15, 17, and A3–A6.Object-Oriented Programs with ParametersPROOF SYSTEM POP :This system consists of the group of axiomsand rules 1–6, 10, 14, 18, 19, and A2–A6.PROOF SYSTEM TOP :This system consists of the group of axiomsand rules 1–4, 6, 7, 10, 14, 18, 20, and A3–A6.Object-Oriented Programs with Object CreationPROOF SYSTEM POC :This system consists of the group of axiomsand rules 1–6, 10, 14, 18, 19, 21, 22 and A2–A7.C Proof SystemsPROOF SYSTEM TOC :This system consists of the group of axiomsand rules 1–4, 6, 7, 10, 14, 18, 20–22 and A3–A7.Disjoint Parallel ProgramsPROOF SYSTEM PP :This system consists of the group of axiomsand rules 1–6, 24, 25 and A2–A6.PROOF SYSTEM TP :This system consists of the group of axiomsand rules 1–5, 7, 24, 25 and A3–A6.Parallel Programs with Shared VariablesPROOF SYSTEM PSV :This system consists of the group of axiomsand rules 1–6, 25–27 and A2–A6.PROOF SYSTEM TSV :This system consists of the group of axiomsand rules 1–5, 7, 25–27 and A3–A6.Parallel Programs with SynchronizationPROOF SYSTEM PSY :This system consists of the group of axiomsand rules 1–6, 25, 27, 28 and A2–A6.PROOF SYSTEM TSY :This system consists of the group of axiomsand rules 1–5, 7, 25, 28, 29 and A3–A6.473474C Proof SystemsNondeterministic ProgramsPROOF SYSTEM PN :This system consists of the group of axiomsand rules 1, 2, 3, 6, 30, 31 and A2–A6.PROOF SYSTEM TN :This system consists of the group of axioms and rules1, 2, 3, 6, 32, 33 and A3–A6.Distributed ProgramsPROOF SYSTEM PDP :This system consists of the proof system PN augmentedby the group of axioms and rules 34, A8 and A9.PROOF SYSTEM WDP :This system consists of the proof system TN augmentedby the group of axioms and rules 35 and A9.PROOF SYSTEM TDP :This system consists of the proof system TN augmentedby the group of axioms and rules 36 and A9.FairnessPROOF SYSTEM PNR :This system consists of the proof systemPN augmented with Axiom 37.PROOF SYSTEM TNR :This system is obtained from the proof system TNby adding Axiom 37 and replacing Rule 33 by Rule 38.PROOF SYSTEM FN :This system is obtained from the proof system TNby replacing Rule 33 by Rule 39.Appendix D Proof OutlinesThe following formation axioms and rules were used in this book to defineproof outlines.(i) {p} skip {p}(ii) {p[u := t]} u := t {p}(iii)(iv)(v)(vi)(vii){p} S1∗ {r}, {r} S2∗ {q}{p} S1∗ ; {r} S2∗ {q}{p ∧ B} S1∗ {q}, {p ∧ ¬B} S2∗ {q}{p} if B then {p ∧ B} S1∗ {q} else {p ∧ ¬B} S2∗ {q} fi {q}{p ∧ B} S ∗ {p}{inv : p} while B do {p ∧ B} S ∗ {p} od {p ∧ ¬B}p → p1 , {p1 } S ∗ {q1 }, q1 → q{p}{p1 } S ∗ {q1 }{q}{p} S ∗ {q}{p} S ∗∗ {q}where S ∗∗ results from S ∗ by omitting some of the intermediate assertions not labeled by the keyword inv.{p ∧ B} S ∗ {p},{p ∧ B ∧ t = z} S ∗∗ {t < z},(viii) p → t ≥ 0{inv : p}{bd : t} while B do {p ∧ B} S ∗ {p} od {p ∧ ¬B}475476D Proof Outlineswhere t is an integer expression and z is an integer variable not occurringin p, t, B or S ∗∗ .(ix)(x){pi } Si∗ {qi }, i ∈ {1, .
. . , n}VnVn{ i=1 pi } [{p1 } S1∗ {q1 }k. . .k{pn } Sn∗ {qn }] { i=1 qi }{p} S ∗ {q}{p} hS ∗ i {q}where S ∗ stands for an annotated version of S.(1) {p ∧ B} S ∗ {p} is standard,(2) {pre(R) ∧ t = z} R {t ≤ z} for every normalassignment and atomic region R within S,(3) for each path π ∈ path(S) there existsa normal assignment or atomic region R in π(xi)such that{pre(R) ∧ t = z} R {t < z},(4) p → t ≥ 0{inv : p}{bd : t} while B do {p ∧ B} S ∗ {p} od {p ∧ ¬B}where t is an integer expression and z is an integer variable not occurringin p, t, B or S ∗ , and where pre(R) stands for the assertion preceding Rin the standard proof outline {p ∧ B} S ∗ {p} for total correctness.(xii){p ∧ B} S ∗ {q}{p} await B then {p ∧ B} S ∗ {q} end {q}where S ∗ stands for an annotated version of S.Wnp → i=1 Bi ,∗(xiii) {p ∧ Bi } Si {q}, i ∈ {1, .
. . , n}{p} if ¤ni=1 Bi → {p ∧ Bi } Si∗ {q} fi {q}{p ∧ Bi } Si∗ {p}, i ∈ {1, . . . , n},{p ∧ Bi ∧ t = z} Si∗∗ {t < z}, i ∈ {1, . . . , n},(xiv) p → t ≥ 0{inv : p}{bd : t} do ¤ni=1 Bi → {p ∧ Bi } Si∗ {p} od {p ∧Vni=1¬Bi }where t is an integer expression and z is an integer variable not occurringin p, t, Bi or Si for i ∈ {1, . . . , n}.ReferencesM. Abadi and K. Leino[2003] A logic of object-oriented programs, in: Verification: Theory and Practice, N. Dershowitz, ed., vol. 2772 of Lecture Notes in Computer Science,Springer, pp. 11–41.
Cited on page 240.J.-R. Abrial[1996] The B Book – Assigning Programs to Meanings, Cambridge UniversityPress. Cited on page 371.[2009] Modeling in Event-B: System and Software Engineering, Cambridge University Press. To appear. Cited on page 371.J.-R. Abrial and S. Hallerstede[2007] Refinement, Decomposition and Instantiation of Discrete Models: Application to Event-B, Fundamentae Informatica, 77, pp. 1–28.
Cited on pages13 and 371.R. Alur and T. A. Henzinger[1994] Finitary fairness, in: Proceedings, Ninth Annual IEEE Symposium onLogic in Computer Science (LICS ’94), IEEE Computer Society Press,pp. 52–61. Cited on page 455.P. America[1987] Inheritance and subtyping in a parallel object-oriented language, in: European Conference on Object-Oriented Programming, (ECOOP), vol.
276 ofLecture Notes in Computer Science, Springer, pp. 234–242. Cited on page12.P. America and F. S. de Boer[1990] Proving total correctness of recursive procedures, Information and Computation, 84, pp. 129–162. Cited on pages 150 and 183.K. R. Apt[1981] Ten years of Hoare’s logic, a survey, part I, ACM Trans.
Prog. Lang. Syst.,3, pp. 431–483. Cited on pages 124, 125, 150, and 182.[1984] Ten years of Hoare’s logic, a survey, part II: nondeterminism, TheoreticalComput. Sci., 28, pp. 83–109. Cited on page 370.[1986] Correctness proofs of distributed termination algorithms, ACM Trans.Prog. Lang. Syst., 8, pp. 388–405. Cited on pages 15, 390, and 405.477478ReferencesK. R. Apt, F. S. de Boer, and E.-R. Olderog[1990] Proving termination of parallel programs, in: Beauty is Our Business, ABirthday Salute to Edsger W. Dijkstra, W.
H. J. Feijen, A. J. M. vanGasteren, D. Gries, and J. Misra, eds., Springer, New York, pp. 0–6. Citedon page 305.K. R. Apt, L. Bougé, and P. Clermont[1987] Two normal form theorems for CSP programs, Inf. Process. Lett., 26,pp. 165–171. Cited on page 405.K. R. Apt, N. Francez, and S. Katz[1988] Appraising fairness in distributed languages, Distributed Computing, 2,pp. 226–241. Cited on page 455.K. R. Apt, N.
Francez, and W. P. de Roever[1980] A proof system for communicating sequential processes, ACM Trans. Prog.Lang. Syst., 2, pp. 359–385. Cited on pages 12, 403, and 405.K. R. Apt and E.-R. Olderog[1983] Proof rules and transformations dealing with fairness, Sci. Comput. Programming, 3, pp. 65–100. Cited on pages 15 and 455.K. R.
Apt and G. D. Plotkin[1986] Countable nondeterminism and random assignment, J. Assoc. Comput.Mach., 33, pp. 724–767. Cited on page 455.K. R. Apt, A. Pnueli, and J. Stavi[1984] Fair termination revisited with delay, Theoretical Comput. Sci., 33, pp. 65–84. Cited on page 455.E. Ashcroft and Z. Manna[1971] Formalization of properties of parallel programs, Machine Intelligence, 6,pp. 17–41. Cited on page 370.R.-J. Back[1989] A method for refining atomicity in parallel algorithms, in: PARLE Conference on Parallel Architectures and Languages Europe, Lecture Notes inComputer Science 366, Springer, New York, pp.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
