4 Коммуникационный протокол с таймером - устройство и обоснование корректности (1185642), страница 3
Текст из файла (страница 3)
 ñèñòåìå åñòüäîïîëíèòåëüíûå ïåðåõîäû, íå ñâÿçàííûå ñ äåéñòâèÿìèïðîòîêîëîâ ïðîöåññîâ. Ñ èõ ïîìîùüþ ìîäåëèðóþòñÿ îøèáêèïîòåðè è äóáëèðîâàíèÿ ñîîáùåíèé â êàíàëàõ ñâÿçè.Êîììóíèêàöèîííàÿ ñðåäàTime:(* δ > 0 *)i do Ut[i] := Ut[i] − δ ;St := St − δ ;Rt := Rt − δ ;if Rt ≤ 0 then delete (Rt, Exp); (* cr := false *)forall h.., ρi ∈ Mp , Mq dobegin ρ := ρ − δ ;if ρ ≤ 0 then remove packetbegin forallendendÄåéñòâèå Time ïðèâîäèò ê óìåíüøåíèþ ïîêàçàòåëåé âñåõòàéìåðîâ ñèñòåìû íà îäíó è òó æå âåëè÷èíó δ , è ýòî êàê ðàçñîîòâåòñòâóåò òîìó, ÷òî ïðîèñõîäèò, êîãäà äâà äèñêðåòíûõñîáûòèÿ îêàçûâàþòñÿ ðàçäåëåííûìè èíòåðâàëîì âðåìåíèïðîòÿæåííîñòè δ .Êîììóíèêàöèîííàÿ ñðåäàTime:(* δ > 0 *)i do Ut[i] := Ut[i] − δ ;St := St − δ ;Rt := Rt − δ ;if Rt ≤ 0 then delete (Rt, Exp); (* cr := false *)forall h.., ρi ∈ Mp , Mq dobegin ρ := ρ − δ ;if ρ ≤ 0 then remove packetbegin forallendendÏðîöåññïîëó÷àòåëü çàêðûâàåò ñåàíñ ñâÿçè, êàê òîëüêîïîêàçàíèå òàéìåðà ïîëó÷àòåëÿ Rt îêàçûâàåòñÿ ðàâíûì 0 ,ñåàíñ ñâÿçè çàêðûâàåòñÿ.
