Учебное пособие по методам Флойда (1185162), страница 4
Текст из файла (страница 4)
Заглавнымибуквами обозначены блок-схемы, строчными — предикаты.a) ∀ a ∀ P ∃ b {a}P{b} ⇒ {b}P{a}b) ∀ a ∀ P ∃ b 〈a〉P〈b〉 ⇒ {b}P{a}c) ∀ P ∃ a ∃ b {a}P{b}d) ∀ P ∃ a ∃ b 〈a〉P〈b〉e) ∀ P ∃ a ∃ b {a}P{b} ∧ ¬ 〈a〉P〈b〉1.4 ФормулировкаметодовФлойдадлядоказательства корректности программМы рассмотрели доказательство полной корректности программы на примере программы целочисленного деления. Теперь мыопределим методы доказательства корректности программ, представленных в виде блок-схем, в общем случае.Как и в примере, доказательство полной корректности будетпроводиться в два этапа.
Сначала доказывается частичная корректность программы. Для этого мы будем использовать метод индуктивных утверждений Флойда. Вторым шагом проводится доказа-27тельство завершаемости программы. Для решения этой задачи мыбудем использовать метод фундированных множеств Флойда.Метод индуктивных утверждений ФлойдаБудем рассматривать пути в блок-схемах и обозначать ихследующим образом: – путь в блок-схеме, начинающийся сосвязки e1 и завершающийся связкой ek (связка e1 выходит из некоторого оператора n1, связка ek входит в некоторый оператор nk+1): n1–e1 n2 –e2 … –ek nk+1. Внутри этого пути находятся операторыn2, n3,..., nk.Дадим несколько вспомогательных определений. Определимпредикат допустимости пути (или просто, предикат пути )R(x,y) : Dx Dy {Т, F} и функцию пути r(x,y) : Dx Dy Dy.
Предикат пути R(x,y) определяет, какое должно быть значениевходных и промежуточных переменных в начале пути (в моментвыполнения перехода по связке e1), чтобы дальнейшее вычислениешло по пути . Функция пути r(x,y) определяет, как изменятсязначения промежуточных переменных в результате исполнения последователь-ности операторов блок-схемы, находящихся внутрипути .Наиболее простым способом составления формул для предикатапути R(x,y) и функции пути r(x,y) является метод обратныхподстановок.Для каждого m { 1, …, k } определим предикат Rm(x,y) ифункцию rm(x,y). При m = k это будут предикат и функция пути,состоящего из одной связки (внутри этого пути не будет ни одногооператора).
А при положительных целых m < k это будут предикат28и функция пути от связки em в связку ek (т. е. пути nm –em nm+1 –em+1 … nk –ek nk+1, проходящего через операторы nm+1, …, nk).Таким образом,R(x,y) R1(x,y)r(x,y) r1(x,y)Предикаты Rm(x,y) и функции rm(x,y) определим индукциейпо m.Базис индукции (для путей, состоящих из одной связи):Rk(x, y) Trk(x, y) yИндуктивное предположение:Зафиксируем некоторое m < k.
Предположим, что Rm+1(x,y) иrm+1(x,y)уже определены, т. е. определены предикат и функцияпути nm+1 –em+1 … nk –ek nk+1, проходящего через операторы nm+2,…, nk.Индуктивный переход:Тогда в пути из связки em в связку ek связка em будет входитьв оператор nm+1, за которым идет путь, рассмотренный в индуктивном предположении. Поэтому можно определить R m(x,y) и rm(x,y)в зависимости от оператора nm+1: Если nm+1 – оператор присваивания ASSIGN: y g(x,y), тоRm(x, y) Rm+1(x, g(x, y)) ∧ g(x, y) ≠ ωrm(x, y) rm+1(x, g(x, y)) Если nm+1 – условный оператор TEST: t(x, y) и связкаem помечена символом T, тоRm(x, y) Rm+1(x, y) ∧ t(x, y)29rm(x, y) rm+1(x, y) Если nm+1 – условный оператор TEST: t(x, y) и связкаem помечена символом F, тоRm(x, y) Rm+1(x, y) ∧ t(x, y)rm(x, y) rm+1(x, y) Если nm+1 – оператор соединения JOIN, тоRm(x, y) Rm+1(x, y)rm(x, y) rm+1(x, y)Обратите внимание, что в этом перечислении нет начальногои завершающего оператора — причина в том, что эти операторы немогут встречаться внутри пути.
Однако в них могут входить и выходить первая или последняя связка пути. Если началом первойсвязки пути является начальный оператор START: y f(x), тобудем использовать предикат R'(x) R(x, f(x)) ∧ f(x) ≠ ω ифункцию r'(x) r(x, f(x)). Если концом последней связки пути является завершающий оператор HALT: z h(x, y), то будем использовать предикат R''(x, y) R(x, y) ∧ h(x, r(x, y)) ≠ ω ифункцию r''(x, y) h(x, r(x, y)) (r''(x, y) : Dx Dy Dz).Индуктивные утверждения. Пусть P – блок-схема, а = (,) – ее спецификация.
Рассмотрим следующий метод доказательства частичной корректности программы P относительно спецификации .Шаг 1. Точки сечения. Выберем подмножество связок блок-схемы. Эти связки мы будем называть точками сечения. Выбранноемножество точек сечения должно быть таким, чтобы каждый циклв блок-схеме содержал, по крайней мере, одну точку сечения.30Все ориентированные пути между точками сечения, не содержащие других точек сечения, мы будем называть промежуточнымибазовыми путями. Пути, начинающиеся в начальном операторе, заканчиваю-щиеся в точке сечения и не содержащие других точек сечения, мы будем называть начальными базовыми путями.
Пути, начинающиеся в точке сечения, заканчивающиеся в одном из завершающихся операторов и не содержащие других точек сечения, мыбудем называть конечными базовыми путями. И наконец, пути, начинающиеся в начальном операторе, заканчивающиеся в одном иззавершающихся операторов и не содержащие других точек сечения,мы будем называть простыми базовыми путями.Шаг 2. Индуктивные утверждения.
Выберем для каждой точки сечения i предикат pi(x, y), который характеризует отношениемежду переменными блок-схемы при прохождении данной связки.Будем называть эти предикаты индуктивными утверждениями.Кроме того, свяжем входной предикат (x) с начальным оператором блок-схемы, а выходной предикат (x, z) – со всемизавершающими операторами.Шаг 3.
Условия верификации. На третьем шаге сконструируемдля каждого промежуточного базового пути , начинающегося вточке сечения i и завершающегося в точке сечения j, условия верификации: x Dx y Dy [ (x) ∧ pi(x, y) ∧ R(x, y) pj( x, r(x,y) ) ]Эти условия утверждают, что если предикат p i(x, y) истинендля некоторых значений переменных x и y, и эти значения такие,что, начиная из точки сечения i, вычисление пойдет по пути и31успешно достигнет конца пути, то предикат p j(x, y) будет истинендля значений переменных x и y, после прохождения по пути .Для начального базового пути , завершающегося в точке сечения j, условия верификации будут выглядеть следующим образом: x Dx [ (x) ∧ R'(x) pj( x, r'(x) ) ]В этом случае условия утверждают, что если входной предикат(x) истинен для некоторых значений входных переменных и этизначения такие, что начальное вычисление пойдет по пути иуспешно достигнет конца пути, то предикат p j(x, y) будет истинендля значений переменных x и y, после прохождения по пути .Для каждого конечного базового пути , начинающегося в точкесечения i, условия верификации конструируются следующим образом: x Dx y Dy [ (x) ∧ pi(x, y) ∧ R''(x, y) (x, r''(x,y)) ]Здесь условия верификации утверждают, что если предикатpi(x, y) истинен для некоторых значений переменных x и y и этизначения такие, что, начиная из точки сечения i, вычисление пойдет по пути , то предикат (x, z) будет истинен для значенийпеременных x и z после успешного завершения работы блок-схемыпри прохождении по пути .Если в блок-схеме существуют простые базовые пути, то длякаждого такого пути (входящего в оператор HALT с функциейh) условие верификации будут выглядеть следующим образом: x Dx[ (x) ∧ R'(x) ∧ h(x, r'(x)) ≠ ω (x, h(x,r'(x))) ]32В этом случае условия утверждают, что если входной предикат(x) истинен для некоторых значений входных переменных и этизначения такие, что вычисление пойдет по пути и успешно достигнет его конца, то выходной предикат (x, z) будет истинен длязначений переменных x и z после завершения работы блок-схемыпри прохождении по пути .Лемма 5.
Пусть все условия верификации истинны. Пусть дановычисление блок-схемы P, входные переменные которого удовлетворяют входному предикату . Тогда для каждого прохода вычисления Ck – Ck+1 через точку сечения i, предикат pi(x, y) будет истинен на значениях переменных x и y в конфигурации Ck.Теорема 1. (Метод индуктивных утверждений Флойда)Пусть даны блок-схема P и ее спецификация = (, ). Выполним следующие действия:1. Выберем точки сечения;2. Найдем подходящий набор индуктивных утверждений;3. Построим условия верификации для всех базовых путей.Если все условия шага 3 истинны, то блок-схема P частичнокорректна относительно спецификации .Доказательства леммы и теоремы предоставляется читателю вкачестве упражнения.Все шаги метода Флойда, за исключением второго, могут бытьвыполнены относительно автоматически.
А вот выбор подходящегонабора индуктивных утверждений требует хорошего пониманияфункционирования программы и поэтому сложно поддается автоматизации.33Метод фундированных множеств ФлойдаДалее мы рассмотрим метод доказательства завершаемости программ, представленных в виде блок-схем.Напомним некоторые определения. Частично-упорядоченныммножеством (W, ≺) называется непустое множество W и любоебинарное отношение ≺ на этом множестве, которое удовлетворяетследующим свойствам:1. Для всех a, b, c W из a ≺ b и b ≺ c следуетa ≺c [Транзитивность]2.
Для всех a, b W из a ≺ b следует ( b ≺ a ) [Асиметричность]3. Для всех a W ( a ≺ a ) [Иррефлексивность]Знаком ≻ будем обозначать бинарное отношение такое, что длялюбых a, b W a ≻ b тогда и только тогда, когда b ≺ a. Частичноупорядоченное множество (W, ≺) называется фундированным, еслине существует бесконечно убывающей последовательности его элементов, т. е. такой последовательности {ai}, что a1 ≻ a2 ≻ a3 ≻ … .Наиболее известным примером фундированного множества является множество натуральных чисел с отношением порядка <.Пусть P – блок-схема, а – ее входной предикат. Рассмотримследующий метод доказательства завершаемости программы P на.Шаг 1.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
