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

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

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

гл. 13), чтобыпроцессы были неотличимы (см. гл. 9), и т. п.Методы верификации,описанные в этом параграфе, основываются на истинности утверждений о конфигурациях, достижимых по ходу выполнения. Такогорода методы называются ассертивными 2) методами верификации.

Под утверждением понимается одноместное отношение на множестве конфигураций, т. е.предикат, который является истинным на множестве одних конфигураций и ложным на множестве других.2.2.1. Свойства безопасностиСвойством безопасности алгоритма является всякое свойство, которое можно сформулировать в виде следующего предложения: «Для любого выполненияалгоритма утверждение P истинно в каждой конфигурации выполнения».

Болеекратко это свойство можно сформулировать так: «Утверждение P всегда истинно». Основной прием, при помощи которого удается показать, что утверждениеP всегда истинно, заключается в доказательстве того, что P является инвариантом согласно определению, которое приводится ниже. Запись P( ), где —конфигурация, будет обозначать булево выражение, принимающее истинное значение в том случае, если утверждение P справедливо для конфигурации , и ложное значение в противном случае.Пусть задана некоторая система переходов S = (C , →, I).

В дальнейшем мыбудем использовать запись {P} → {Q} для обозначения того, что для каждогоперехода → в системе S истинность утверждения P( ) влечет истинностьутверждения Q( ). Таким образом, запись {P} → {Q} означает, что если утверждение P выполнялось в начале перехода, то утверждение Q будет выполнятьсяпо завершении перехода.Определение 2.9.

Утверждение P называется инвариантом системы S,если1) P( ) истинно для каждой начальной конфигурации ∈ I , и2) {P} → {P}.В этом определении говорится о том, что инвариант выполняется в каждойначальной конфигурации и его выполнимость сохраняется после каждого перехода. Отсюда следует, что инвариант будет выполняться в каждой достижимойконфигурации; об этом свидетельствует следующая теорема.Теорема 2.10. Если утверждение P является инвариантом системыпереходов S, то для любого выполнения системы S утверждение P будетсправедливо в каждой конфигурации выполнения.2) отслова «assertion» (утверждение).

— Прим. перев.2.2. Как обосновывать свойства систем переходов63Д о к а з а т е л ь с т в о. Рассмотрим произвольное выполнение E = ( 0 , 1 , 2 , . . .)системы S. Воспользовавшись индукцией, покажем, что P( i) принимает истинное значение для каждого i. Во-первых, истинность утверждения P( 0) следуетиз первого пункта определения 2.9 и того факта, что 0 ∈ I .

Во-вторых, предположив, что P( i) истинно и по ходу выполнения совершен переход i → i+1 , мызаключаем, исходя из второго пункта определения 2.9, что истинным будет такжеи P( i+1). Этим и завершается доказательство.Однако неверно, что утверждение, которое является истинным в каждой конфигурации любого выполнения, обязательно является инвариантом (см.

упражнение 2.2). Это означает, что отнюдь не всякое свойство безопасности можнодоказать, применяя теорему 2.10. Тем не менее, каждое утверждение, котороевсегда истинно, является следствием некоторого инварианта 3) ; поэтому для обоснования того, что некоторое утверждение всегда истинно, можно воспользоватьсяследующей теоремой.

Нужно, однако, заметить, что часто бывает весьма непросто подобрать подходящий инвариант Q, чтобы применить эту теорему.Теорема 2.11. Если Q является инвариантом системы переходов S и длякаждой конфигурации ∈ C выполняется отношение Q =⇒ P, то длялюбого выполнения системы S утверждение P будет истинно в каждойконфигурации выполнения.Д о к а з а т е л ь с т в о. По теореме 2.10, утверждение Q выполняется в каждой конфигурации 4) . Так как Q =⇒ P, утверждение P будет также выполнятьсяв каждой конфигурации.Иногда бывает полезно вначале установить какой-нибудь слабый инвариант,а затем, воспользовавшись им, установить и более сильный инвариант.

