Лекция 9. Аналитическая проверка корректности программ. Верификация программ.

· верификация (verification) – установление соответствия между программой и ее спецификацией.

Спецификацию программы Prgm будем определять путем приписывания индуктивных утвержденийточкам разреза графа потоков управления программы (точкам между операторами программы). При этом выходу оператора STARTприписываетсявходной предикат (предусловие) программы P(x), определяющий множество допустимых значений исходных данных x(xдопустимо, еслиP(x): true), а входу оператора STOPприписываетсявыходной предикат (постусловие) Q(x,y), определяющий целевую функцию программы (связь между входными и выходными данными программы).

Тогда свойство частичной корректности программы определяется следующей формулой логики предикатов:

PCOR(Prgm, P, Q): "x ( P(x) Ù fin(x) Þ Q( x, f(x) ) ),

где fin(x) –предикат завершения программыPrgm, начатой в состоянииx;

f(x) –функция, вычисляемая программойPrgm,

свойство завершенности может быть определено формулой:

FIN(Prgm, P): "x ( P(x) Þ fin(x) ),

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

TCOR(Prgm, P, Q): "x ( P(x) Þ Q(x, f(x) ) Ù fin(x) ).

Аналогичным образом могут быть формализованы и другие перечисленные выше свойства корректности (записать самостоятельно).

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

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

Рассмотрим метод индуктивных утверждений для программ с конечным множеством простых переменных { x₁, x₂, … x_n }, где n³1, а операторами являются:

· операторы присваивания вида x_i := f (x₁, x₂, … x_n);

· составной оператор вида A ; B;

· оператор условного перехода if a(x₁, x₂, … x_n) then L₊ else L_–,

где L₊,L_– – метки операторов, которым передается управление;

· начальный оператор START;

· конечный оператор STOP.

Такой состав структурных компонентов вполне достаточен для представления произвольного алгоритма и поэтому не ограничивает общности излагаемого метода.

Установление частичной корректности осуществляется за четыре последовательных шага.

Шаг 1.Разрезание циклов программы

Очевидно, что при выполнении программы для различных исходных данных возможны различные последовательности операторов, начинающиеся оператором STARTи оканчивающиеся оператором STOP. Назовем такие последовательности трассами вычислений.

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

· путь через тело цикла;

· путь к выходу из цикла.