Pex 和代码合同答案

【问题标题】：Pex and Code ContractsPex 和代码合同
【发布时间】：2011-12-07 16:31:58
【问题描述】：

以下是来自 Pex 文档 pexandcontracts.pdf http://research.microsoft.com/en-us/projects/pex/pexandcontracts.pdf 的代码示例。我意识到这不是特定于 pex 的问题，而是与代码合同有关，但它是 pex 教程中的代码。

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：确保未经证实：!Contract.Result().EndsWith(suffix) 在点 (1) 和点 (2)。

我的问题是，如何解决这个问题？根据 pex 的探索，合同没有被违反的可能性。（……有吗？）

【问题讨论】：

标签： c# code-contracts pex

【解决方案1】：

我认为这是对 Contract.Ensures 的不良使用，因为保证相当复杂，不太可能轻易地用于以后的 Requires。我更倾向于提供非空值和长度的保证（即不超过原始值字符串。）!EndsWith 条件应该是测试的断言，Pex 可以使用它来指导其探索。

【讨论】：

我倾向于同意（这就是我提出问题的原因）。请提供示例实现，我会将您的答案标记为正确。尽管如此，还是感谢您的意见。

【解决方案2】：

当静态检查器无法验证表达式时，最好使用Contract.Assume。

如果您试图使静态检查器警告为零，除非您的程序是微不足道的，因为大多数 .Net 库还没有合同，所以我不会担心。大多数时候，拥有清晰的代码和一组良好的单元测试比零合约警告要好。就是说，请保留波浪线，以便在编码时验证警告是否为误报。

【讨论】：

【解决方案3】：

是的，有可能违反合同。请记住，IndexOf 和 EndsWith 默认使用特定于文化的比较，这有时可能会产生令人惊讶的行为。如果我写

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

那么IndexOf不匹配第一次出现，因为它认为中间的字符是单个'á'，所以index是2，方法返回"\u0301a"，显然是后缀结尾的.

如果您想要可证明正确的算法，请使用StringComparison.Ordinal。

但是，Code Contracts 静态检查器目前不支持对字符串值的分析，并且不理解 IndexOf 和 Substring 之间的这种关系。

【讨论】：