問題タブ [code-contracts]

Microsoft の CodeContracts をいじっていて、解決できない問題に遭遇しました。2 つのコンストラクターを持つクラスがあります。

この例は簡略化されています。2 番目のコンストラクターが > 0 であることを確認する方法がわかりませんf。これはコントラクトでも可能ですか?

Visual Studio 2010内からコードコントラクトが正常に機能ccrewrite.exeしていますが、コマンドラインからは何もできません。サンプルアプリは次のとおりです。

次に、コードをコンパイルして、ccrewrite.exeを実行します。

RewrittenDummy.exeその後、ファイルはありません。

たくさんのオプションを試しましたが、何も違いはありません。私が気づいたいくつかのこと：

• 存在しないファイルを指定すると死ぬので、間違いなくDummy.exeを読み込んでいます
• Dummy.exeには、Contractへの参照が確実に含まれています。引数なしで実行すると、適切に失敗します（ただし、書き直された場合に期待するように、エラーメッセージが入力されていません）。
• 事後条件と不変条件を使用しても違いはありません

警告と冗長性を上げてみましたが、まったく役に立ちません。何が間違っているのでしょうか。

（Code Contractsフォーラムでも質問されています。関連する回答はここに自分で追加します。）

私は Code Contracts で不変条件を実証しようとしています。文字列の並べ替えられたリストの例を挙げたいと思いました。配列を内部的に維持し、追加などのための予備スペースを備えています-List<T>基本的には と同じです。アイテムを追加する必要がある場合は、それを配列に挿入するなどします。3 つの不変条件があると考えました。

• カウントは適切である必要があります: 非負であり、最大でバッファ サイズと同じ大きさです。
• バッファの未使用部分はすべて null にする必要があります
• バッファの使用部分の各アイテムは、少なくともその前のアイテムと同じくらい「大きい」必要があります

今、私はこの方法でそれを実装しようとしました:

残念ながら、ccrewriteループを台無しにしています。

ユーザー ドキュメントによると、このメソッドは への一連の呼び出しである必要がありますContract.Invariant。本当にこのようなコードを書き直す必要がありますか?

それは機能しますが、やや醜いです。（以前の試みよりもはるかに優れています。念のため。）

私の期待は不合理ですか？私の不変条件は不合理ですか？

(コード コントラクト フォーラムでも質問されています。関連する回答があれば、ここに追加します。)

( MSDN フォーラムにも投稿されていますが、私が見る限り、トラフィックはそれほど多くありません。)

Assertとの例を提供しようとしていますAssume。これが私が持っているコードです:

(もちろん、既存の参照の代わりに null 参照を渡すことができるというビジネスRandomは、純粋に教育的なものです。)

firstRollチェッカーがそれを知っていて、secondRollそれぞれが範囲内[1, 6]にある場合、合計が範囲内にあると判断できると思っていました[2, 12]。

これは無茶な希望ですか？何が起こるかを正確に把握するのはトリッキーなビジネスだと思います...しかし、チェッカーが十分にスマートであることを望んでいました:)

これが現在サポートされていない場合、近い将来サポートされる可能性があるかどうかを知っている人はいますか?

編集:静的チェッカーの算術演算には非常に複雑なオプションがあることがわかりました。「高度な」テキスト ボックスを使用して、Visual Studio からそれらを試すことができますが、私が知る限り、それらが何をするかについての適切な説明はありません。

Visual Studio (2008) 内から静的検証の警告に気付いたとき、スタック オーバーフローで誰かの質問に答えようとしていじり回していました。

「 required unproven source != null」というメッセージが表示されます。これが事実ではないことは私には明らかです。もちろんこれはほんの一例です。一方で、いくつかのかなり気の利いたものがかなりうまく機能しているようです。

1.2.20518.12 リリース (5 月 18 日) を使用しています。コード コントラクトは非常に興味深いと思いますが、他にこのようなケースがあった人はいますか? 現在の実装は実際に使用できると思いますか、それとも現時点では純粋に学術的であると考えますか?

私はこれをコミュニティ wiki にしましたが、いくつかの意見を聞きたいです :)

私が話しているのは、.NET 4.0 になるコード コントラクトです。すべてを機能させるコードを挿入するために、彼らはどのバイナリ リライターを使用しており、それは公開されていますか? AOP に彼らのバイナリ リライタを使用できるようにしたいので、これが単なるコンパイラの問題ではないことを願っています。

例えばこちらの記事で紹介しています。

メリットは何ですか？

静的分析はクールに思えますが、同時に単体テストで null をパラメーターとして渡す機能を妨げます。（記事の例に従った場合）

