Введение в распределённые алгоритмы. Ж. Тель (2009) (1185665), страница 19

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 19)

Основной прием, при помощи которого удается показать, что утверждениеР всегда истинно, заключается в доказательстве того, что Р является и н в а р и ­а н т о м согласно определению, которое приводится ниже. Запись Р { у), где у —конфигурация, будет обозначать булево выражение, принимающее истинное зна­чение в том случае, если утверждение Р справедливо для конфигурации у, и лож­ное значение в противном случае.Пусть задана некоторая система переходов S = (С, — 1). В дальнейшем мыбудем использовать запись {Р} —*• {Q} для обозначения того, что для каждогоперехода у —» 8 в системе 5 истинность утверждения Р(у) влечет истинностьутверждения (?(8).

Таким образом, запись {Я} —*• {Q} означает, что если утвер­ждение Р выполнялось в начале перехода, то утверждение Q будет выполнятьсяпо завершении перехода.Определение 2.9. Утверждение Р называется и н в а р и а н т о м системы S,если1) Р ( у) истинно для каждой начальной конфигурации у e l , и2) { Р } - { Р } .В этом определении говорится о том, что инвариант выполняется в каждойначальной конфигурации и его выполнимость сохраняется после каждого пере­хода. Отсюда следует, что инвариант будет выполняться в каждой достижимойконфигурации; об этом свидетельствует следующая теорема.Теорема 2.10. Е с л и у т в е р ж д е н и е Р я в л я е т с я и н в а р и а н т о м с и с т е м ып ер ехо д о в S , т о д ля лю б о го вы п о л н е н и я сист ем ы S ут вер ж д ен и е Р б уд етс п р а в е д л и в о в к а ж д о й к о н ф и г у р а ц и и в ы п о л н е н и я .22W слова «assertion» (утверждение). — Прим, перев.2.2.

Как обосновывать свойства систем переходов63Д о к а з а т е л ь с т в о . Рассмотрим произвольное выполнение Е = (уо, у i , У2 , •системы S. Воспользовавшись индукцией, покажем, что Я(у;) принимает истин­ное значение для каждого i. Во-первых, истинность утверждения Я(уо) следуетиз первого пункта определения 2.9 и того факта, что уоВо-вторых, предпо­ложив, что Я(у;) истинно и по ходу выполнения совершен переход у; —>у;+ь мызаключаем, исходя из второго пункта определения 2.9, что истинным будет такжеи P(y;+i). Этим и завершается доказательство.□Однако неверно, что утверждение, которое является истинным в каждой кон­фигурации любого выполнения, обязательно является инвариантом (см.

упраж­нение 2.2). Это означает, что отнюдь не всякое свойство безопасности можнодоказать, применяя теорему 2.10. Тем не менее, каждое утверждение, котороевсегда истинно, является следствием некоторого инварианта 3); поэтому для обос­нования того, что некоторое утверждение всегда истинно, можно воспользоватьсяследующей теоремой. Нужно, однако, заметить, что часто бывает весьма непро­сто подобрать подходящий инвариант Q , чтобы применить эту теорему.Теорема 2.11. Е с л и Q я в л я е т с я и н в а р и а н т о м с и с т е м ы п е р е х о д о в S и д л як а ж д о й к о н ф и г у р а ц и и у е С в ы п о л н я е т с я о т н о ш е н и е Q ==> Р , т о д л ялю б о го в ы п о л н е н и я сист ем ы S у т вер ж д ен и е Р б уд ет и с т и н н о в каж дойконф игурации вы полнения.Д о к а з а т е л ь с т в о .

По теореме 2.10, утверждение Q выполняется в каж­дой конфигурации4^. Так как Q ==>• Р , утверждение Р будет также выполнятьсяв каждой конфигурации.□Иногда бывает полезно вначале установить какой-нибудь слабый инвариант,а затем, воспользовавшись им, установить и более сильный инвариант.

О том,как можно усиливать инварианты, говорится в определении и теореме, которыеприводятся ниже.Определение 2.12. Пусть S — это система переходов, а Р , Q — некоторыеутверждения. Утверждение Р назовем Q - п р о и з в о д н ы м , если1) для любой начальной конфигурации увыполняется отношение д(у) =£•и2) { д л я } - {Q =► Р } .Р{Теорема 2.13. Е с л и у т в е р ж д е н и е Q я в л я е т с я и н в а р и а н т о м , а у т в е р ­ж дение Р я вл я е т с я Q -п р о и зво д н ы м , т о у т ве р ж д е н и е Q А Р я вл я е т с я и н ­вариант ом .Д о к а з а т е л ь с т в о . Согласно определению 2.9 необходимо показать, что1) для каждой начальной конфигурации у e l выполняется отношение д(у)ЛЯ(у)и2) { д л я } -> { д л я } .Можно заметить, однако, что в теореме 2.11 доказывается другое, гораздо более слабое утвер­ждение. — Прим, перев.^Достижимой конфигурации.

