В компьютерном программировании постусловие — это условие или предикат , который всегда должен быть истинным сразу после выполнения некоторого раздела кода или после операции в формальной спецификации . Постусловия иногда проверяются с помощью утверждений внутри самого кода. Часто постусловия просто включаются в документацию затронутого раздела кода.
Например: Результат факториала всегда является целым числом, большим или равным 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 do hour := a_hour ensure hour_set : hour = a_hour end При наличии наследования процедуры, унаследованные классами-потомками (подклассами), делают это с их контрактами, то есть их предусловиями и постусловиями, в силе. Это означает, что любые реализации или переопределения унаследованных процедур также должны быть написаны для соответствия их унаследованным контрактам. Постусловия могут быть изменены в переопределенных процедурах, но они могут быть только усилены. [2] То есть переопределенная процедура может увеличить преимущества, которые она предоставляет клиенту, но не может уменьшить эти преимущества.