ペックスとコード契約

Question

以下は、Pexドキュメントpexandcontracts.pdf http://research.microsoft.com/en-us/projects/pex/pexandcontracts.pdfのコードサンプルです。私はこれが厄介な特定の質問ではなく、むしろコード契約に関連していることを認識していますが、それはpexチュートリアルのコードです。

CodeContracts：

namespace CodeDigging 
{ 
    public class StringExtension 
    { 
     public static string TrimAfter(string value, string suffix) 
     { 
      // <pex> 
      Contract.Requires(!string.IsNullOrEmpty(suffix)); 
      // </pex> 
      Contract.Requires(value != null); 
      Contract.Ensures(!Contract.Result<string>().EndsWith(suffix)); 

      int index = value.IndexOf(suffix); 
      if (index < 0) 
       return value;     // (1) First possible contract violation 
      return value.Substring(0, index); // (2) second possible contract violation 
     } 
    } 
} 

静的検証者は、次の警告を提供しています証明されていない保証：Contract.Result（）EndsWith（サフィックス）の時点で（1）と点（2）。

私の質問は、これを解決するにはどうすればいいですか？ペックスの調査によれば、契約違反の可能性はない。 （...ありますか？）

Answer 1

スタティックチェッカーで式を確認できない場合は、Contract.Assumeを使用することをお勧めします。

ほとんどの.Netライブラリにまだ契約がないため、あなたのプログラムが些細なことがない限り、静的チェッカーの警告がゼロになるようにしようとすると、Contract.Assumeを使用する必要があります。私はそれについて心配しないでしょう。ほとんどの場合、明確なコードと単体テストの良いセットは、ゼロの契約警告を持つよりも優れています。それは、あなたがコーディングしているときに警告が偽陽性であることを確認できるように、くすんだままにしておきます。

Answer 2

私はこれがContract.Ensuresの貧弱な使用であると主張します。これは保証がかなり複雑で、後でRequiresに簡単に供給されないためです。無限長と長さの保証（つまり、元の値の文字列よりも長くない）を保証する傾向があります。！EndsWith条件は、Pexがその探索の指針として使用できるテストの主張でなければなりません。

Answer 3

はい、契約違反の可能性があります。既定では文化固有の比較を使用することを覚えておいてください。これは時々驚くべき動作をすることがあります。私は

TrimAfter("\u0301a\u0301a", "\u0301a") 

を記述する場合、それは単一'á'する中央の文字を考慮するためIndexOfは、最初の出現と一致していないので、indexは2で、この方法は明らかに接尾辞で終了する、"\u0301a"を返します。

確かに正しいアルゴリズムが必要な場合はStringComparison.Ordinalを使用してください。

ただし、コード契約の静的チェッカーは現在のところ文字列値の解析をサポートしておらず、IndexOfとSubstringの間のこの関係を理解し​​ていません。