Анализ завершенности последовательных программ

Особенность свойства завершенности программ состоит в том, что оно не зависит от постусловия программы, и для заданной программы полностью определяется предусловием. В общем случае формальный анализ свойства завершенности представляет весьма сложную проблему.

Имеются по меньшей мере две причины, по которым программа с заданным предусловием P может не завершиться:

· обращение к частично определенной функции со значением аргументов вне области определения;

· зацикливание.

Первая причина может приводить к аварийному завершению даже нециклических программ (например, при делении на нуль). Вторая причина присуща программам с итеративными циклами.

Ограничимся рассмотрением методов анализа завершения циклических вычислений без учета других возможных причин незавершения, т.е. предполагается, что любой нециклический оператор завершается и передает управление на его выход.

Наибольшее распространение получили два метода логического анализа завершения циклических вычислений:

· метод Флойда;

· метод счетчиков.

Метод Флойда

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

Для формализации этой идеи в достаточно общей форме введем понятие фундированного множества.

Пусть S – частично упорядоченное множество относительно бинарного отношения #на его элементах, т.е. на множестве Sдля a, bи с Î Sвыполняются свойства:

· антирефлексивности Ø(a # a);

· антисимметрии a # b Þ (Ø(b # a));

· транзитивности a # b Ù b # c Þ a # c.

Множество Sназывается фундированным, если не существуетбесконечной убывающей последовательности элементов из S.

Примеры фундированных множеств:

· множество натуральных чисел с отношением <;

· множество S^* всех слов в алфавите S, включая пустое слово с отношением w₁ < w₂, означающим что w₁ есть собственное подслово w₂.

Пусть Prgm – аннотированная программа, для которой методом индуктивных утверждений доказана частичная корректность. С каждой контрольной точкой r, лежащей на циклическом пути ( для этой точки существует обратный путь в точку r), свяжем частичную (ограничивающую) функцию y_r (x₁, … , x_n), принимающую значения в фундированном множестве S.

Для каждого пути aмежду парой соседних контрольных точек rи t(rможет совпадать с t), лежащих на циклическом пути, определим условие завершения в виде

W_a: ( inv_r(x₁, …, x_n) Þ (_Ûa(x₁, …, x_n)) Þ (y_r(x₁, …, x_n)ÎS Ù

y_t(j_a(x₁, …, x_n))ÎS Ù y_r(x₁, …, x_n) ~y_t(j_a(x₁, …, x_n))))),

где U_a: inv_r(x₁, …, x_n) Þ (_Ûa(x₁, …, x_n)) Þ inv_t(j_a(x₁, …, x_n))– условие корректности метода индуктивных утверждений, j_a –обратное преобразование, осуществляемое на пути aв методе индуктивных утверждений, т.е.

U₀ = _Ûa(x₁, …, x_n)Þ inv_t(j_a(x₁, …, x_n)), где (y_r –ограничивающая функция видаX₁´ X₂´ …´ Xn ® S, приписанная точке r.

Для доказательства завершенности программы методом Флойда может потребоваться усиление инвариантов, используемыхв доказательстве частичной корректности. В целом успех доказательства в значительной мере предопределяется искусством выбора ограничивающих функций y.

Метод счетчиков

Идея этого метода состоит во введении в программу Prgm новых переменных-счетчиков, добавляемых по одной в каждый цикл программы. Переменная-счетчик должна инициализироваться перед входом в цикли увеличивать свое значение при каждом прохождении по циклу.

В преобразованной таким образом программе Prgm’ измененные инварианты циклов представляются в виде, содержащем условие ограниченности значений счетчиков функциями, зависящими только от входных переменных.

В отличие от метода Флойда этот метод не требует введения ограничивающих функций в контрольных точках. Переменные-счетчики рассматриваются как органическая часть программы, позволяющая логически выразить свойство завершенности в инвариантах цикла.

Преимущество этого метода перед методом Флойда состоит в том, что одни и те же инварианты используются при доказательстве частичной корректности и завершенности. Однако метод Флойда обладает большей общностью.

Успех доказательства завершенности в методе счетчиков определяется тем, удастся ли подобрать соответствующее условие ограниченности счетчика в инварианте цикла.

Этот метод, так же как и метод Флойда, требует творческого подхода программиста.