§ 23. Понятие правильности и сложности алгоритма

23.2. Правильность алгоритма

Алгоритм обладает свойством массовости, т. к. исходными данными для него может быть любая конечная последовательность символов. Алгоритм не обладает этим свойством, если он работает лишь на ограниченном наборе исходных данных, но на остальных наборах не работает или работает неправильно.

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

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

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

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

Идея математического доказательства корректности программ (верификации) обычно сводится к доказательству того факта, что программа (подпрограмма) является корректной относительно ее входной и выходной спецификации. Наиболее известный метод, называемый методом индуктивных утверждений, был предложен в 1967 г. Флойдом, хотя сама идея его восходит к Тьюрингу (1950).

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

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

Принцип верификации был выдвинут Венским кружком в 20-е гг. XX в. Члены кружка полагали, что в науке должны остаться два класса научных предложений — аналитические истины, не имеющие предметного содержания, и фактические истины, эмпирические факты конкретных наук, значение которых может быть проверено особым способом – принципом верификации.  Однако вскоре стало очевидным, что такой прямой верификационизм невозможен в тех случаях, когда мы имеем дело с событиями прошлого, с общими суждениями и т. д.