c# - 为什么这个基于字符串的 Contract.Ensure 调用未经证实？

Question

我的 .Net 4 应用程序中有以下代码:

static void Main(string[] args) {
    Func();
}

static string S = "1";

static void Func() {
    Contract.Ensures(S != Contract.OldValue(S));
    S = S + "1";
}

这在编译时给了我一个确保未经证实的警告:

warning : CodeContracts: ensures unproven: S != Contract.OldValue(S)

这是怎么回事？如果 S 是整数，这就可以正常工作。如果我将 Ensure 更改为 S == Contract.OldValue(S + "1")，它也会起作用，但这不是我想要做的。

Answer 1

我猜契约(Contract)引擎不够聪明，无法理解这是有保证的。如果你说:

S = S + "";

...那么契约(Contract)就不起作用了。因此引擎必须执行一些额外的逻辑来确定 S = S + "1" 将始终更改字符串的值。该团队根本没有时间添加该逻辑。