c# - 代码契约(Contract)似乎不适用于 VS2012

Question

我正在阅读 Code Contracts，乍一看它似乎非常具有革命性，但我似乎无法让它们工作。我正在运行 Windows 8 和 Visual Studio 2012 Premium(两者的发行版)。然后我从 here 安装了代码契约(Contract)单击“下载代码契约(Contract)”链接。

然后我在一个全新的控制台应用程序中编写了以下代码:

class Program
{
   static void Main(string[] args)
   {
      var answer = Add(0, 5);
      Console.Write(answer);

      Console.ReadLine();
   }

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

      return x + y;
   }
}

我预计编译会失败，因为 Add 的第一个参数是 0，但程序成功并在控制台打印 5。

我已经尝试使用默认的代码契约设置，也尝试了一些东西但无济于事。我当前的设置如下所示:

知道我做错了什么吗？

更新:

这是“构建”窗口的结果。看起来它正在做某事，但只是发出警告而不是错误。在我观看的视频中，这些东西被标记为编译错误，程序甚至无法运行。

1>------ Build started: Project: DeleteMe, Configuration: Debug Any CPU ------
1>  DeleteMe -> c:\users\mike\documents\visual studio 2012\Projects\DeleteMe\DeleteMe\bin\Debug\DeleteMe.exe
1>  CodeContracts: Task manager is unavailable.
1>  CodeContracts: DeleteMe: Run static contract analysis.
1>  CodeContracts: Suggested requires: Contract.Requires(false);
1>  CodeContracts: DeleteMe: Validated:  0.0 %
1>  CodeContracts: DeleteMe: Contract density: 0.87
1>  CodeContracts: DeleteMe: Total methods analyzed 4
1>  CodeContracts: DeleteMe: Methods with 0 warnings 3
1>  CodeContracts: DeleteMe: Total time 4.974sec. 1243ms/method
1>  CodeContracts: DeleteMe: Methods with necessary preconditions: 1
1>  CodeContracts: DeleteMe: Discovered 1 new candidate preconditions in 00:00:00.1718843
1>  CodeContracts: DeleteMe: Retained 1 preconditions after filtering
1>  CodeContracts: DeleteMe: Inferred 0 object invariants
1>  CodeContracts: DeleteMe: Retained 0 object invariants after filtering
1>  CodeContracts: DeleteMe: Detected 0 code fixes
1>  CodeContracts: DeleteMe: Proof obligations with a code fix: 0
1>c:\Users\Mike\Documents\Visual Studio 2012\Projects\DeleteMe\DeleteMe\Program.cs(14,10,14,33): warning : CodeContracts: requires is false: x > 0 && y > 0
1>c:\Users\Mike\Documents\Visual Studio 2012\Projects\DeleteMe\DeleteMe\Program.cs(22,10,22,44): warning : CodeContracts: location related to previous warning
1>  CodeContracts: Checked 1 assertion: 1 false
1>  CodeContracts: DeleteMe: 
1>  CodeContracts: DeleteMe: Static contract analysis done.
========== Build: 1 succeeded, 0 failed, 0 up-to-date, 0 skipped ==========

Answer 1

因此，这个问题似乎是代码契约的几个限制和陷阱的组合。希望这个答案能帮助像我这样刚起步的人。

首先，自 1.4.50327.0 版本以来，Code Contracts 确实支持 Visual Studio 2012(Express 以外的任何版本)，尽管您必须运行 devenv.exe/setup如果您的版本早于 1.4.50910.0。查看Release Notes获取更多信息。

我遇到的第一个问题是在“代码契约(Contract)”属性选项卡的“静态检查”部分中选中了“缓存结果”复选框。这个选项默认是开启的，也需要SQL Server CE来存储它的缓存数据，Windows 8、VS2012或者Code Contracts都没有安装。不幸的是，您的程序将继续正常编译，并且您必须手动挖掘生成输出才能看到错误:

CodeContracts: xxx: Unhandled Exception: System.IO.FileNotFoundException: Could not load file or assembly 'System.Data.SqlServerCe, Version=3.5.1.0, Culture=neutral, PublicKeyToken=89845dcd8080cc91' or one of its dependencies. The system cannot find the file specified.

取消选中“缓存结果”复选框将解决此问题，安装 SQL Server CE 也是如此。

第二个问题是违反代码契约(Contract)被视为 warnings, and not compile errors .即使您启用了“将警告视为错误”，您的程序仍将继续编译并成功运行。如果您有一个较大的项目，其中包含大量您忽略的警告，则可能很难注意到这些新的代码契约(Contract)警告。在demo video I saw ，这些警告也反射(reflect)在 Visual Studio IDE 中(调用代码有蓝色下划线)，但是我似乎没有在 Visual Studio 2012 中看到这种行为。

这个设计决定让我很不安。如果我在我的代码中定义了一个契约，那个函数必须接受一个大于 0 的整数，而我公然传入一个 0，这是一个错误。不是警告。我违反了那份契约(Contract)，简单明了。

总的来说，我认为 Code Contracts 非常强大，并且可能会改变我们测试软件的方式。 MS Research 确实做得很好。但是，我认为它还没有真正为主流做好准备。它需要一些调整才能开始工作，它不会无缝集成到 Visual Studio 构建过程中，而且速度也很慢。在较小的项目上，它按预期工作，但当我将它插入一个较大的项目时，分析所有代码花了整整十分钟。