問題タブ [design-by-contract]

私はcontract.pyで遊んでいます.Terrence WayのPython用のデザインバイコントラクトのリファレンス実装です。コントラクト (事前条件/事後条件/不変条件) に違反すると、実装は例外をスローしますが、メソッドに複数のコントラクトが関連付けられている場合に、どの特定のコントラクトが失敗したかを簡単に特定する方法は提供しません。

たとえば、circbuf.pyの例を取り上げて、次のように負の引数を渡して前提条件に違反するとします。

次に、次のようなトレースバックを取得します。

私の推測では、PreconditionViolationError (4) の 2 番目の引数は、circbuf の行番号を参照しています。アサーションを含むinit docstring:

ただし、ファイルを開いて docstring の行番号を数えなければならないのは面倒です。どの契約が失敗したかを特定するためのより迅速な解決策を誰かが持っていますか?

(この例では前提条件が 1 つであるため、明らかですが、複数の前提条件が可能であることに注意してください)。

Python のコントラクトを使用して、事前条件/事後条件/不変条件を指定しています。また、単体テストを行うために doctests を使用しています。

コントラクトを有効にしてすべてのdoctest単体テストを実行したいと思います。残念ながら、nose でテストを実行すると、前/後/不変アサーションが実行されません。各 .py ファイルにセットアップ関数を配置して、確実contract.checkmodに呼び出されるようにします

テストを実行する前に、この関数がノーズによって実行されていることを確認できますが、コントラクトはまだ実行されません。

一方、 を呼び出して doctest を実行するとdoctest.testmod、pre/post/inv が呼び出されます。

これは、直接呼び出された場合はテストが成功するが、nose で呼び出された場合は失敗する Python スクリプトの例です。

上記のファイルをスタンドアロンで実行すると、テストに合格します。

ここに鼻があります：

数年前、私は Java 用の DbC パッケージの調査を行いましたが、完全に満足できるものはありませんでした。残念ながら、私は自分の調査結果を適切に記録していませんでした。状況が変化したと思います。Java 用のさまざまな DbC パッケージを比較対照したい人はいますか?

C ++アプリケーションでの契約原則による設計の実装を支援するライブラリはありますか？

特に、このような原理の使い方を備えた図書館を探しています。

私は Design by Contract の概念にかなり慣れていませんが、今のところ、潜在的なバグを簡単に見つけられる点が気に入っています。

ただし、Microsoft.Contracts ライブラリ (これは非常に優れています) を使用して作業しており、障害に遭遇しました。

私がやろうとしていることのこの単純化された例を見てください:

要約すると、プラグインが従うインターフェイスを宣言し、状態を宣言するように要求し、任意の状態で呼び出すことができるものを制限しています。

これは、静的検証とランタイム検証の両方で、呼び出しサイトで機能します。Resetしかし、私が得続ける警告は、関数と関数の両方に対して「契約：証明されていないことを保証します」ですPrepare。

私は s を試してみましたが、制約Invariantを証明するのに役立つとは思われません。Ensures

インターフェイスを介して証明する方法についてのヘルプは役に立ちます。

EDIT1：

これを MyAwesomePlugin クラスに追加すると:

IPlugin としての状態が私のプライベート状態と同じであることをほのめかそうとすると、同じ警告が表示され、さらに「private int? number = null」行が不変条件を証明できないという警告が表示されます。

それが静的コンストラクターの最初の実行可能行であることを考えると、なぜそう言うのかがわかりますが、それが ? を証明しないのはなぜEnsuresですか?

EDIT2

でマークStateする[ContractPublicPropertyName("State")] と、「'MyNamespace.State' 型の 'State' という名前のパブリック フィールド/プロパティが見つかりません」というエラーが表示されます。

これは私をより近づけるはずですが、私はまだそこにいません。

静的チェッカーを使用して Microsoft.Contacts をインストールできるという Visual Studio Team System の要件とは別に、チーム システムなしで静的チェッカーを実行することは可能ですか? それとも、スタジオのチーム システム コンポーネントによって公開されている API に依存していますか?

また、スタティックチェッカーをチームシステムのコンピュータからプロのコンピュータにコピーすることはライセンス内ですか?

DbCメソッドでは、関数に事前条件と事後条件がついていることがわかりました。

私が疑問に思っているのは、それがメンバー関数にも当てはまるかどうかです。

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

編集：（私の例をクリーンアップ）

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

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

編集：

事後条件は、不変条件のサブセットをチェックしているだけではありませんか?

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

ありがとう。

トーナメントでラウンドを実行するアプリケーションがあり、この単純化されたコード構造に関する契約警告が表示されます。

警告は次のとおりです。

私は何が間違っているのですか？どうすればこれを証明できIList<T>ますか？これは静的アナライザのバグですか？バグレポートをMicrosoftに送信するにはどうすればよいですか？

エッフェルコミュニティの外で実際に契約による設計がどれだけ使用されているのか知りたいです。契約による設計を使用するアクティブなオープンソースプロジェクトはありますか？

または、質問を1つにまとめると、単一の答えがあります。契約による設計を使用する、最も広く使用されている（Eiffel以外の）オープンソースプロジェクトは何ですか？

最近 Visual Studio 2010b2 をダウンロードしましたが、Microsoft 契約の静的チェッカーに関するいくつかの質問を再評価したいと思いました。

コードの名前空間を使用してほとんどのコードを再利用System.Diagnostics.Contractsできましたが、静的チェッカーを有効にする方法がわかりません。追加のプラグインが必要ですか?

VS2010 では、契約による設計は「そのまま機能する」はずだという印象を受けました。

ご協力いただきありがとうございます。