Pex和Code合同

Question

下面是Pex Documentation 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
        }
    }
}

静态验证器提供以下警告：

后缀:确保点(1)和点(2)处的后缀：！Contract.Result().EndsWith(后缀)。

我的问题是，如何解决这个问题？根据pex调查，不存在违反合同的可能性。(...有吗？)

Answer 1

我认为这是对Contract.Ensures的一种糟糕的使用，因为保证相当复杂，不太可能随时提供给以后的需求。我更倾向于提供非空性和长度的保证(即不超过原始值字符串)。相反，!EndsWith条件应该是测试的断言，Pex可以使用它来指导它的探索。

Answer 2

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

如果你试图得到零静态检查器警告，你会在很多地方使用Contract.Assume，除非你的程序是琐碎的，因为大多数.Net库还没有契约，所以我不会担心这个问题。大多数情况下，拥有清晰的代码和一组良好的单元测试总比没有协定警告要好。也就是说，让弯曲图保持开启状态，这样你就可以在编码时验证警告是否为假阳性。

Answer 3

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

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

则IndexOf不匹配第一次出现的内容，因为它将中间字符视为单个'á'，因此index为2，方法返回"\u0301a"，该后缀显然以后缀结尾。

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

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