単体テストのトピックについてですが、自動テストを既に実践している場合、現在の状況を考えると、コード契約の意味はありませんか?

アップデート

Code Contracts で遊んでみて、少しがっかりしました。たとえば、受け入れられた回答のコードに基づいて：

単体テストでは、null が渡されないこと、およびコントラクトがビジネス ロジックの場合に結果がゼロ以上であることを確認するテストを作成する必要があります。つまり、最初のコントラクトを削除しても、特にこの機能のテストを行っていない限り、テストが壊れることはありません。ただし、これは、Visual Studio のより優れた (究極など) エディションに組み込まれている静的分析を使用しないことに基づいています。

基本的に、それらはすべて従来の if ステートメントを記述する別の方法に要約されます。Code Contracts を使用して TDDを実際に使用した私の経験は、その理由とその方法を示しています。

.net 3.5 の .net コード コントラクトを試しています。コード カバレッジを計算するために PartCover を実行している単体テストがあります。

PartCover は、レポートに System.Diagnostics.Contracts を含め続けます。MyProject を含め、他のすべてを除外するために使用しているルールを次に示します。

助言がありますか？

コード コントラクトは、すべての LINQ ステートメントに対して「null 参照でメソッドを呼び出している可能性があります」という警告を表示し続け、それらを黙らせる方法が見つかりません。たとえば、次のメソッドでは、最初に null をチェックせずに「car」オブジェクトの「Make」および「Model」プロパティにアクセスしているため、このような警告が 2 つ生成されます。

私の特定のケースでは、 Cars コレクションに null エントリが含まれることは決してないことがわかっているので、次のように Assume をメソッドに追加して、静的チェッカーを無音にすることができると考えました。

おそらく、静的チェッカーが理解することを期待するには少し多すぎるためです。そこで、次の SuppressMessage 属性を使用して警告を抑制することにしました。

しかし、何らかの理由で、警告を抑制することができません。次の SuppressMessage 属性も試しましたが、どれも機能しませんでした。

ContractVerification 属性を使用して、メソッドのコントラクト検証を完全に無効にしようとさえしました。

しかし、それもうまくいきませんでした。そこで、LINQ ステートメントの "where" 句に明示的な null チェックを追加することにしました。

これにより、「where」句の警告は正常に取り除かれますが、「select」句の警告は解消されません。実際、両方の警告を実際に取り除く唯一の方法は、次のように LINQ ステートメントのすべての句に null チェックを追加することです。

明らかに、これはあまりきれいで効率的なコードではありません。実際には、すべての LINQ ステートメントにそのような冗長な null チェックを追加するつもりはありません。特に、列挙に null エントリが含まれていないことがわかっている場合はなおさらです。この問題の最善の解決策は、静的チェッカーが、コレクション内の各項目の非 null 値を保証する Contract.Assume ステートメントを理解することですが、それができない場合は、少なくともメソッドの SuppressMessage 属性を尊重します。 .

私は VS2008 ( http://msdn.microsoft.com/en-us/devlabs/dd491992.aspx ) でコード コントラクトを使用してきました。
それらは確かに優れており、メソッド内の if-then-throw チェックの確実な代替手段を提供します。

それにもかかわらず、null 非許容の参照型に対して私が強く感じているニーズを満たすことができることを望んでいました。
残念ながら、私が見る限り、そうではないようです。
これは私が理解したものです：

• このようなものは、実行時に問題を引き起こします。
  MyClass a = null;
a.ToString();

• より簡潔で合理化された方法であっても、チェックを明示的に記述する必要があります。

• VS Team System を使用しない限り、コード コントラクトを使用して実行時にチェックすることしかできず、コンパイル時にメリットはありません。
  何か問題が発生した場合でも、処理する必要があることを意味します。
  単純な例外の処理と大差ありません。

• VSTS の静的分析を使用しても、実行時に行われる分析ほど効果的ではありません。
  これは完全に理解できますが、この機能がランタイムでの使用を意図していることを示すもう 1 つの兆候です。

私が間違っている場合は修正してください。ただし、コード コントラクトが私の生活を楽にし、null 非許容の参照型のようにプログラムをより堅牢にする方法はありません。

誤解しないでほしいのですが、私はコード コントラクトが嫌いではありません。
それらは、フレームワーク全体に対する非常に優れた拡張機能です。
ただ、null 非許容の参照型を持たないことによって C# が残したギャップをこれで埋められない場合、現時点では何も埋められないのではないかと心配しています。
どう思いますか？