Постусловие

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

Например: Результат факториала всегда является целым числом и больше или равен 1. Таким образом, программа, которая вычисляет факториал входного числа, будет иметь постусловия, что результат после вычисления будет целым числом и что он будет больше или равно 1. Другой пример: программа, которая вычисляет квадратный корень из входного числа, может иметь постусловия, согласно которым результатом является число и его квадрат равен входному значению.

Постусловия в объектно-ориентированном программировании

В некоторых подходах к проектированию программного обеспечения постусловия, наряду с предусловиями и инвариантами классов , являются компонентами метода создания программного обеспечения по контракту .

Постусловием для любой процедуры является объявление свойств, которые гарантируются после завершения выполнения процедуры. ^[1] Что касается контракта подпрограммы, постусловие дает потенциальным вызывающим сторонам гарантию того, что в случаях, когда подпрограмма вызывается в состоянии, в котором выполняется ее предусловие , свойства, объявленные постусловием, гарантированы.

Эйфелева пример

Следующий пример, написанный на Eiffel, устанавливает значение атрибута класса. hour на основе аргумента, предоставленного вызывающим абонентом a_hour. Постусловие следует за ключевым словом ensure. В этом примере постусловие гарантирует, что в случаях, когда предусловие выполняется (т. е. когда a_hour представляет действительный час дня), что после выполнения set_hour, атрибут класса hour будет иметь то же значение, что и a_hour. Тег " hour_set:" описывает это предложение постусловия и служит для его идентификации в случае нарушения постусловия во время выполнения.

    set_hour (a_hour: INTEGER)
            -- Set `hour' to `a_hour'
        require
            valid_argument: 0 <= a_hour and a_hour <= 23
        do
            hour := a_hour
        ensure
            hour_set: hour = a_hour
        end

Постусловия и наследование

При наличии наследования подпрограммы, унаследованные классами-потомками (подклассами), делают это со своими контрактами, то есть с действующими предусловиями и постусловиями. Это означает, что любые реализации или переопределения унаследованных подпрограмм также должны быть написаны в соответствии с их унаследованными контрактами. Постусловия могут быть изменены в переопределенных процедурах, но их можно только усилить. ^[2] То есть переопределенная процедура может увеличить выгоды, которые она предоставляет клиенту, но не может уменьшить эти выгоды.

См. также

Ссылки

^ Мейер, Бертран , Объектно-ориентированное создание программного обеспечения , второе издание, Prentice Hall, 1997, стр. 342.
^ Мейер, 1997, стр. 570–573.

[1] Мейер, Бертран , Объектно-ориентированное создание программного обеспечения , второе издание, Prentice Hall, 1997, стр. 342.

[2] Мейер, 1997, стр. 570–573.

[1]

[2]