— Прим, перев.Гл. 2. Модель64Так как Q является инвариантом, утверждение (?(у) истинно для каждой на­чальной конфигурации у e l . Так же для каждой начальной конфигурации у € Iвыполняется отношение Q(y) =>• Р(у). Отсюда мы заключаем, что Р(у) истин­но для всех начальных конфигураций у € 1. Следовательно, (?(у) А Р(у) истиннодля всех конфигураций у из X.Предположим, что у —» 8 и Q(y) А Р(у) имеет истинное значение. Так какQ является инвариантом, Q(8) будет также иметь истинное значение.

Посколькуимеет место отношение {(? А Р} —» [QР}, выражение ф(8) =$• Р(8)будет иметь истинное значение. Отсюда следует, что и Р(8) принимает истинноезначение. Значит, Q(8) А Р(8) также истинно.□В §3.3.1 мы рассмотрим примеры свойств безопасности, для доказательствакоторых будем использовать описанные здесь методы.2.2.2. Свойства живостиСвойством живости алгоритма является всякое свойство, которое можно сфор­мулировать в виде следующего предложения: «Для любого выполнения алгоритмаутверждение Р истинно в некоторой конфигурации выполнения». Более краткоэто свойство можно сформулировать так: «Утверждение Р когда-то обязатель­но становится истинным». Основной прием, при помощи которого удается пока­зать, что утверждение Р когда-то обязательно становится истинным, заключаетсяв использовании функций нормировки и отсутствия блокировки, или пра­вильного завершения.

Более простой метод можно использовать в том случае,когда все выполнения алгоритмов имеют фиксированную конечную длину.Рассмотрим систему переходов S и предикат Р. Будем считать, что предикатterm по определению принимает истинное значение в каждой заключительнойконфигурации и ложное значение в конфигурациях, которые не являются заклю­чительными. Вначале рассмотрим те случаи, когда выполнение достигает заклю­чительной конфигурации. Обычно бывает нежелательно достичь такой конфигу­рации, прежде чем выполнится «целевой» предикат Р; в этом случае говорят, чтопроизошла блокировка. С другой стороны, если цель достигнута, то выполне­ние разрешается завершить; в этом случае говорят, что произошло правильноезавершение.Определение 2.14.

Система S правильно завершает выполнения (или,иными словами, свободна от блокировки ), если предикат (term =>• Р) всегдаявляется истинным для системы S.В основу функций нормировки положено математическое понятие фундиро­ванного множества. Это такое множество с отношением порядка <, в которомотсутствуют бесконечно убывающие последовательности элементов.Определение 2.15. Частично упорядоченное множество ( W , <) называетсяфундированным , если из его элементов нельзя составить бесконечно убываю­щую последовательностьW\>W2 >ЙУз > . . . .2.2.

Как обосновывать свойства систем переходов65Примерами фундированных множеств, которые будут использоваться в этойкниге, могут служить множество натуральных чисел с обычным отношением по­рядка, а также множество всех наборов длины п, состоящих из натуральныхчисел, с отношением лексикографического порядка (см. §4.6.3). Отсутствие бес­конечно убывающих последовательностей, состоящих из элементов фундирован­ного множества, можно использовать для доказательства того, что некотороеутверждение Р наверняка станет истинным. Для этого нужно показать, что су­ществует функция /, отображающая С в фундированное множество W так, чтокаждый переход приводит к тому, что либо значение / уменьшается, либо Р ста­новится истинным.Определение 2.16.

Пусть заданы система переходов S и утверждение Р.Функция /, отображающая множество С в фундированное множество W, назы­вается функцией нормировки (по отношению к Р), если для каждого переходау —> 8 либо выполняется отношение /(у) > /(8), либо Р(Ь) принимает истинноезначение.Теорема 2.17. Пусть заданы система переходов S и утверждение Р.Если S правильно завершает выполнения и существует функция норми­ровки / (по отношению к Р), то для каждого выполнения S утверждениеР становится истинным в некоторой конфигурации.Д о к а з а т е л ь с т в о .

Рассмотрим произвольное выполнение Е = (уо, у i , У2 , • • •)системы S. Если Е — конечная последовательность, то последняя конфигурацияявляется заключительной, и, коль скоро в системе S всегда верно соотноше­ние term ==>• Р, утверждение Р выполняется в этой конфигурации. Если вы­полнение Е продолжается бесконечно долго, то выделим в нем самый длинныйначальный отрезок Е', не содержащий ни одной конфигурации, в которой выпол­нялось бы утверждение Р. Рассмотрим последовательность s = (/(уо), /(yi), ...)для всех конфигураций у;, содержащихся в Е'. Согласно выбору Е' и в соот­ветствии с определением функции нормировки / последовательность s являетсяубывающей.

Коль скоро W — фундированное множество, последовательность sявляется конечной. Это означает также, что Е' является конечным префиксом(То, Уь • • •, Jk) выполнения Е. Тогда, помятуя о выборе Е \ приходим к заклю­чению о том, что P(jk+\) имеет истинное значение.□Если в расчет принять свойства справедливости, то доказать, что Р навер­няка станет истинным, можно исходя из более слабых предпосылок, нежели те,которые фигурируют в теореме 2.17; значения функции нормировки не обяза­тельно должны убывать после каждого перехода. Допущение справедливостиможно использовать для того, чтобы показать, что в бесконечных выполненияхпереходы определенного вида совершаются бесконечно часто.

Характеристики

Список файлов книги