Применение правил вывода
Для доказательства правильности программы или сегмента программы, необходимо четко определить смысл понятия «корректность» по отношению к рассматриваемой конкретной программе. Кроме того, необходимо знать, по крайней мере, постусловие. Часто также задается предусловие и в таком случае необходимо доказать заданное утверждение о правильности, то есть проверить, действительно ли данное предусловие является предусловием для данного постусловия по отношению к данной программе. В остальных случаях необходимо получить предусловие для данного постусловия и данной программы.
Выбор для применения того или иного правила вывода зависит: во-первых, от вида рассматриваемого оператора программы и, во-вторых, от того, задано ли предусловие или же его следует получить.
Правила вывода DC1 - DС4 можно применять для операторов всех типов и для обеих задач доказательства (проверки и получения предусловия) для разложения длинных условий на малые части. Из правил вывода и их практической применимости при доказательстве правильности программ вытекает ряд требований, которым должна удовлетворять документация на программу.
Первое и наиболее важное из них состоит в том, что предусловия и постусловия необходимо включать в документацию. Их необходимо сформулировать в виде выражений алгебры логики. Эти формулы должны сопровождаться краткими пояснениями на естественном языке и схемами, если последние необходимы в качестве средства облегчения их восприятия читателем. При этом следует учитывать затраты времени и простоту восприятия.
В документации по подпрограмме необходимо четко указывать, на какие переменные не влияет ее выполнение. Обычно данное требование выполняется в результате перечисления всех переменных, которые изменяются (или, что более точно, могут изменяться) рассматриваемой подпрограммой. Совершенно обязательно в документации должен быть указан инвариант цикла для каждого цикла.
Кроме того, в документации необходимо указать те условия (суждения), которые должны быть истинными в определенных местах подпрограммы.
В этом плане особенно удобными являются места между циклами и условными операторами, а также до и после последовательности операторов присваивания. Не требуется включать в документацию те условия, которые можно легко получить непосредственно из других условий. Но в документацию обязательно должны быть включены те условия, которые отражают принятые в работе решения или которые можно получить лишь в результате выполнения длинных алгебраических преобразований, занимающих много времени. Как отмечалось выше, содержащиеся в документации условия будут особенно полезны при последующем доказательстве правильности программы и ее сопровождении (изменении).
Любой программист, который составляет свою программу и включает в нее оператор вызова документированной подпрограммы, должен знать предусловия и постусловия для этой подпрограммы, а также переменные, которые изменяются в результате ее выполнения. Предусловие указывает ему, какое состояние должна подготовить его программа перед вызовом подпрограммы, то есть, что ему следует учитывать перед вызовом. Постусловие сообщает ему о том, что он может считать истинным после вызова подпрограммы.
И хотя методы доказательства правильности программ изо своей «громоздкости» существенно ограничены при доказательстве безопасности большинства программных комплексов, тем не менее, есть области, где данные методы могут найти прикладное значение. Следующий пример характеризует это.
