Объяснение к (3): значение High предполагается равным нулю во всех конфигурациях, в которых со стороны приемника нет соединения.
Ëåììà 3.10 P0 - инвариант протокола, основанного на таймере.
Äîêàçàòåëüñòâî. Первоначально не соединения, нет пакетов, и B = 0, из чего следует, что P0 - true.
Ap: (1) сохраняется, т.к. St всегда присваивается значения S (St = S). (3) сохраняется, т.к. перед увеличением High, Ut[B + High] присваивается значение U. (5), (6) и (7) сохраняются, т.к. St может только увеличиваться. (8) сохраняется, т.к. High может только увеличиваться.
Sp: (1) сохраняется, т.к. St всегда присваивается значения S. (4) сохраняется, т.к. каждый пакет посылается с оставшимся временем жизни равным m. (5) сохраняется, т.к. пакет <.., m> посылается и St устанавливается в S, и S = R + 2m. (6) и (7) сохраняется, т.к. St может только увеличиться в этом действии. (8) сохраняется, т.к. новый пакет удовлетворяет w = inp[B + i] и i < High.
Rp: Действие Rp не меняет никаких переменных из P0, и удаление пакета сохраняет (4) и (7).
Ep: Действие Ep не меняет никаких переменных из P0.
Cp: Действие Cp делает равным false заключения (5), (6) и (7), но ((2), (5), (6) и (7)) применимы только когда их посылки ложны. Cp также меняет значение B, но, т.к. пакетов для передачи нет, (по (5) и (7)), (8) сохраняется.
Rq: (2) сохраняется, т.к. Rt всегда присваивается значение R (если присваивается). (6) сохраняется, т.к. Rt устанавливается только в R только при принятии пакета <data, s,i,w,r>, è из (4) и (5) следует cs Ù St ³ R + m когда это происходит.
Sq: (4) сохраняется, т.к. каждый пакет посылается с оставшимся временем жизни, равным m. (7) сохраняется, т.к. пакет < ack,i,r > посылается с r = m когда cr истинно, так что из (2) и (6) St > m.
Loss: (4), (5), (7) и (8) сохраняются, т.к. удаление пакета может фальсифицировать только их посылку.
Dupl: (4), (5), (7) и (8) сохраняются, т.к. ввод пакета m применимо только если m уже был в канале, из чего следует, что заключение данного предложения было истинным и перед введением.
Time: (1), (2) и (3) сохраняются, т.к. St, Rt, и Ut[i] может только уменьшаться, и соединение приемника закрывается, когда Rt становится равным 0. (4) сохраняются, т.к. r может только уменьшиться, и пакет удаляется, когда его r-поле достигает значения 0. Заметим, что Time уменьшает все таймеры (включая r-поле пакета) на одну и ту же величину, значит сохраняет все утверждения вида Xt > Yt +C, где Xt и Yt -таймеры, и C - константа. Это показывает, что (5), (6) и (7) сохраняются. ð
Первое требование к протоколу в том, что каждое слово в конце концов доставляется или объявляется потерянным. Определим предикат 0k(i) как
0k(i) - error [i] = true \/ q доставил inp [i].
Сейчас может быть показано, что протокол не теряет никаких слов, не объявляя об этом. Определим утверждение P1 как
P1º P0
/\ Øcs Þ" i < B: 0k(i) (9)
/\ cs Þ" i < B + Low : 0k(i) (10)
/\ <data,true,I,w,r > ÎMqÞ"i<B+I: 0k(i) (11)
/\ cr Þ" i < B+ Exp : 0k(i) (12)
/\ <ack,I,r>Î Mp Þ" i<B+I: 0k(i) (13)
Ëåììà 3.11 P1 - инвариант протокола, основанном на таймере.
Äîêàçàòåëüñòâî. Сначала заметим, что как только 0k(i) стало true для некоторого i, он никогда больше не становится false. Сначала нет соединения, нет пакетов, и B = 0, откуда следует, что P1 выполняется.
Ap: Действие Ap может открыть соединение, но при этом сохраняется (10), т.к. соединение открывается с Low = 0 и "i < B : 0k(i) выполняется из (9).
Sp: Действие Sp может послать пакет < data, s, I, w, r >, но т.к. s истинно только при I = Low, то это сохраняет (11) из (10).
Rp: Значение Low может быть увеличено, если принят пакет < ack, I, r >. Тем не менее, (10) сохраняется, т.к. из (13) "i < B + I : 0k(i) выполняется, если получено это подтверждение.
Ep: Значение Low может быть увеличено, когда применяется действие Ep, но генерация сообщения об ошибке гарантирует, что (10) сохраняется.
Cp: Действие Cp обращает cs в false, но оно применимо только если St < 0 и Low == High. Из (10) следует, что "i < B+ High : 0k(i) выполняется прежде выполнения Cp, следовательно (9) сохраняется. Посылка (10) обращается в false в этом действии, и из (5), (6) и (7) следует, что посылки (11), (12) и (13) ложны; следовательно (10), (11), (12) и (13) сохраняются.
Rq: Сначала рассмотрим случай, когда q принимает < data, true,l,w,r> при не существующем соединении (cr - false). Тогда "i < B+I : 0k(i) из (11), и w доставляется в действии. Т.к.
w = inp[B+I] из (8), присваивание Exp := I + 1 сохраняет (12).
Теперь рассмотрим случай, когда Exp увеличивается в результате принятия
< data, s,Exp,w,r> при открытом соединении. Из (12), "i < B + Exp : 0k(i) выполнялось перед принятием, и слово w = Wp[B + Exp] доставляется действием, следовательно приращение Exp сохраняет (12).
Sq: Отправление <ack, Exp, m> сохраняет (13) из (12).
Loss: Выполнение Loss может только фальсифицировать посылки предложений.
Dupl: Введение пакета m возможно только если посылка соответствующего предложения (и, следовательно, заключение) была истинна еще до введения.
Time: Таймеры не упоминались явно в (9)-(13). Выведение пакета или закрытие процессом q может только фальсифицировать посылки (11), (12) или (13).ð
Теперь может быть доказана первая часть спецификации протокола, но после дополнительного предположения. Без этого предположения отправитель может быть чрезвычайно ленивым в объявлении слов возможно потерянными; в Àëãîðèòìе 3.4 указано только, что это сообщение может и не возникнуть в промежуток времени 2m + R после окончания интервала для отправления слова, но не указано, что оно вообще должно появиться. Итак, позвольте сделать дополнительное предположение, что действие Ep на самом выполниться процессом p и в течение разумного времени, а именно прежде, чем Ut[B + Low] = —2m —R—l.
Òåîðåìà 3.12 (Нет потерь) Каждое слово inp доставляется q или объявляется p как возможно потерянное в течение U+2m+R+l после принятия слова процессом p.
Äîêàçàòåëüñòâî. После принятия слова inp[I], B+High > I начинает выполняться. Если соединение закрывается в течение указанного периода после принятия слова inp[I], то B > I, и результат следует из (9). Если соединение не закрывается в этот промежуток времени и B + Low £ I, отчет обо всех словах из промежутка B + Low..I возможен ко времени 2m + R после окончания интервала отправления inp[I]. Из этого следует, что этот отчет имел место 2m + R +l после окончания интервала отправления, ò.å., U+ 2m +R+l после принятия. Из этого также следует I < B+ Low, и, значит, слово было доставлено или объявлено (из (10)). ð
Чтобы установить второе требование корректности протокола, должно быть показано, что каждое принимаемое слово имеет больший индекс (в inp), чем ранее принятое слово. Обозначим индекс самого последнего доставленного слова через pr (для удобства запишем, что изначально
pr =-1 and Ut[-1] = -¥ ). Определим утверждение P2 как:
P2º P1
/\ <data,s,i,w,r> Î MqÞ Ut[B+i] > r -m (14)
/\ i1 £ i2 < B + High Þ Ut[i1] £ Ut[i2] (15)
/\ cr Þ Rt ³ Ut[pr] + m (16)
/\ pr < B + High /\ ( Ut[pr] > -m Þ cr) (17)
/\ cr Þ B + Exp = pr + 1 (18)
Ëåììà 3.13 P2 - инвариант протокола, основанного на таймере.
Äîêàçàòåëüñòâî. Изначально Mq пусто, B + High равно нулю, Øcr выполняется, и
Ut[pr] < -m, откуда следуют (14)-(18).
Ap: (15) сохраняется, т.к. каждое новое принятое слово получает значение таймера U, что из (3) по крайней мере равно значениям таймеров ранее принятых слов.
Sp: (14) сохраняется, т.к. Ut[B +i] > 0 и пакет отправляется с r=m .
Cp: (14), (16) и (18) сохраняются, т.к. из (5) è (6) их посылки ложны, когда Cp применимо. (15) сохраняется, т.к. B принимает значение B + High è таймеры не меняются. (17) сохраняется, т.к. B присваивается значение B + High è pr è cr не меняются.
Rq: (16) сохраняется, т.к. когда Rt устанавливается в R (при принятии слова) Ut[pr] £ U из (3), è R³ 2m+U. (17) сохраняется, т.к. pr < B+High, что следует из (8), è cr становится true. (18) сохраняется, т.к. Exp устанавливается в i +1 è pr в B + i, откуда следует, что (18) становится true.
Time: (14) сохраняется, т.к. Ut[B + i] è r уменьшаются на одно и то же число (è выведение пакета только делает ложной посылку). (15) сохраняется, т.к. Ut[i1] è Ut[i2] уменьшаются на одну и туже величину. (16) сохраняется, т.к. cr не становится истинным в этом действии, è Rt è Ut[pr] уменьшаются на одну и ту же величину. (17) сохраняется, т.к. его заключение становится ложным только, если Rt становится £ 0, откуда следует (по (16)), что Ut[pr] становится < -m. (18) сохраняется, т.к., если cr не обратился в false, B, Exp è pr не меняются.