差分
ナビゲーションに移動
検索に移動
; [[事前条件]] (precondition) :[[サブルーチン]]の開始時に、これを呼ぶ側で保証すべき性質。
; [[事後条件]] (postcondition) :[[サブルーチン]]が、終了時に保証すべき性質。が、終了時に保証すべき性質。たとえば「[[戻り値]]は絶対に[[null]]を返さない」などを決めておくことを言う。
; [[不変条件]] (invariant) :[[クラス]]などの[[オブジェクト]]がその外部に公開しているすべての操作の開始時と終了時に保証されるべき、オブジェクト毎に共通した性質。
コードを呼ぶ側が[[事前条件]]と[[不変条件]]を満たす義務を負うことで、呼ばれたコードはその条件が恒真であるとの前提を利益として得る。
