0

我正在关注 codecontracts 教程（https://docs.microsoft.com/en-us/dotnet/framework/debug-trace-profile/code-contracts#usage-guidelines），但我似乎无法让最简单的事情正常工作. 给定方法定义

public int Add(int x, int y)
{
   Contract.Requires(x > 0);
   Contract.Requires(y > 0);

   return x+y;
}

当我调用o.Add(0,0)该方法时，前置条件检查不会失败。当我处于调试模式时，Contract.Requires()会跳过这些语句。我在哪里做错了？

第二个问题可以Contract.Invariant()用来检查循环不变量吗？根据对象不变量的定义，Object invariants are conditions that should be true for each instance of a class whenever that object is visible to a client.这似乎与循环不变量有点不同，因为在每次循环迭代中，循环不变量可能不一定对客户端可见，因此它可能违反属性但未被检查。这种理解正确吗？

4

1 回答 1

0

在回答您的第一个问题时，请从此处下载并运行 Code Contracts .msi 文件。.msi 文件包括静态检查器和二进制重写器（用于运行时检查），它通过注入合同来修改程序，使它们作为程序执行的一部分进行检查。没有重写器，将不会检查合同。请注意，重写器仅适用于 Visual Studio 2013 和 2015。

在回答你的第二个问题时，你不能Contract.Invariant()用来检查循环不变量。我建议Contract.Assume()在循环内使用。

于 2019-05-14T20:56:37.170 回答