Постусловие

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

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

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

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

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

Пример Эйфелевой [ править ]

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

    set_hour   (  a_hour  :   INTEGER  ) 
             — Установите для `hour' значение `a_hour' 
         require 
             valid_argument  :   0   <=   a_hour   и   a_hour   <=   23 
         dohour 
             :   =   a_hour 
         убедитесь, 
             что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]