Лекция 9. Аналитическая проверка корректности программ. Верификация программ.
Корректность является статическим свойством программы, поскольку она не зависит от времени (если, конечно, не изменяются цели разработки) и отражает специфику ошибок разработки программ (ошибок проекта и кодирования).
Различают два типа проверки корректности:
· валидация (validation) – установление соответствия между тем, что делает программа, и тем, что нужно Заказчику;
· верификация (verification) – установление соответствия между программой и ее спецификацией.
Определение верификациии симметрично ввиду относительного характера свойства корректности: если программа не соответствует своей спецификации, то либо программа, либо спецификация, либо оба этих объекта содержат ошибки. Перефразируя известное изречение Э.Дейкстры о тестировании программ, можно сказать, что верификация способна доказать отсутствие ошибок в программе, но не всегда доказывает их присутствие.
В отличие от тестирования верификацияпредполагает аналитическое исследование свойств программы по ее тексту (без выполнения программы). Таким образом, для проведения верификации необходимо построить формально-логическую систему, в которой были бы формально определены свойства корректности программы. Для этих целей наиболее широкое применение получило исчисление предикатов первого порядка, расширенное аксиоматической арифметикой.
Можно сказать, что верификация – это вычисление истинности предикатаот двух аргументов: программы и спецификации. Истинность этого предиката устанавливает свойство корректности программы, если спецификация не содержит ошибок, однако, его ложность, вообще говоря, не означает наличие ошибок в программе, а требует более точного разбора.
Учитывая специфику проявления ошибок в программах в процессе их выполнения на ЭВМ, целесообразно выделить в понятие корректности программы два свойства:
· частичную корректность – удовлетворение внешним(входной и выходной) спецификациямпрограммы при условии завершения выполнения программы;
· завершенность – достижение в процессе выполнения выхода программы при определенных входной спецификацией данных.
Свойство завершенностине является тривиальнымдля такого объекта, как программа, ввиду возможности циклических и рекурсивных вычислений, а также наличия частично-определенных операций. Случаи, когда свойство завершенности не удовлетворяется, довольно обычны для программ с ошибками, и приводят к заведомо некорректным программам независимо от спецификации выхода.
Каждое из двух выделенных свойств корректности программы может удовлетворяться или не удовлетворяться. Таким образом, можно выделить шесть основных задач анализа корректности программы:
· частичная корректность (при условии завершенности);
· завершенность программы;
· незавершенность программы;
· тотальная корректность (частичная корректность и завершенность);
· частичная некорректность (некорректность при условии завершенности);
· некорректность (незавершенность или частичная некорректность).
Разделение свойств частичной корректности и завершенности следует рассматривать как методологический прием, направленный на уменьшение сложности верификации программ.
Рассмотрим формальные постановки задач анализа корректности.
Введем ограничение: будем рассматривать программы, начинающиеся оператором START(первый выполняемый оператор) и заканчивающиеся оператором STOP(последний выполняемый оператор).
Спецификацию программы 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) ).
Аналогичным образом могут быть формализованы и другие перечисленные выше свойства корректности (записать самостоятельно).
Заметим, что для произвольных программ каждое из этих свойств (завершенность и частичная корректность) является алгоритмически неразрешимым, т.е. не существует алгоритма, позволяющего оценить истинность соответствующих формул логики предикатов. Однако для отдельных классов программ в настоящее время разработаны достаточно эффективные методы верификации, позволяющие вручную или автоматически проводить соответствующие доказательства. Такие методы могут рассматриваться как составная часть процессов разработки и отладки программ, обеспечивая логическую завершенность этих процессов.
Наиболее распространенным методом доказательства частичной корректности программ является метод индуктивных утверждений, предложенный Флойдом. Он позволяет свести доказательство частичной корректности программы к доказательству некоторого конечного числа утверждений, записанных на языке исчислений предикатов первого порядка и имеющих интерпретацию в соответствующей проблемной области.
Рассмотрим метод индуктивных утверждений для программ с конечным множеством простых переменных { x1, x2, … xn }, где n³1, а операторами являются:
· операторы присваивания вида xi := f (x1, x2, … xn);
· составной оператор вида A ; B;
· оператор условного перехода if a(x1, x2, … xn) then L+ else L–,
где L+,L– – метки операторов, которым передается управление;
· начальный оператор START;
· конечный оператор STOP.
Такой состав структурных компонентов вполне достаточен для представления произвольного алгоритма и поэтому не ограничивает общности излагаемого метода.
Установление частичной корректности осуществляется за четыре последовательных шага.
Шаг 1.Разрезание циклов программы
Очевидно, что при выполнении программы для различных исходных данных возможны различные последовательности операторов, начинающиеся оператором STARTи оканчивающиеся оператором STOP. Назовем такие последовательности трассами вычислений.
Сложность анализа частичной корректности программы разбиением на трассы заключается в том, что при наличии циклов в программе он не может быть выполнен непосредственным перебором всех трасс. Эта сложность может быть преодолена путем включения в граф потока управления программы конечного числа точек, называемых точками разреза, таким образом, что каждый цикл содержит одну такую точку, которая “разрезает” циклические пути на два:
· путь через тело цикла;
· путь к выходу из цикла.
Дата добавления: 2015-08-26; просмотров: 1544;