Теория и практика защиты программ



Применение правил вывода - часть 2


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

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

И хотя методы доказательства правильности программ изо своей «громоздкости» существенно ограничены при доказательстве безопасности большинства программных комплексов, тем не менее, есть области, где данные методы могут найти прикладное значение. Следующий пример характеризует это.




Содержание  Назад  Вперед