Ýòî ïðîèñõîäèò, åñëè â òå÷åíèåâðåìåíè R , îòâåäåííîãî äëÿ ïðèåìà îæèäàåìîãî ñëîâà, ýòîñëîâî íå áûëî ïîëó÷åíî.Êîððåêòíîñòü ïðîòîêîëà ñ òàéìåðàìèÑâîéñòâà áåçîïàñíîñòè ïðîòîêîëà.1. Îòñóòñòâèå ïîòåðü. Êàæäîå ñëîâî èç ìàññèâà inp áóäåòâðó÷åíî ïðîöåññîì q èëè çàðåãèñòðèðîâàíî ïðîöåññîì p(êàê ¾âåðîÿòíî ïîòåðÿííîå¿) ñïóñòÿ îãðàíè÷åííûé îòðåçîêâðåìåíè ñ ìîìåíòà ïîñòóïëåíèÿ ýòîãî ñëîâà ê ïðîöåññó p .2. Ñîáëþäåíèå ïîðÿäêà.
Ñëîâà, êîòîðûå âðó÷àþòñÿïðîöåññîì q , ñëåäóþò â ïîðÿäêå ñòðîãîãî âîçðàñòàíèÿíîìåðîâ â ìàññèâå inp .Êîððåêòíîñòü ïðîòîêîëà ñ òàéìåðàìèÄëÿ äîêàçàòåëüñòâà ýòèõ ñâîéñòâ áåçîïàñíîñòè âîñïîëüçóåìñÿìåòîäîì èíâàðèàíòîâ.Óñòàíîâèì èíâàðèàíòíîñòü äâóõ óòâåðæäåíèé P0 (èíâàðèàíòïðîöåññàîòïðàâèòåëÿ) è P1 (èíâàðèàíò ïðîöåññàïîëó÷àòåëÿ).Êîððåêòíîñòü ïðîòîêîëà ñ òàéìåðàìèÒåîðåìà 4.1.Ñëåäóþùåå óòâåðæäåíèå ÿâëÿåòñÿ èíâàðèàíòîì ïðîòîêîëà ñòàéìåðàìè.P0 ≡∧∧∧∧∧∧∧cs ⇒ St ≤ Scr ⇒ 0 < Rt ≤ R∀i < B + High : Ut[i] ≤ U∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µhdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + Rcr ⇒ cs ∧ St ≥ Rt + µhack, i, ρi ∈ Mp ⇒ cs ∧ St > ρhdata, s, i, w , ρi ∈ Mq ⇒ (w = inp [B + i] ∧ i < High)Äëÿ ïðàâèëüíîãî èñòîëêîâàíèÿ ñîîòíîøåíèÿ (3), ìû áóäåìïðåäïîëàãàòü, ÷òî çíà÷åíèå High ðàâíî íóëþ âî âñåõ òåõêîíôèãóðàöèÿõ, â êîòîðûõ îòïðàâèòåëü íå èìååò ñîåäèíåíèÿ.(1)(2)(3)(4)(5)(6)(7)(8)Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0Äîêàçàòåëüñòâî. ñàìîì íà÷àëå âû÷èñëåíèÿ ñîåäèíåíèÿ îòñóòñòâóþò, íåòíèêàêèõ ïàêåòîâ, B = 0 , è ïîýòîìó óòâåðæäåíèå P0 ÿâëÿåòñÿèñòèííûì.Äàëåå ðàññìîòðèì ïîñëåäîâàòåëüíî âñå äåéñòâèÿ ïðîöåññîâ p èq , è ïîêàæåì âûïîëíèìîñòü ñîîòíîøåíèÿ{P0 } −→ {P0 }Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0Ap :cs thencreate(St, High, Low ) ; (* cs := true *)Low := High := 0 ; St := S end;Ut[B + High] := U ; High := High + 1 endbegin if notbeginP0 ≡∧∧∧∧∧∧∧cs ⇒ St ≤ Scr ⇒ 0 < Rt ≤ R∀i < B + High : Ut[i] ≤ U∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µhdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + Rcr ⇒ cs ∧ St ≥ Rt + µhack, i, ρi ∈ Mp ⇒ cs ∧ St > ρhdata, s, i, w , ρi ∈ Mq ⇒ (w = inp [B + i] ∧ i < High)Ñîîòíîøåíèå (1) ñîõðàíÿåòñÿ, ò.ê.
îïåðàòîð ïðèñâàèâàíèÿ, âïðàâîé ÷àñòè êîòîðîãî ñòîèò St , âñåãäà ïðèâîäèò ê òîìó, ÷òîâûïîëíÿåòñÿ ðàâåíñòâî St = S .(1)(2)(3)(4)(5)(6)(7)(8)Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0Ap :cs thencreate(St, High, Low ) ; (* cs := true *)Low := High := 0 ; St := S end;Ut[B + High] := U ; High := High + 1 endbegin if notbeginP0 ≡∧∧∧∧∧∧∧cs ⇒ St ≤ Scr ⇒ 0 < Rt ≤ R∀i < B + High : Ut[i] ≤ U∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µhdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + Rcr ⇒ cs ∧ St ≥ Rt + µhack, i, ρi ∈ Mp ⇒ cs ∧ St > ρhdata, s, i, w , ρi ∈ Mq ⇒ (w = inp [B + i] ∧ i < High)Ñîîòíîøåíèÿ (2) è (4) ñîõðàíÿþòñÿ, ò.ê.
ýòî äåéñòâèå íå âëèÿåòíà ïåðåìåííûå ýòèõ ñîîòíîøåíèé(1)(2)(3)(4)(5)(6)(7)(8)Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0Ap :cs thencreate(St, High, Low ) ; (* cs := true *)Low := High := 0 ; St := S end;Ut[B + High] := U ; High := High + 1 endbegin if notbeginP0 ≡∧∧∧∧∧∧∧cs ⇒ St ≤ Scr ⇒ 0 < Rt ≤ R∀i < B + High : Ut[i] ≤ U∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µhdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + Rcr ⇒ cs ∧ St ≥ Rt + µhack, i, ρi ∈ Mp ⇒ cs ∧ St > ρhdata, s, i, w , ρi ∈ Mq ⇒ (w = inp [B + i] ∧ i < High)Ñîîòíîøåíèå (3) ñîõðàíÿåòñÿ, ò.ê.
ïåðåä òåì, êàê ïåðåìåííàÿHigh óâåëè÷èò ñâîå çíà÷åíèå, ýëåìåíòó Ut[B + High]ïðèñâàèâàåòñÿ çíà÷åíèå U .(1)(2)(3)(4)(5)(6)(7)(8)Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0Ap :cs thencreate(St, High, Low ) ; (* cs := true *)Low := High := 0 ; St := S end;Ut[B + High] := U ; High := High + 1 endbegin if notbeginP0 ≡∧∧∧∧∧∧∧cs ⇒ St ≤ Scr ⇒ 0 < Rt ≤ R∀i < B + High : Ut[i] ≤ U∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µhdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + Rcr ⇒ cs ∧ St ≥ Rt + µhack, i, ρi ∈ Mp ⇒ cs ∧ St > ρhdata, s, i, w , ρi ∈ Mq ⇒ (w = inp [B + i] ∧ i < High)Ñîîòíîøåíèÿ (5), (6) è (7) ñîõðàíÿþòñÿ, ò.ê.
çíà÷åíèå St ìîæåòòîëüêî óâåëè÷èòüñÿ.(1)(2)(3)(4)(5)(6)(7)(8)Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0Ap :cs thencreate(St, High, Low ) ; (* cs := true *)Low := High := 0 ; St := S end;Ut[B + High] := U ; High := High + 1 endbegin if notbeginP0 ≡∧∧∧∧∧∧∧cs ⇒ St ≤ Scr ⇒ 0 < Rt ≤ R∀i < B + High : Ut[i] ≤ U∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µhdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + Rcr ⇒ cs ∧ St ≥ Rt + µhack, i, ρi ∈ Mp ⇒ cs ∧ St > ρhdata, s, i, w , ρi ∈ Mq ⇒ (w = inp [B + i] ∧ i < High)Ñîîòíîøåíèå (8) ñîõðàíÿåòñÿ, ïîñêîëüêó çíà÷åíèå High ìîæåòòîëüêî óâåëè÷èòüñÿ.(1)(2)(3)(4)(5)(6)(7)(8)Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0Sp :{ cs ∧ Low ≤ i < High ∧ Ut[B + i] > 0 }begin sendhdata, (i = Low ), i, inp [B + i], µi ; St := SP0 ≡∧∧∧∧∧∧∧endcs ⇒ St ≤ Scr ⇒ 0 < Rt ≤ R∀i < B + High : Ut[i] ≤ U∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µhdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + Rcr ⇒ cs ∧ St ≥ Rt + µhack, i, ρi ∈ Mp ⇒ cs ∧ St > ρhdata, s, i, w , ρi ∈ Mq ⇒ (w = inp [B + i] ∧ i < High)Ñîîòíîøåíèå (1) ñîõðàíÿåòñÿ, ò.ê.
St âñåãäà áóäåò ïðèñâîåíîçíà÷åíèå S .(1)(2)(3)(4)(5)(6)(7)(8)Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0Sp :{ cs ∧ Low ≤ i < High ∧ Ut[B + i] > 0 }begin sendhdata, (i = Low ), i, inp [B + i], µi ; St := SP0 ≡∧∧∧∧∧∧∧endcs ⇒ St ≤ Scr ⇒ 0 < Rt ≤ R∀i < B + High : Ut[i] ≤ U∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µhdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + Rcr ⇒ cs ∧ St ≥ Rt + µhack, i, ρi ∈ Mp ⇒ cs ∧ St > ρhdata, s, i, w , ρi ∈ Mq ⇒ (w = inp [B + i] ∧ i < High)Ñîîòíîøåíèÿ (2) è (3) ñîõðàíÿþòñÿ, ò.ê. ýòî äåéñòâèå íå âëèÿåòíà ïåðåìåííûå ýòèõ ñîîòíîøåíèé(1)(2)(3)(4)(5)(6)(7)(8)Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0Sp :{ cs ∧ Low ≤ i < High ∧ Ut[B + i] > 0 }begin sendhdata, (i = Low ), i, inp [B + i], µi ; St := SP0 ≡∧∧∧∧∧∧∧endcs ⇒ St ≤ Scr ⇒ 0 < Rt ≤ R∀i < B + High : Ut[i] ≤ U∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µhdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + Rcr ⇒ cs ∧ St ≥ Rt + µhack, i, ρi ∈ Mp ⇒ cs ∧ St > ρhdata, s, i, w , ρi ∈ Mq ⇒ (w = inp [B + i] ∧ i < High)Ñîîòíîøåíèå (4) ñîõðàíÿåòñÿ, ò.ê.
êàæäûé îòïðàâëÿåìûé ïàêåòèìååò âðåìÿ îñòàâøåéñÿ æèçíè ðàâíîå µ .(1)(2)(3)(4)(5)(6)(7)(8)Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0Sp :{ cs ∧ Low ≤ i < High ∧ Ut[B + i] > 0 }begin sendhdata, (i = Low ), i, inp [B + i], µi ; St := SP0 ≡∧∧∧∧∧∧∧endcs ⇒ St ≤ Scr ⇒ 0 < Rt ≤ R∀i < B + High : Ut[i] ≤ U∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µhdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + Rcr ⇒ cs ∧ St ≥ Rt + µhack, i, ρi ∈ Mp ⇒ cs ∧ St > ρhdata, s, i, w , ρi ∈ Mq ⇒ (w = inp [B + i] ∧ i < High)Ñîîòíîøåíèå (5) ñîõðàíÿåòñÿ, ò.ê. ïàêåò h.., µi îòïðàâëåí, Stïîëàãàåòñÿ ðàâíûì S , è S = R + 2µ .(1)(2)(3)(4)(5)(6)(7)(8)Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0Sp :{ cs ∧ Low ≤ i < High ∧ Ut[B + i] > 0 }begin sendhdata, (i = Low ), i, inp [B + i], µi ; St := SP0 ≡∧∧∧∧∧∧∧endcs ⇒ St ≤ Scr ⇒ 0 < Rt ≤ R∀i < B + High : Ut[i] ≤ U∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µhdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + Rcr ⇒ cs ∧ St ≥ Rt + µhack, i, ρi ∈ Mp ⇒ cs ∧ St > ρhdata, s, i, w , ρi ∈ Mq ⇒ (w = inp [B + i] ∧ i < High)Ñîîòíîøåíèÿ (6) è (7) ñîõðàíÿþòñÿ, ò.ê.
çíà÷åíèå St ìîæåòòîëüêî óâåëè÷èòüñÿ.(1)(2)(3)(4)(5)(6)(7)(8)Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0Sp :{ cs ∧ Low ≤ i < High ∧ Ut[B + i] > 0 }begin sendhdata, (i = Low ), i, inp [B + i], µi ; St := SP0 ≡∧∧∧∧∧∧∧endcs ⇒ St ≤ Scr ⇒ 0 < Rt ≤ R∀i < B + High : Ut[i] ≤ U∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µhdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + Rcr ⇒ cs ∧ St ≥ Rt + µhack, i, ρi ∈ Mp ⇒ cs ∧ St > ρhdata, s, i, w , ρi ∈ Mq ⇒ (w = inp [B + i] ∧ i < High)Ñîîòíîøåíèå (8) ñîõðàíÿåòñÿ, äëÿ íîâîãî ïàêåòà âûïîëíÿþòñÿóñëîâèÿ w = inp [B + i] è i < High .(1)(2)(3)(4)(5)(6)(7)(8)Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0Rp :(* Ïîëó÷èòü ïîäòâåðæäåíèå *){ cs ∧ hack, i, ρi ∈ Mp }begin receivehack, i, ρi ; Low := max (Low , i)P0 ≡∧∧∧∧∧∧∧endcs ⇒ St ≤ Scr ⇒ 0 < Rt ≤ R∀i < B + High : Ut[i] ≤ U∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µhdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + Rcr ⇒ cs ∧ St ≥ Rt + µhack, i, ρi ∈ Mp ⇒ cs ∧ St > ρhdata, s, i, w , ρi ∈ Mq ⇒ (w = inp [B + i] ∧ i < High)Äåéñòâèå Rp íå èçìåíÿåò çíà÷åíèé íè îäíîé èç ïåðåìåííûõ,ôèãóðèðóþùèõ â ôîðìóëå P0 , è èçúÿòèå ïàêåòà ñîõðàíÿåòñîîòíîøåíèÿ (4) è (7).(1)(2)(3)(4)(5)(6)(7)(8)Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0Ep :{ cs ∧ Ut[B + Low ] ≤ −2µ − R }begin error [B + Low ] := true ; Low := Low + 1P0 ≡∧∧∧∧∧∧∧endcs ⇒ St ≤ Scr ⇒ 0 < Rt ≤ R∀i < B + High : Ut[i] ≤ U∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µhdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + Rcr ⇒ cs ∧ St ≥ Rt + µhack, i, ρi ∈ Mp ⇒ cs ∧ St > ρhdata, s, i, w , ρi ∈ Mq ⇒ (w = inp [B + i] ∧ i < High)Äåéñòâèå Ep íå èçìåíÿåò çíà÷åíèé íè îäíîé èç ïåðåìåííûõ,ôèãóðèðóþùèõ â ôîðìóëå P0 .(1)(2)(3)(4)(5)(6)(7)(8)Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0Cp :{ cs ∧ St < 0 ∧ Low = High }begin B := B + High ; delete (St, High, Low )(* cs := false *)P0 ≡∧∧∧∧∧∧∧endcs ⇒ St ≤ Scr ⇒ 0 < Rt ≤ R∀i < B + High : Ut[i] ≤ U∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µhdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + Rcr ⇒ cs ∧ St ≥ Rt + µhack, i, ρi ∈ Mp ⇒ cs ∧ St > ρhdata, s, i, w , ρi ∈ Mq ⇒ (w = inp [B + i] ∧ i < High)Ñîîòíîøåíèå (1) ñîõðàíÿåòñÿ, ò.ê.
ïîñëå äåéñòâèÿ Cp íåâûïîëíÿåòñÿ åãî ïðåäïîñûëêà.(1)(2)(3)(4)(5)(6)(7)(8)Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0Cp :{ cs ∧ St < 0 ∧ Low = High }begin B := B + High ; delete (St, High, Low )(* cs := false *)P0 ≡∧∧∧∧∧∧∧endcs ⇒ St ≤ Scr ⇒ 0 < Rt ≤ R∀i < B + High : Ut[i] ≤ U∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µhdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + Rcr ⇒ cs ∧ St ≥ Rt + µhack, i, ρi ∈ Mp ⇒ cs ∧ St > ρhdata, s, i, w , ρi ∈ Mq ⇒ (w = inp [B + i] ∧ i < High)Ñîîòíîøåíèÿ (2),(3) è (4) ñîõðàíÿþòñÿ, ò.ê.
ýòî äåéñòâèå íåâëèÿåò íà ïåðåìåííûå ýòèõ ñîîòíîøåíèé.(1)(2)(3)(4)(5)(6)(7)(8)Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0Cp :{ cs ∧ St < 0 ∧ Low = High }begin B := B + High ; delete (St, High, Low )(* cs := false *)P0 ≡∧∧∧∧∧∧∧endcs ⇒ St ≤ Scr ⇒ 0 < Rt ≤ R∀i < B + High : Ut[i] ≤ U∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µhdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + Rcr ⇒ cs ∧ St ≥ Rt + µhack, i, ρi ∈ Mp ⇒ cs ∧ St > ρhdata, s, i, w , ρi ∈ Mq ⇒ (w = inp [B + i] ∧ i < High)Äåéñòâèå Cp ìîæåò íàðóøèòü ñïðàâåäëèâîñòü çàêëþ÷åíèé âñîîòíîøåíèÿõ (5), (6) è (7), íî ñîãëàñíî (2), (5), (6) è (7) îíîïðèìåíèìî òîëüêî òîãäà, êîãäà ïðåäïîñûëêè ýòèõ ñîîòíîøåíèéíå âûïîëíÿþòñÿ.(1)(2)(3)(4)(5)(6)(7)(8)Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0Cp :{ cs ∧ St < 0 ∧ Low = High }begin B := B + High ; delete (St, High, Low )(* cs := false *)P0 ≡∧∧∧∧∧∧∧endcs ⇒ St ≤ Scr ⇒ 0 < Rt ≤ R∀i < B + High : Ut[i] ≤ U∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µhdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + Rcr ⇒ cs ∧ St ≥ Rt + µhack, i, ρi ∈ Mp ⇒ cs ∧ St > ρhdata, s, i, w , ρi ∈ Mq ⇒ (w = inp [B + i] ∧ i < High)Äåéñòâèå Cp òàêæå èçìåíÿåò çíà÷åíèå ïåðåìåííîé B , íîïîñêîëüêó ñîãëàñíî ñîîòíîøåíèÿì (5) è (7) íè îäèí ïàêåò íåíàõîäèòñÿ íà ýòàïå ïåðåñûëêè, âûïîëíèìîñòü ñîîòíîøåíèÿ (8)ñîõðàíÿåòñÿ.(1)(2)(3)(4)(5)(6)(7)(8)Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0Rq : { hdata, s, i, w , ρi ∈ Mq }begin receive hdata, s, i, w , ρi ;if criftheni = Exp then begin Rt := R ; Exp := i + 1 ; deliver w ends = true then begin create (Rt, Exp) ; (* cr := true *)Rt := R ; Exp := i + 1 ; deliver w endelse ifend∧∧∧∧∧cs ⇒ St ≤ S∀i < B + High : Ut[i] ≤ U∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µhdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + Rhack, i, ρi ∈ Mp ⇒ cs ∧ St > ρhdata, s, i, w , ρi ∈ Mq ⇒ (w = inp [B + i] ∧ i < High)(1)(3)(4)(5)(7)(8)Ñîîòíîøåíèÿ (1),(3-5) è (7-8) ñîõðàíÿþòñÿ, ò.ê.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
