コード契約では、ループの検証が保証されていません

Question

スタティックチェッカーが何を証明できないかを知るために、.Net Code Contracts（VS2010 Ultimate .Net 4）を使い始めました。

私は、次の例にしようとしている： -

public int Mult(int num1, int num2) 
    { 
     Contract.Requires(num2 >= 0); 
     Contract.Ensures(Contract.Result<int>() == (num1 * num2)); 
     int result = 0; 
     for (int i = 0; i < num2; i++) 
     { 
      result = result + num1; 
     } 
     return result; 
    } 

すなわち、乗算機能の簡単な実装を、繰り返し加えることで。 ..

CodeContracts: ensures unproven: Contract.Result<int>() == (num1 * num2) 

私の機能は、実際に製品を正しく計算されていないか、または静的チェッカーは確認できない別の理由があります - は：

静的チェッカは事後条件が満たされていることを確認することはできません必要ですか？ループが存在すると難しいですか？

ループが存在するときに静的チェッカーが物事を確認することが困難な場合は、常に多くの警告を発するのは非常に面倒です。

最初にバグの原因となっている一般的に私の間違った仮定であるため、私は何が起こっていると思うかを推測するためにAssumesを入れるオプションが嫌いです！

静的チェッカーで何かを証明できない場合、どうすればそれを手伝うことができますか？ たとえば、関数を再帰関数として書き直すことができます。チェッカーは、それをより簡単に検証できるでしょうか？ （関数型プログラミングの主張者は、これが最初の場所に書かれているべきだと言っているかもしれない。静的チェッカーを簡単にするために他のどのような方法でコードを変更できますか？

感謝！:)

Answer 1

静的チェッカーは、これを証明することはできませんが、実行時のチェッカー意志ありません。

コンパイル時に静的チェッカーが適用されます。あなたの保証を証明できるようにするには、あなたのアルゴリズムとあなたがしていることを完全に分析できなければなりません。それはそれほど強力ではありません。

ランタイムチェッカーは、機能が終了し、適切なユニットテストで、保証の有効性を証明する必要があるたびに、保証を検証します。

Answer 2

言い換えれば、コード契約は数学者/論理学者ではありません。

あなたは

num1 + num1 + ... + num1  (num2 terms in total) 

が

num1 * num2 

は、あなたがそれに任意の数学の問題とコードの契約を養うことができませんでし等しいことを「証明」することを期待のようなコードの契約は、実際にあなたのコードについて理由をできればあなたのためにそれを解決するだろうか？

私は理論計算機科学の専門家ではない、と私は、次の請求については完全にわからないんだけど、私はこの質問は、（this blog article by Eric Lippertの下部にも参照）Halting Problemに沸くと思います。

こうして私は、Code Contractsが任意の数学的問題を証明できないと確信しています。私は、コード契約があなたのコードについての推論にどのくらいの距離をおいているのか正確にはわかりませんが、非常に基本的で具体的なものを確認するよりもそれほど進んでいないと思います。例えばブログ記事"Static Checking .NET Code Contracts" by Doug Finkeの2番目のスクリーンショットをご覧ください。