О том,как можно усиливать инварианты, говорится в определении и теореме, которыеприводятся ниже.Определение 2.12. Пусть S — это система переходов, а P, Q — некоторыеутверждения. Утверждение P назовем Q-производным, если1) для любой начальной конфигурации ∈I выполняется отношение Q( ) =⇒ P( )и2) {Q ∧ P} → {Q =⇒ P}.Теорема 2.13. Если утверждение Q является инвариантом, а утверждение P является Q-производным, то утверждение Q ∧ P является инвариантом.Д о к а з а т е л ь с т в о.

Согласно определению 2.9 необходимо показать, что1) для каждой начальной конфигурации ∈I выполняется отношение Q( ) ∧P( )и2) {Q ∧ P} → {Q ∧ P}.3) Можно заметить, однако, что в теореме 2.11 доказывается другое, гораздо более слабое утверждение. — Прим. перев.4) Достижимой конфигурации.— Прим. перев.Гл. 2. Модель2.2. Как обосновывать свойства систем переходовСвойством живости алгоритма является всякое свойство, которое можно сформулировать в виде следующего предложения: «Для любого выполнения алгоритмаутверждение P истинно в некоторой конфигурации выполнения». Более краткоэто свойство можно сформулировать так: «Утверждение P когда-то обязательно становится истинным».

Основной прием, при помощи которого удается показать, что утверждение P когда-то обязательно становится истинным, заключаетсяв использовании функций нормировки и отсутствия блокировки, или правильного завершения. Более простой метод можно использовать в том случае,когда все выполнения алгоритмов имеют фиксированную конечную длину.Рассмотрим систему переходов S и предикат P.

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

Система S правильно завершает выполнения (или,иными словами, свободна от блокировки), если предикат (term =⇒ P) всегдаявляется истинным для системы S.В основу функций нормировки положено математическое понятие фундированного множества. Это такое множество с отношением порядка <, в которомотсутствуют бесконечно убывающие последовательности элементов.Определение 2.15. Частично упорядоченное множество (W, <) называетсяфундированным, если из его элементов нельзя составить бесконечно убывающую последовательностьw1 > w 2 > w 3 > .

. . .Определение 2.16. Пусть заданы система переходов S и утверждение P.Функция f, отображающая множество C в фундированное множество W, называется функцией нормировки (по отношению к P), если для каждого перехода→ либо выполняется отношение f( ) > f( ), либо P( ) принимает истинноезначение.2.2.2. Свойства живости65Примерами фундированных множеств, которые будут использоваться в этойкниге, могут служить множество натуральных чисел с обычным отношением порядка, а также множество всех наборов длины n, состоящих из натуральныхчисел, с отношением лексикографического порядка (см.

§ 4.6.3). Отсутствие бесконечно убывающих последовательностей, состоящих из элементов фундированного множества, можно использовать для доказательства того, что некотороеутверждение P наверняка станет истинным. Для этого нужно показать, что существует функция f, отображающая C в фундированное множество W так, чтокаждый переход приводит к тому, что либо значение f уменьшается, либо P становится истинным.Так как Q является инвариантом, утверждение Q( ) истинно для каждой начальной конфигурации ∈ I .

Так же для каждой начальной конфигурации ∈ Iвыполняется отношение Q( ) =⇒ P( ). Отсюда мы заключаем, что P( ) истинно для всех начальных конфигураций ∈ I . Следовательно, Q( ) ∧ P( ) истиннодля всех конфигураций из I .Предположим, что → и Q( ) ∧ P( ) имеет истинное значение. Так какQ является инвариантом, Q( ) будет также иметь истинное значение. Посколькуимеет место отношение {Q ∧ P} → {Q =⇒ P}, выражение Q( ) =⇒ P( )будет иметь истинное значение. Отсюда следует, что и P( ) принимает истинноезначение. Значит, Q( ) ∧ P( ) также истинно.В § 3.3.1 мы рассмотрим примеры свойств безопасности, для доказательствакоторых будем использовать описанные здесь методы.64Теорема 2.17. Пусть заданы система переходов S и утверждение P.Если S правильно завершает выполнения и существует функция нормировки f (по отношению к P), то для каждого выполнения S утверждениеP становится истинным в некоторой конфигурации.Д о к а з а т е л ь с т в о.

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

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