Анализ завершенности последовательных программ
Особенность свойства завершенности программ состоит в том, что оно не зависит от постусловия программы, и для заданной программы полностью определяется предусловием. В общем случае формальный анализ свойства завершенности представляет весьма сложную проблему.
Имеются по меньшей мере две причины, по которым программа с заданным предусловием P может не завершиться:
· обращение к частично определенной функции со значением аргументов вне области определения;
· зацикливание.
Первая причина может приводить к аварийному завершению даже нециклических программ (например, при делении на нуль). Вторая причина присуща программам с итеративными циклами.
Ограничимся рассмотрением методов анализа завершения циклических вычислений без учета других возможных причин незавершения, т.е. предполагается, что любой нециклический оператор завершается и передает управление на его выход.
Наибольшее распространение получили два метода логического анализа завершения циклических вычислений:
· метод Флойда;
· метод счетчиков.
Метод Флойда
Этот метод может рассматриваться как дальнейшее развитие метода индуктивных утверждений. Основная идея метода состоит в том, чтобы с каждой контрольной точкой программы, лежащей на циклическом пути, связать некоторую частичную функцию, значения которой ограничены.
Для формализации этой идеи в достаточно общей форме введем понятие фундированного множества.
Пусть 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.
Метод счетчиков
Идея этого метода состоит во введении в программу Prgm новых переменных-счетчиков, добавляемых по одной в каждый цикл программы. Переменная-счетчик должна инициализироваться перед входом в цикли увеличивать свое значение при каждом прохождении по циклу.
В преобразованной таким образом программе Prgm’ измененные инварианты циклов представляются в виде, содержащем условие ограниченности значений счетчиков функциями, зависящими только от входных переменных.
В отличие от метода Флойда этот метод не требует введения ограничивающих функций в контрольных точках. Переменные-счетчики рассматриваются как органическая часть программы, позволяющая логически выразить свойство завершенности в инвариантах цикла.
Преимущество этого метода перед методом Флойда состоит в том, что одни и те же инварианты используются при доказательстве частичной корректности и завершенности. Однако метод Флойда обладает большей общностью.
Успех доказательства завершенности в методе счетчиков определяется тем, удастся ли подобрать соответствующее условие ограниченности счетчика в инварианте цикла.
Этот метод, так же как и метод Флойда, требует творческого подхода программиста.
Дата добавления: 2015-08-26; просмотров: 1144;