提问人：user1935724 提问时间：4/21/2019 更新时间：4/23/2019 访问量：145
使用 Microsoft 代码协定检查不变性
checking invariant using Microsoft code contracts
问：
刚刚接触到了 Microsoft Code 合约，用于检查代码 （https://learn.microsoft.com/en-us/dotnet/framework/debug-trace-profile/code-contracts） 中的前置、后置条件和对象不变量，并想尝试一下。我想确认一个关于健全性和完整性的问题，假设检查器不输出任何错误消息，假设不变量不输出任何错误消息，这是否意味着不变量确实是（可证明的）真，或者它仍然可能是误报。
答：
0赞
Jeffrey L Whitledge
4/23/2019
#1
静态检查器可以通过各种方式被愚弄，例如添加错误的假设。在这个答案中，我将假设没有做过类似的事情。
此外，检查器中可能存在错误。但假设没有......
静态检查器旨在不产生误报。所有前置和后置条件以及不变量都将被检查，只有当条件的真实性可以得到肯定验证时，它们才会通过。如果无法验证条件，则将提供错误消息。
系统不会尝试证明可以违反不变量。“未经证实”的错误消息意味着没有找到正确性的证据。不变量可能仍然是正确的，只是未经证实。
因此，没有误报（同样，根据设计，假设没有错误或破坏）。
评论