事後条件

コンピュータ プログラミングにおいて、事後条件とは、コードの一部を実行した後、または正式な仕様での操作の後に常に真でなければならない条件または述語です。事後条件は、コード自体の中でアサーションを使用してテストされることがあります。多くの場合、事後条件は、影響を受けるコード セクションのドキュメントに単に組み込まれます。

たとえば、階乗の結果は常に整数で、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' に設定する有効な引数が必要: 0 <= a_hourかつa_hour <= 23であるhour := a_hourであることを確認するhour_set : hour = a_hourであることを確認するend  
            
        
                   
        
              
        
               
        

継承が存在する場合、子孫クラス（サブクラス）に継承されたルーチンは、その契約、つまり前提条件と事後条件を有効にして実行されます。つまり、継承されたルーチンの実装または再定義も、継承された契約に準拠するように記述する必要があります。事後条件は再定義されたルーチンで変更できますが、強化することしかできません。^[2]つまり、再定義されたルーチンは、クライアントに提供する利点を増やすことはできますが、その利点を減らすことはできません。

• 前提条件
• 契約による設計
• ホーア論理
• 条件によって維持される不変量
• データベーストリガー