Тема 6.1. Основные принципы верификации программ

Понятие корректности (правильности) подразумевает соответствие проверяемого объекта некоторому эталонному объекту или совокупности формализованных эталонных характеристик и правил.

Корректность программы при ее разработке определяется степенью ее соответствия программной спецификации.

Программная спецификация – это документ, в котором формулируются в требованиях к программе.

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

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

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

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

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

В этом случае доказательство правильности состоит из доказательства того, что:

- программа, будучи запущенной, в конце концов, будет закончена;

- после окончания программы будет справедливо утверждение о правильности.

Проиллюстрируем эти идеи на примере очень простой программы.

Пример 6.1. Предположим, что нужно вычислить произведение двух любых целых чисел M, N, причем M ³ 0 и операцию умножения использовать нельзя. Для этого можно использовать операцию сложения и вычислить сумму из M слагаемых (каждое равно N). В результате получим M*N.

Рассмотрим блок-схему, реализующую такое вычисление (рис.6.1).

Рис.6.1. Блок-схема, реализующая задачу в примере 6.1.

Нужно доказать, что приведенная программа правильно вычисляет произведение двух любых целых чисел M и N при условии, что M ³ 0, то есть если программа выполняется с целыми числами M и N, где M ³ 0, то она в конце концов окончится (достигнув точки 5) со значением J = M * N.

Сформулируем все необходимые утверждения и сопоставим их различным точкам блок-схемы (рис.5.2).

M, N – целые значения, M ³ 0 - Утверждение о данных

при каждом попадании в эту точку J = I * N - Утверждение об инварианте цикла

на последнем шаге цикла в этой точке I = M. -Утверждение о конечности цикла

попадаем в эту точку с J = M * N - Утверждение о правильности программы

Рис.6.2. Блок-схема с введенными утверждениями о правильности

Чтобы удостовериться в правильности работы блок-схемы можно проверить ее на некоторых фиксированных данных, например, M = 3, N = 5. Результат дожжен быть равен 15, то есть в точку 5 мы должны прийти со значением J = 15.

Трассировка на фиксированных данных приведена в табл.6.1.

Число проходов N через точку 2	Значение I	Значение J

Таблица 6.1. Трассировка блок-схемы на фиксированных данных

Таким образом, можно убедиться, что при M = 3 и N = 5 блок-схема работает верно. Хотя это и укрепляет уверенность в правильности работы программы, но тем не менее никак не доказывает, что программа будет работать правильно при всех возможных значениях M и N.

Обобщим трассировку для некоторых произвольных значениях M и N.

Трассировка на символьных данных приведена в табл. 6.2.

Число проходов N через точку 2	Значение I	Значение J
...	...	...
M +1	M	M*N

Таблица 6.2. Трассировка блок-схемы на символьных данных

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

Как определить, какие значения I и J должны стоять после этого пробела? Как можно быть уверенным, что именно такие?

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

Ответ на второй вопрос требует доказательства.