Структуры данных и модели вычислений
Методика доказательства правильности программ
Рассматриваемая методика предназначена для доказательства правильности алгоритмов, представленных в виде графов, вершинам которых поставлены в соответствие операторы над памятью, а дугам — переходы от оператора к оператору. Одну из вершин назовем входной, ей соответствует оператор, с которого начинается выполнение алгоритма, а выходных вершин может быть несколько. Считаем, что входная и выходная вершины помечены, соответственно, входящей и выходящей стрелками. Такие представления алгоритмов называют блок-схемами. Доказать правильность алгоритма — это значит доказать следующее утверждение:
- Если входные данные удовлетворяют входному условию, то алгоритм через конечное число шагов завершает работу и выходные данные удовлетворяют требуемому выходному условию.
На практике такое утверждение часто разбивают на два.
- Если входные данные удовлетворяют входному условию и алгоритм через конечное число шагов завершает работу, то выходные данные удовлетворяют требуемому выходному условию.
- Если входные данные удовлетворяют входному условию, то алгоритм через конечное число шагов завершает работу.
Алгоритм, для которого доказано утверждение 1, называется частично правильным или частично корректным. Если же доказаны утверждения 1 и 2, то алгоритм называется правильным или корректным.
Заметим, что когда доказательство утверждения 2 представляет непреодолимые трудности, то ограничиваются доказательством утверждения 1. Таковы, например, итерационные алгоритмы, для которых неизвестна область сходимости. В таком случае, если алгоритм в приемлемое время завершает свою работу, то правильность ответа гарантируется.
Остановимся на доказательстве частичной корректности. Методика заключается в следующем:
- Для контроля над ходом вычислений выбираются так называемые контрольные дуги. К числу контрольных обязательно относят входную и все выходные дуги, а также некоторое количество других дуг, так, чтобы в граф-схеме алгоритма оказались "разрезанными" все циклы.
- Для каждой контрольной дуги формулируется индуктивное условие, которому предположительно должно удовлетворять содержимое памяти алгоритма при каждом его прохождении через рассматриваемую дугу. Считаем, что все контрольные дуги (в дальнейшем будем называть их контрольными точками) и соответствующие им индуктивные утверждения пронумерованы.
- Для каждой пары , контрольных точек, для которых в блок-схеме имеется путь из в , минующий другие контрольные точки, выбираются все такие пути, и для каждого выбранного пути доказывается утверждение (индуктивный шаг): "Если при очередном проходе через точку выполнялось индуктивное предположение и если реализуется рассматриваемый путь, то при достижении точки
будет выполняться условие ".
Если все индуктивные шаги доказаны, то, используя принцип математической индукции, можно утверждать частичную корректность алгоритма. Для доказательства полной корректности остается доказать завершаемость программы через конечное число шагов.
