postcondition (постусловие)

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

См. invariant; precondition.

Структура

Постусловие моделируют в виде ограничения, имеющего стереотип "postcondition", который прикрепляется к операции.

Нотация

Постусловие изображается в виде примечания с ключевым словом "postcondition". Примечание присоединяется к соответствующей операции.

Пример

На рис. 145 изображено постусловие для операции сортировки массива. Новое значение массива (а) связано с исходным его значением (а). Выражение в данном примере написано на структурированном естественном языке. Можно также пользоваться и более формальным языком.