問題タブ [code-contracts]

私は Code Contracts にかなり慣れていません...そして問題に遭遇しました。

私は次のようなメソッドLINQクエリを持っています:

そして、プロジェクトにコード コントラクトを実装したいと考えています。この時点に到達するまで、すべてを正常に実行しました。静的チェッカーを実行すると、クエリで定義されている変数 p と fAttr に関するいくつかの前提条件 (Contract.Requires) を追加する必要があることが示唆されます。また、証明されていない要件がいくつかあります。

どうすればこれを解決できますか? 何か案は？

MyClass には、次の 2 つの前提条件も含まれています。

前もって感謝します ：）

INotifyPropertyChanged の正しい実装を強制する簡単な方法を探しています。つまり、PropertyChanged が発生したときに、実際に定義されているプロパティを参照する必要があります。Microsoft の新しい CodeContract ツールでこれを実行しようとしましたが、「CodeContracts: requires unproven」という警告が引き続き表示されます。これが私のコードです...

とにかくこれを機能させる方法はありますか？

私は Microsoft DevLabs Code Contracts 静的アナライザーを採用しようとしましたが、それが自分なのかそれとも彼らなのか実際にはわからない状況に直面しました。コードは次のとおりです。

静的アナライザーは、コメントされた事後条件とアサートを証明できなかったと主張します。いつそれが間違っているのかわかりませんでした。

編集asserts を asserts に置き換えても、事後条件はまだ証明されていません。

.NET 4.0 コード コントラクトで使用する静的アナライザーは、Visual Studio の Team Suite エディションでのみ利用できるようです。これは、私のチームの予算をはるかに超えています。

コントラクト スタイル コード (必ずしも .net コード コントラクトを使用する必要はありません) による設計の同様の静的分析を提供する代替手段 (オープン ソース、無料、または手頃な価格) はありますか。完全な価値はBCL自体が契約を結んだときにのみ発生するため、答えはノーになると思いますが、途中で進むものはありますか?

asp.netのMicrosoft.Contracts名前空間が必要なのは何ですか?

つまり、どのような場合に書くことができますusing Microsoft.Contracts;か?

私は最近コードコントラクトに出くわし、C＃プロジェクトでそれらを使い始めました。ただし、C ++/CLIで記述されたプロジェクトもいくつかあります。

C＃およびVBの場合、コードコントラクトは、プロジェクトのプロパティダイアログに便利な構成パネルを提供します。C ++ / CLIプロジェクトの場合、そのようなパネルはありません。

ドキュメントから、C ++ / CLIプロジェクトにコードコントラクトのサポートを追加することは、ビルドプロセスの一部としていくつかの外部ツール（つまり、、、および）を呼び出すだけの簡単な問題であるという印象を受けccrefgen.exeましcccheck.exeたccrewrite.exe。ただし、コマンドラインオプションの数と呼び出しシーケンスに関する制限により、私は多少不安になりました。

Visual Studioのビルドプロセスの自動化された部分としてコードコントラクトツールを実行する簡単な方法を誰かに教えてもらえますか？

VS2010 Beta 2 で利用可能なコード コントラクト ツールを使用して、インターフェイス、そのインターフェイスのコントラクト クラス、およびインターフェイスを実装する 2 つのクラスを定義しました。

コードをテストするときは、実装クラスをテストして、それらの機能が正しいことを確認し、コントラクト コードをテストして、条件が正しいことを確認したいと考えています。

2 つの実装クラスのそれぞれで各コントラクト ステートメントをテストできますが、それは明らかに冗長です。これらの実装クラスのいずれかでテストを作成することもできますが、それは少し間違っているようです。どちらを選択するか、コントラクトを変更するときにどれを更新するかを覚えておくなどです。

実際のインターフェイス コントラクト クラスをテストしたいのですが、コンパイル時に、テストしたいインターフェイス メソッドがインターフェイス コントラクト クラスで使用できないというあらゆる種類の警告が表示されます。コントラクト コードを実装クラスに実際に挿入するコンパイル後の魔法が発生していることはわかっていますが (ILDASM で確認できます)、インターフェイスのコントラクト クラス メソッドを調べると、MISL に存在しますが、空です。

私は何かが足りない、または私がやりたいことは不可能です。そうでない場合、これの「ベストプラクティス」は何ですか?

===編集===

ここでの 1 つの提案は、インターフェイス コントラクトをテストすることのみを目的とするクラス (テスト アセンブリの内部) にインターフェイスを実装することです。

これを書くと：

静的コントラクト チェッカーは、すべてのアサーションを証明できます。

しかし、代わりにこれを書くと：

owner == null || count > 0事後条件が証明されていないと主張しています。

2 番目の形式がこの事後条件に違反していないことを証明できると思います。

私の証明に何か問題がありますか？

証明にアサーションをContract.Assertコードへの呼び出しとして追加し、これだけを追加すると事後条件を証明できるという結論に達しました。

しかし、同じアサーションを「より自然な」方法に変更すると、失敗します。

これら 2 つのアサーションは同等であると予想されますが、静的チェッカーはそれらを異なる方法で扱います。

(ちなみにVS10のベータ2を使っています)

このコントラクトを以下に記述すると、Visual Studio でエラーが表示されます。

Error 20 Malformed contract section in method '....get_Page'

問題はifブロック？

編集：

Lasse V. Karisen はコメントに投稿しました:

どうですか: Contract.Ensures(result == null || result >= 0);?

はい、Karisen、以前にこれを試してみましたが、コンパイルされました。しかし、疑問が残ります:ifコントラクトを使用するときに s を持つことはできないのでしょうか?

私が抱えている別の問題は無知です（主に上記の例が機能することを考慮して）、結果の使用も含まれます：

私のマシンには vs 2008 と vs 2010 がインストールされており、devlabs のコード コントラクト (バージョン 1.2.21023.14) もインストールされています。vs 2008 では正常に動作します。ただし、vs 2010 では「コード コントラクト」タブがありません。インストールする必要があるものはありますか？