1

以下是 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 的探索，合同没有被违反的可能性。（... 在那儿？）

4

3 回答 3

3

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

于 2011-12-07T19:34:49.363 回答
2

您最好的选择是Contract.Assume在静态检查器无法验证表达式时使用。

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

于 2011-12-07T19:21:32.147 回答
0

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

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

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

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

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

于 2015-09-26T19:42:34.530 回答