为什么这个基于字符串的 Contract.Ensure 调用未经验证？
我的 .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")，它也可以工作，但这不是我想要做的。
I have the following code in my .Net 4 app:
static void Main(string[] args) {
Func();
}
static string S = "1";
static void Func() {
Contract.Ensures(S != Contract.OldValue(S));
S = S + "1";
}
This givens me an ensures unproven warning at compile time:
warning : CodeContracts: ensures unproven: S != Contract.OldValue(S)
What is going on? This works fine if S is an integer. It also works if I change the Ensure to S == Contract.OldValue(S + "1"), but that's not what I want to do.
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（2）
我猜合约引擎不够聪明，无法理解这是有保证的。如果你说：
……那么合同就不起作用。因此，引擎必须执行一些额外的逻辑来确定
S = S + "1"始终会更改字符串的值。该团队根本没有抽出时间来添加该逻辑。I'm guessing the contracts engine just isn't smart enough to understand that this is guaranteed. If you had said:
... then the contract wouldn't work. So the engine would have to do some extra logic to determine that
S = S + "1"will always change the value of the string. The team simply hasn't gotten around to adding that logic.这表明代码契约不知道使用非空字符串常量的字符串连接总是会产生不同的字符串。
这并不是完全不合理，但您可能想向团队建议它，作为他们在未来版本中采用的内容。
That suggests that Code Contracts doesn't know that string concatenation using a non-empty string constant will always produce a different string.
That's not entirely unreasonable, but you might want to suggest it to the team as something they take on for future releases.