Pex和代碼合同

Question

以下是來自Pex Documentation pexandcontracts.pdf http://research.microsoft.com/en-us/projects/pex/pexandcontracts.pdf的代碼示例。我意識到這不是pex的具體問題，而是它涉及代碼合同，但它是來自pex教程的代碼。在點Contract.Result（）的endsWith（後綴）（1）和點（2）：

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 
     } 
    } 
} 

靜態驗證提供了以下警告：

CodeContracts：確保未經證實！。

我的問題是，如何解決這個問題呢？根據pex探索，合同不可能被違反。 （...有沒有？）

Answer 1

當靜態檢查器無法驗證表達式時，最好的辦法是使用Contract.Assume。

如果您想要達到零靜態檢查警告，您將最終得到很多需要使用Contract.Assume的地方，除非您的程序很瑣碎，因爲大多數.Net庫尚未簽署合同所以我不會爲此擔心。大多數情況下，有明確的代碼和一套好的單元測試比零合同警告要好。也就是說，請保持打開狀態，以便在編碼時驗證警告是誤報。

Answer 2

我會認爲這是Contract.Ensures的一個糟糕用法，因爲擔保相當複雜，不太可能隨時供應給後來的Requires。我更傾向於提供非無效性和長度的保證（即不超過原始值字符串）。！EndsWith條件應該是測試的斷言，Pex可以用它來指導其探索。

Answer 3

是的，有可能違反合同。記住IndexOf和EndsWith默認情況下使用文化特定的比較，有時可能會有令人驚訝的行爲。如果我寫

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

然後IndexOf不匹配的第一次出現，是因爲它認爲中間人物是一個單一'á'，所以index是2並且該方法返回"\u0301a"，這顯然與後綴結尾。

如果您想要證明正確的算法，請使用StringComparison.Ordinal。

但是Code Codes靜態檢查器當前不支持字符串值的分析，並且不瞭解IndexOf和Substring之間的這種關係。