2015-05-06
870
Этот метод может рассматриваться как дальнейшее развитие метода индуктивных утверждений. Основная идея метода состоит в том, чтобы с каждой контрольной точкой программы, лежащей на циклическом пути, связать некоторую частичную функцию, значения которой ограничены.
Для формализации этой идеи в достаточно общей форме введем понятие фундированного множества.
Пусть S – частично упорядоченное множество относительно бинарного отношения # на его элементах, т.е. на множестве S для a, b и с Î S выполняются свойства:
· антирефлексивности Ø(a # a);
· антисимметрии a # b Þ (Ø(b # a));
· транзитивности a # b Ù b # c Þ a # c.
Множество S называется фундированным, если не существуетбесконечной убывающей последовательности элементов из S.
Примеры фундированных множеств:
· множество натуральных чисел с отношением <;
· множество S* всех слов в алфавите S, включая пустое слово с отношением w1 < w2, означающим что w1 есть собственное подслово w2.
Пусть Prgm – аннотированная программа, для которой методом индуктивных утверждений доказана частичная корректность. С каждой контрольной точкой r, лежащей на циклическом пути (для этой точки существует обратный путь в точку r), свяжем частичную (ограничивающую) функцию yr (x1, …, xn), принимающую значения в фундированном множестве S.
|
|
|
Для каждого пути a между парой соседних контрольных точек r и t (r может совпадать с t), лежащих на циклическом пути, определим условие завершения в виде
Wa: (invr(x1, …, xn) Þ (Ûa(x1, …, xn)) Þ (yr(x1, …, xn)ÎS Ù
yt(ja(x1, …, xn))ÎS Ù yr(x1, …, xn) ~yt(ja(x1, …, xn))))),
где Ua: invr(x1, …, xn) Þ (Ûa(x1, …, xn)) Þ invt(ja(x1, …, xn)) – условие корректности метода индуктивных утверждений, ja – обратное преобразование, осуществляемое на пути a в методе индуктивных утверждений, т.е.
U0 = Ûa(x1, …, xn)Þ invt(ja(x1, …, xn)), где (yr – ограничивающая функция вида X1´ X2´ …´ Xn ® S, приписанная точке r.
Для доказательства завершенности программы методом Флойда может потребоваться усиление инвариантов, используемыхв доказательстве частичной корректности. В целом успех доказательства в значительной мере предопределяется искусством выбора ограничивающих функций y.
