为什么这个基于字符串的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

我猜合约引擎不够聪明，无法理解这是有保证的。如果你说：

S = S + "";

……那么合同就无效了。因此，引擎必须执行一些额外的逻辑来确定S = S + "1"始终会更改字符串的值。该团队根本没有抽出时间来添加该逻辑。