Предусловия и постусловия в доказательствах правильности

Условие — это алгебраическое выражение, значение которого либо «ложно», либо «истинно». Обычно в выражениях присутствуют имена переменных программы; каждому имени соответствует значение соответствующей переменной. Условия также называют логическими или булевыми выражениями или суждениями.

Если из истинности условия V непосредственно перед выполнением оператора S следует истинность условия Р после выполнения этого оператора, то говорят, что V есть предусловие для постусловия Р по отношению к оператору S. Подобная взаимозависимость V, Р и S обычно записывается как {У} S {Р}. Оператор S может быть простым или составным, содержащим любое число отдельных операторов, т. е. может быть сегментом программы или же целой программой.

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

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

Предусловия и постусловия представляют ключевые моменты в доказательствах корректности. Они выражают понятие «корректность» конкретной программы или сегмента программы. Записанные различным образом, предусловие и постусловие вместе образуют общую спецификацию рассматриваемой программы. Основные части стандартного доказательства правильности используют предусловия и постусловия и, в частности, их взаимозависимости.

Иногда можно алгебраическим путем вывести предусловие для заданного постусловия и заданного оператора (простого или составного). Такой подход особенно плодотворен в случае операторов присваивания. Часто задача сводится к проверке (доказательству) утверждения о корректности предусловий и постусловий сегмента программы. В таком случае доказываемое утверждение о корректности разбивается на утверждения о корректности частей рассматриваемого сегмента программы, и они доказываются раздельно с помощью ряда полезных правил, которые будут рассмотрены ниже.