事後条件

Postconditionとは、Preconditionを満たして開始したOperationが契約どおり完了した後に、提供側が成立を保証するConstraintです。

SimpleModelingでは、結果値、Stateの変化、生成されたEvent、関連Objectとの整合をPostconditionとして表します。成功時と失敗時のOutcomeが異なる場合は、それぞれの保証を区別します。