Тема 6.2. Доказательство правильности программ

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

Рассмотрим доказательство правильности программы представленной в примере 6.1. Из таблицы 6.2 следует, что всякий раз, когда попадаем в точку 2, имеем J = I * N.

Попробуем доказать это методом индукции по n – числу проходов через точку 2.

Для доказательства справедливости некоторого высказывания в момент прохождения через какую-либо из точек внутреннего цикла нужно:

1. Показать, что высказывание справедливо при первом попадании в эту точку.

2. Показать что, если при очередном (n-ом) попадании в эту точку высказывание справедливо, то оно справедливо и в следующий раз (если, конечно, мы попадем в эту точку n+1 раз). То есть выполнение цикла не нарушает истинности высказывания – инвариант цикла.

Проведем доказательство блок-схемы в рассмотренном выше примере.

1. Докажем, что при попадании в точку 2: J = I * N:

a. При первом попадании в точку 2 имеем I = 0, J = 0, следовательно

J = I * N = 0 * N = 0 справедливо;

b. Предположим, что в точке 2 справедливо выражение J = I * N для I_n и J_n, т.е. J_n, = I_n * N, далее выполняется цикл и получается новое значение

I_n+1, J_n+1 : I_n+1 = I_n + 1, J_n+1 = J_n + N,

J_n+1 = I_n * N + N (по гипотезе индукции) = (I_n + 1) * N = I_n+1* N ч.т.д.

2. Докажем, что на последнем шаге цикла в точке 2: I = M.

a. При первом попадании в точку 2: I = 0. При последующих попаданиях I увеличивается на единицу. Так как M в программе нигде не изменяется и M³0, то очевидно в какой-то момент I станет равным M.

3. Если в точке 2: I = M, то следовательно J = I * N = M * N. Истинность I = M приведет к переходу в точку 5 с J = M * N ч.т.д.

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

Как можно было заметить из примера, при верификации эталоном для проверки корректности становятся формализованные по спецификации утверждения. Так как утверждения и текст программы готовятся независимо различными специалистами, это увеличивает вероятность обнаружения ошибок.

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

Для верификации программ необходимы три языка:

-язык записи контролируемых текстов программ;

-язык формулировки условий верификации;

-язык формулирования и доказательства свойств корректности.

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