最近在学校跟着老师参与了一个代码验证的工作，需要使用Microsoft Research（微软学术）开发的VCC工具，是开源的，托管在Codeplex上。这东西英语资料极其少，中文资料基本没有。我只能看官方给的英文文档。因此，我也就有了心思写几篇简单的博客，也包括文档的一些翻译。留个纪念也好。
VCC主页（https://vcc.codeplex.com/）
翻译了一下VCC教程上的简介：
它涵盖了注释语言、验证方法和使用VCC本身。
本教程介绍如何使用VCC验证C代码。我们的主要受众是的想编写正确的代码的C程序员。唯一的要求是拥有C语言的工作知识。使用VCC，你首先要注释你的代码，指明他做什么(如：为你的输入进行排序)，以及为什么它能这样做(如：与你的循环和数据结构相适应的不变量）。然后VCC会试图(以数学的方式)证明程序符合你之前订下的规范。与大多数程序分析器不同，VCC不会寻找bug，或者分析程序的抽象；如果VCC证明程序是正确的，那么您的程序是就是正确的。
为了检查程序，VCC使用演绎验证模式。它生成一定数量的数学表达式(称为验证条件)，保证程序的正确性的“有效性表达式(?)”，并试图使用一个自动定理验证器来证明这些语句。如果这些证明失败，VCC会将失败的原因反映到你的程序代码身上（而不是让你看到定理验证器用的那些公式）。因此，你通常是在代码和程序状态层面与VCC交互的。通常情况下，你可以忽略在VCC内部的数学推理。例如，如果您的程序使用了除法，如果VCC无法证明除数一定非零，它会报告你的程序有(潜在的)错误。这并不意味着你的程序必然是不正确的。事实上，大多数情况下它都没有问题。（VCC会报错）那是因为你还没有提供足够的信息来让VCC推断出这个疑似错误一定不会发生。但即使它没有，你至少也能会证明你的代码不受这种错误影响，同时你也会产生精确的规格注释——一种非常有用的文档。
本教程中的示例和VCC源码在一起。
VCC可以从VCC主页（http://vcc.codeplex.com/）下载，一定要阅读安装说明，里面提供了关于安装条件和设置工具路径的方法等重要信息。”
安装
安装VCC之前请先在机器上准备好以下的环境：
- .Net v4.0 or later - Download installer.
- F# 2.0 Redistributable - Download installer.
- Microsoft Visual C++ 2010 Redistributable Package - Download installer.
- Visual Studio 2010 以上(any edition with C++ support). 注意，Express速成版是不推荐的，它不支持在IDE上使用VCC。 我是在Windows10+VS2010上使用的，成功装上了插件。
准备好以上的环境之后，你就可以前往VCC主页（http://vcc.codeplex.com/）下载最新的安装程序进行安装了。