3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 80
Текст из файла (страница 80)
. . , n}.Vn(xxiii) < do ⊓⊔ni=1 Bi → Si od, σ > → < E, σ > where σ |= i=1 ¬Bi .(xxiv) < do ¤mj=1 gj → Sj od, σ > → < E, σ >where for j ∈ {1, . . ., m} gj ≡ Bj ; αj and σ |=[S1′ k. . .kSn′ ], τ>(xxv) < [S1 k. . .kSn ], σ > → <where for some k, ℓ ∈ {1, . . ., n}, k 6= ℓVmj=1¬Bj .1Sk ≡ do ¤mj=1 gj → Rj od,2Sℓ ≡ do ¤mj=1 hj → Tj od,for some j1 ∈ {1, . . ., m1 } and j2 ∈ {1, . . ., m2 } the generalizedguards gj1 ≡ B1 ; α1 and hj2 ≡ B2 ; α2 match, and(1)(2)(3)(4)(5)σ |= B1 ∧ B2 ,M[[Eff (α1 , α2 )]](σ) = {τ },Si′ ≡ Si for i 6= k, ℓ,Sk′ ≡ Rj1 ; Sk ,Sℓ′ ≡ Tj2 ; Sℓ .(xxvi) < x :=?, σ > → < E, σ[x := d] > for every natural number d.Appendix B Axioms and Proof RulesThe following axioms and proof rules were used in the proof systems studiedin this book.AXIOM 1: SKIP{p} skip {p}AXIOM 2: ASSIGNMENT{p[u := t]} u := t {p}where u ∈ V ar or u ≡ a[s1 , .
. . , sn ], for a ∈ V ar.AXIOM 2 ′ : PARALLEL ASSIGNMENT{p[x̄ := t̄]} x̄ := t̄ {p}RULE 3: COMPOSITION{p} S1 {r}, {r} S2 {q}{p} S1 ; S2 {q}RULE 4: CONDITIONAL{p ∧ B} S1 {q}, {p ∧ ¬B} S2 {q}{p} if B then S1 else S2 fi {q}RULE 4 ′ : FAILURE{p ∧ B} S {q}{p} if B → S fi {q}459460B Axioms and Proof RulesRULE 4 ′′ : FAILURE IIp → B, {p} S {q}{p} if B → S fi {q}RULE 5: LOOP{p ∧ B} S {p}{p} while B do S od {p ∧ ¬B}RULE 6: CONSEQUENCEp → p1 , {p1 } S {q1 }, q1 → q{p} S {q}RULE 7: LOOP II{p ∧ B} S {p},{p ∧ B ∧ t = z} S {t < z},p →t≥0{p} while B do S od {p ∧ ¬ B}where t is an integer expression and z is an integer variable that does notappear in p, B, t or S.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 .RULE 9: RECURSION II{p1 } P1 {q1 }, . . . , {pn } Pn {qn } ⊢ {p} S {q},{p1 ∧ t < z} P1 {q1 }, . . . , {pn ∧ t < z} Pn {qn } ⊢{pi ∧ t = z} Si {qi }, i ∈ {1, . . ., n},pi → t ≥ 0, i ∈ {1, . . ., n}{p} S {q}where D = P1 :: S1 , .
. . , Pn :: Sn and z is an integer variable that does notoccur in pi , t, qi and Si for i ∈ {1, . . . , n} and is treated in the proofs as aconstant.B Axioms and Proof Rules461RULE 10: BLOCK{p} x̄ := t̄; S {q}{p} begin local x̄ := t̄; S end {q}where {x̄} ∩ f ree(q) = ∅.RULE 11: INSTANTIATION{p} P (x̄) {q}{p[x̄ := t̄]} P (t̄) {q[x̄ := t̄]}where var(x̄) ∩ var(D) = var(t̄) ∩ change(D) = ∅.RULE 12: RECURSION III{p1 } P1 (t̄1 ) {q1 }, . . . , {pn } Pn (t̄n ) {qn } ⊢ {p} S {q},{p1 } P1 (t̄1 ) {q1 }, .
. . , {pn } Pn (t̄n ) {qn } ⊢{pi } begin local ūi := t̄i ; Si end {qi }, i ∈ {1, . . ., n}{p} S {q}where Pi (ūi ) :: Si ∈ D for i ∈ {1, . . . , n}.RULE 12 ′ : MODULARITY{p0 } P (x̄) {q0 } ⊢ {p0 } begin local ū := x̄; S end {q0 },{p0 } P (x̄) {q0 }, {p} P (x̄) {q} ⊢ {p} begin local ū := x̄; S end {q}{p} P (x̄) {q}where var(x̄) ∩ var(D) = ∅ and D = P (ū) :: S.RULE 13: RECURSION IV{p1 } P1 (ē1 ) {q1 }, . . . , {pn } Pn (ēn ) {qn } ⊢tot {p} S {q},{p1 ∧ t < z} P1 (ē1 ) {q1 }, . . .
, {pn ∧ t < z} Pn (ēn ) {qn } ⊢tot{pi ∧ t = z} begin local ūi := ēi ; Si end {qi }, i ∈ {1, . . ., n}{p} S {q}where Pi (ūi ) :: Si ∈ D, for i ∈ {1, . . ., n}, and z is an integer variable thatdoes not occur in pi , t, qi and Si for i ∈ {1, . . ., n} and is treated in the proofsas a constant.AXIOM 14: ASSIGNMENT TO INSTANCE VARIABLES{p[u := t]} u := t {p}where u ∈ IV ar or u ≡ a[s1 , .
. . , sn ] and a ∈ IV ar.462B Axioms and Proof RulesRULE 15: INSTANTIATION II{p} y.m {q}{p[y := s]} s.m {q[y := s]}where y 6∈ var(D) and var(s) ∩ change(D) = ∅.RULE 16: RECURSION V{p1 } s1 .m1 {q1 }, . . . , {pn } sn .mn {qn } ⊢ {p} S {q},{p1 } s1 .m1 {q1 }, . . . , {pn } sn .mn {qn } ⊢{pi } begin local this := si ; Si end {qi }, i ∈ {1, .
. ., n}{p} S {q}where mi :: Si ∈ D for i ∈ {1, . . . , n}.RULE 17: RECURSION VI{p1 } s1 .m1 {q1 }, . . . , {pn } sn .mn {qn } ⊢ {p} S {q},{p1 ∧ t < z} s1 .m1 {q1 }, . . . , {pn ∧ t < z} sn .mn {qn } ⊢{pi ∧ t = z} begin local this := si ; Si end {qi }, i ∈ {1, . . ., n}{p} S {q}where mi :: Si ∈ D, for i ∈ {1, . . . , n}, and z is an integer variable that doesnot occur in pi , t, qi and Si for i ∈ {1, . . ., n} and is treated in the proofs asa constant.RULE 18: INSTANTIATION III{p} y.m(x̄) {q}{p[y, x̄ := s, t̄]} s.m(t̄) {q[y, x̄ := s, t̄]}where y, x̄ is a sequence of simple variables in V ar which do not appear inD and var(s, t̄) ∩ change(D) = ∅.RULE 19: RECURSION VII{p1 } s1 .m1 (t̄1 ) {q1 }, .
. . , {pn } sn .mn (t̄n ) {qn } ⊢ {p} S {q},{p1 } s1 .m1 (t̄1 ) {q1 }, . . . , {pn } sn .mn (t̄n ) {qn } ⊢{pi } begin local this, ūi := si , t̄i ; Si end {qi }, i ∈ {1, . . ., n}{p} S {q}where mi (ūi ) :: Si ∈ D for i ∈ {1, . . . , n}.B Axioms and Proof Rules463RULE 20: RECURSION VIII{p1 } s1 .m1 (ē1 ) {q1 }, .
. . , {pn } sn .mn (ēn ) {qn } ⊢ {p} S {q},{p1 ∧ t < z} s1 .m1 (ē1 ) {q1 }, . . . , {pn ∧ t < z} sn .mn (ēn ) {qn } ⊢{pi ∧ t = z} begin local this, ūi := si , ēi ; Si end {qi }, i ∈ {1, . . ., n}pi → si 6= null, i ∈ {1, . . ., n}{p} S {q}where mi (ūi ) :: Si ∈ D, for i ∈ {1, .
. . , n}, and and z is an integer variablethat does not occur in pi , t, qi and Si for i ∈ {1, . . . , n} and is treated in theproofs as a constant.AXIOM 21: OBJECT CREATION{p[x := new]} x := new {p},where x ∈ V ar is a simple object variable and p is a pure assertion.RULE 22: OBJECT CREATIONp′ → p[u := x]{p [x := new]} u := new {p}′where u is a subscripted normal object variable or a (possibly subscripted)instance object variable, x ∈ V ar is a fresh simple object variable which doesnot occur in p, and p′ is a pure assertion.RULE 23: SEQUENTIALIZATION{p} S1 ; .
. .; Sn {q}{p} [S1 k. . .kSn ] {q}RULE 24: DISJOINT PARALLELISM{pi } Si {qi }, i ∈ {1, . . . , n}VnVn{ i=1 pi } [S1 k. . .kSn ] { i=1 qi }where f ree(pi , qi ) ∩ change(Sj ) = ∅ for i 6= j.RULE 25: AUXILIARY VARIABLES{p} S {q}{p} S0 {q}where for some set of auxiliary variables A of S with f ree(q) ∩ A = ∅, theprogram S0 results from S by deleting all assignments to the variables in A.464B Axioms and Proof RulesRULE 26: ATOMIC REGION{p} S {q}{p} hSi {q}RULE 27: PARALLELISM WITH SHARED VARIABLESThe standard proof outlines {pi } Si∗ {qi },i ∈ {1, . .
. , n}, are interference freeVnVn{ i=1 pi } [S1 k. . .kSn ] { i=1 qi }RULE 28: SYNCHRONIZATION{p ∧ B} S {q}{p} await B then S end {q}RULE 29: PARALLELISM WITH DEADLOCK FREEDOM(1) The standard proof outlines {pi } Si∗ {qi }, i ∈ {1, . . . , n}for weak total correctness are interference free,(2) For every potential deadlock (R1 , . . ., Rn ) of[S1 k. . .kSn ] the corresponding tupleVn ofassertions (r1 , .
. ., rn ) satisfies ¬ i=1 ri .VnVn{ i=1 pi } [S1 k. . .kSn ] { i=1 qi }RULE 30: ALTERNATIVE COMMAND{p ∧ Bi } Si {q}, i ∈ {1, . . . , n}{p} if ⊓⊔ni=1 Bi → Si fi {q}RULE 31: REPETITIVE COMMAND{p ∧ Bi } Si {p}, i ∈ {1, . . . , n}Vn{p} do ⊓⊔ni=1 Bi → Si od {p ∧ i=1 ¬Bi }RULE 32: ALTERNATIVE COMMAND IIWnp → i=1 Bi ,{p ∧ Bi } Si {q}, i ∈ {1, .
. . , n}{p} if ⊓⊔ni=1 Bi → Si fi {q}B Axioms and Proof Rules465RULE 33: REPETITIVE COMMAND II{p ∧ Bi } Si {p}, i ∈ {1, . . . , n},{p ∧ Bi ∧ t = z} Si {t < z}, i ∈ {1, . . . , n},p→t≥0Vn{p} do ⊓⊔ni=1 Bi → Si od {p ∧ i=1 ¬Bi }where t is an integer expression and z is an integer variable not occurring inp, t, Bi or Si for i ∈ {1, . . . , n}.RULE 34: DISTRIBUTED PROGRAMS{p} S1,0 ; . . .; Sn,0 {I},{I ∧ Bi,j ∧ Bk,ℓ } Eff (αi,j , αk,ℓ ); Si,j ; Sk,ℓ {I}for all (i, j, k, ℓ) ∈ Γ{p} S {I ∧ TERM }RULE 35: DISTRIBUTED PROGRAMS II(1) {p} S1,0 ; . . .; Sn,0 {I},(2) {I ∧ Bi,j ∧ Bk,ℓ } Eff (αi,j , αk,ℓ ); Si,j ; Sk,ℓ {I}for all (i, j, k, ℓ) ∈ Γ,(3) {I ∧ Bi,j ∧ Bk,ℓ ∧ t = z} Eff (αi,j , αk,ℓ ); Si,j ; Sk,ℓ {t < z}for all (i, j, k, ℓ) ∈ Γ,(4) I → t ≥ 0{p} S {I ∧ TERM }where t is an integer expression and z is an integer variable not appearing inp, t, I or S.RULE 36: DISTRIBUTED PROGRAMS III(1) {p} S1,0 ; .
. .; Sn,0 {I},(2) {I ∧ Bi,j ∧ Bk,ℓ } Eff (αi,j , αk,ℓ ); Si,j ; Sk,ℓ {I}for all (i, j, k, ℓ) ∈ Γ,(3) {I ∧ Bi,j ∧ Bk,ℓ ∧ t = z} Eff (αi,j , αk,ℓ ); Si,j ; Sk,ℓ {t < z}for all (i, j, k, ℓ) ∈ Γ,(4) I → t ≥ 0,(5) I ∧ BLOCK → TERM{p} S {I ∧ TERM }where t is an integer expression and z is an integer variable not appearing inp, t, I or S.466B Axioms and Proof RulesAXIOM 37: RANDOM ASSIGNMENT{∀x ≥ 0 : p} x :=? {p}RULE 38: REPETITIVE COMMAND IIIwhere{p ∧ Bi } Si {p}, i ∈ {1, . .
. , n},{p ∧ Bi ∧ t = α} Si {t < α}, i ∈ {1, . . . , n},p→t∈WVn{p} do ⊓⊔ni=1 Bi → Si od {p ∧ i=1 ¬Bi }(i) t is an expression which takes values in an irreflexive partial order (P, <)that is well-founded on the subset W ⊆ P ,(ii) α is a simple variable ranging over P that does not occur in p, t, Bi orSi for i ∈ {1, .
. . , n}.RULE 39: FAIR REPETITIONwhere(1) {p ∧ Bi } Si {p}, i ∈ {1, . . . , n},(2) {p ∧ Bi ∧ z̄ ≥ 0∧ ∃zi ≥ 0 : t[zj := if Bj then zj + 1 else zj fi]j6=i = α}Si{t < α}, i ∈ {1, . . . , n},(3) p ∧ z̄ ≥ 0 → t ∈ WVn(4) {p} do ⊓⊔ni=1 Bi → Si od {p ∧ i=1 ¬Bi }(i) t is an expression which takes values in an irreflexive partial order (P, <)that is well-founded on the subset W ⊆ P ,(ii) z1 , . . ., zn are integer variables that do not occur in p, Bi or Si , fori ∈ {1, .
. . , n},(iii) t[zj := if Bj then zj + 1 else zj fi]j6=i denotes the expression that results from t by substituting for every occurrence of zj in t the conditional expression if Bj then zj + 1 else zj fi; here j ranges over the set{1, . . ., n} −{i},(iv) z̄ ≥ 0 abbreviates z1 ≥ 0 ∧ . . . ∧ zn ≥ 0,(v) α is a simple variable ranging over P and not occurring in p, t, Bi or Si ,for i ∈ {1, . . .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
