契約による設計を行う場合、メンバー関数の不変条件に加えて、事前条件と事後条件が必要ですか？

StackOverflow https://stackoverflow.com/questions/1219564

質問

DbCメソッドでは、前提条件と事後条件が関数に付加されることを理解しています。

私が思っているのは、それがメンバー関数にも適用されるかどうかです。

たとえば、各パブリック関数の最初と最後で不変式を使用すると、メンバー関数は次のようになります。

編集：（私の例を整理しました）

void Charcoal::LightOnFire() {
  invariant();
  in_LightOnFire();

  StartBurning();    
  m_Status = STATUS_BURNING;
  m_Color = 0xCCCCCC;

  return; // last return in body

  out_LightOnFire();
  invariant();
}

inline void Charcoal::in_LightOnFire() {
  #ifndef _RELEASE_
  assert (m_Status == STATUS_UNLIT);
  assert (m_OnTheGrill == true);
  assert (m_DousedInLighterFluid == true);
  #endif
}

inline void Charcoal::out_LightOnFire() {
  #ifndef _RELEASE_
  assert(m_Status == STATUS_BURNING);
  assert(m_Color == 0xCCCCCC);
  #endif
}

// class invariant
inline void Charcoal::invariant() {
  assert(m_Status == STATUS_UNLIT || m_Status == STATUS_BURNING || m_Status == STATUS_ASHY);
  assert(m_Color == 0x000000 || m_Color == 0xCCCCCC || m_Color == 0xEEEEEE);
}

グローバル/ジェネリック関数のみで事前条件と事後条件を使用し、クラス内で不変式のみを使用しても問題ありませんか？

これはやりすぎのように思えますが、私の例は悪いかもしれません。

編集：

事後条件は不変式のサブセットをチェックするだけではありませんか？

上記では、 http://www.digitalmars.comの指示に従っています。 /ctg/contract.html には、「クラスコンストラクターの完了時、クラスデストラクターの開始時、パブリックメンバーの実行前、パブリック関数の終了後に不変式がチェックされます」＆quot;

ありがとう。

役に立ちましたか？

解決

はい。

クラスCの不変は、すべてのインスタンス（オブジェクト）に共通のプロパティです。不変式は、オブジェクトが意味的に有効な状態にある場合にのみtrueと評価されます。

エレベーターの不変式には、 ASSERT（IsStopped（）|| Door.IsClosed（））などの情報が含まれる場合があります。ドアを開けたまま）

対照的に、 MoveTo（int flat）などのメンバー関数は、事後条件として CurrentFlat（）== flat を持つ場合があります。 MoveTo（6）の呼び出し後、現在のフラットは6であるためです。同様に、前提条件として IsStopped（）が含まれる場合があります。エレベータが既に移動している場合、MoveTo関数を呼び出しません。まず、その状態を照会し、停止していることを確認してから、関数を呼び出す必要があります。

もちろん、エレベーターの仕組みを完全に単純化しすぎているかもしれません。

いずれの場合でも、一般に、不変条件として前提条件と事後条件は意味がありません。有効な状態にするためにエレベーターが6階にある必要はありません。

より簡潔な例は、ここにあります：インターセプションと属性：Sasha Goldshteinによる契約ごとのサンプル。

他のヒント

クラスのコントラクトを不変式に制限することは最適ではありません。

前提条件と事後条件は、不変条件のサブセットではありません。

不変条件、前提条件、および事後条件の役割は大きく異なります。

不変条件は、オブジェクトの内部一貫性を確認します。コンストラクタの最後と各メソッド呼び出しの前後で有効である必要があります。

前提条件は、オブジェクトの状態と引数がメソッドの実行に適していることを確認します。前提条件は不変条件を補完します。引数のチェック（型自体、つまりnullではない、＆gt; 0など）のチェックをカバーしますが、オブジェクトの内部ステータス（つまり、file.write（＆quotの呼び出し） ; hello＆quot; ）は、file.is_rwおよびfile.is_openがtrueの場合にのみ有効な呼び出しです。

事後条件は、メソッドがその義務を満たしていることを確認します事後条件は、不変条件を補完します。もちろん、オブジェクトのステータスはメソッドの実行後に一貫している必要がありますが、事後条件は期待されるアクションが実行されたことを確認しています（つまりlist.add（i）はlist.has（i）がtrueであるという結果になるはずです）およびlist.count = old list.count + 1）。

さて、不変式のポイントは、常にオブジェクトに当てはまる何かを記述することです。この場合、グリルに何かが入っているか、入っていない（間には何もない）。通常、オブジェクトの状態全体のプロパティを記述します。

事前条件と事後条件は、メソッドが実行される直前および直後に真であり、メソッドによって変更されるべき状態だけに関係することを示します。これは、おそらくオブジェクトの状態とは異なります。事前条件と事後条件は、メソッドのフットプリントを記述するものと考えることができます-必要なもの、触れたもの。

それで、特定の質問に対して、アイデアは異なることをするので、両方を望むかもしれません。確かに、事前条件と事後条件の代わりに不変条件を使用することはできません-この例では、オブジェクト不変条件の一部は「何かがグリル上にあるかどうか」ですが、lightOnFireの前提条件はアイテムがグリル上にあることを知る必要があります。オブジェクトの不変量からこれを推測することはできません。事前条件と事後条件、および既知の開始状態から、オブジェクトの構造がメソッドを介してのみ変更可能であり、事前条件と事後条件がすべての環境変化を記述すると仮定すると、オブジェクト不変式を推測できます。ただし、これは複雑になる可能性があり、「言語で」と述べている場合は、両方を提供する方が簡単です。

もちろん、ブール値の項目がtrueまたはfalseであると述べるバリアントで行うことは少し無意味です-型システムはそれを保証します。

ライセンス： CC-BY-SA と 帰属
所属していません StackOverflow
scroll top