契約プログラミング
クラス不変条件 (class invariant) は、クラスが持つ公開された各メソッドの開始時と正常終了時に共通して保証されるべき状態についての条件である。ただしコンストラクタの呼び出しに関しては、事後条件としてのみ適用され事前条件として保証する必要はない。(引数や返り値などを制約するメソッド個別の事前/事後条件と異なり)不変条件はインスタンスの状態にのみに対する表明である。インスタンスの「状態」はそのインスタンスのすべてフィールドの値によって決まるため、より具体的には、不変条件はフィールドの値に関する表明となる。
不変条件は公開メソッドの事前条件および事後条件として暗黙的に追加される。 不変条件を持つクラスに関して、そのクラスの公開メソッドの呼び出しの際、クライアントはメソッドの事前条件とサプライヤ・クラスの不変条件の両方を満たす義務がある。 またサプライヤは、事前条件(と不変条件)を満たしたメソッド呼び出しに対して、メソッド終了時にそのメソッドの事後条件と不変条件の両方を満たす義務がある。