关于Assertion

这篇博客开始介绍VCC的用法，先用简单的例子介绍VCC的基本语法，固然面对更复杂的程序时，VCC也是将他简化而后分析的。

　　1.Assertion

#include <vcc.h>
int main() {
    int x,y,z;
    if (x <= y) z = x;
    else z = y;
    _(assert z <= x)
    return 0;
}

　　上面的代码使z成为x和y之中的最小值。其中被_(  )包围的注释就是VCC所须要的注释，并且C语言编译器会无视这些注释。由于include的<vcc.h>中定义了#define _(...) /∗nothing∗/

一个相似_(assert E)的注释就是一个Assertion，他要求VCC证实注释中的表达式E是成立（hold）。因此_(assert z <= x)要求当代码执行到这一行时，z应该小于等于x。须要注意的是，若是VCC验证经过了这一条Assertion，这表示VCC证实无论何时，无论执行多少次，这条Assertion都会成立。

     C语言自身也有相似的东西 assert(E)。微软的文档中这样介绍二者的区别。

It is instructive to compare_(assert E)with the macro assert(E) (defined in <assert.h>), which evaluates E at runtime and aborts execution if E doesn’t hold. First, assert(E) requires runtime overhead (at least in builds where the check is made), whereas_(assert E)doesnot.Second,assert(E)will catch failure of the assertion only when it actually fails in an execution, whereas _(assert E) is guaranteed to catch the failure if it is possible in any execution. Third, because _(assert E) is not actually executed, E can include unimplementable mathematical operations, such as quantification over infinite domains.

　　若是要在cmd命令行中用VCC验证这个函数，你能够把代码保存为minimum.c，在命令行中使用VCC大体以下，**表示代码文件目录。

C:\**> vcc.exe minimum.c

Verification of main succeeded.

 　　若是装了VCC的Visual Studio插件，用VS打开文件以后，空白处右击，在菜单中选择Verify minimum.c就能够验证这个文件，验证结果会在VS底部给出。若是在函数内点击也能够只验证这个函数。

 

　　2.VCC的原理部分

　　要理解VCC的工做原理，能够去了解每一步执行中VCC掌握了什么信息。在上面的例子中VCC一开始什么都不知道，而后知道了if的第一个条件x<=y, 而后是z==x, 因此VCC知道z<=x。在else分支中，相似的，VCC知道y<x, z==y, 因此VCC知道z<=x。if的每一个分支VCC都发现Assertion成立，最后他就会验证经过这个Assertion。

　　咱们说VCC知道什么，指的是VCC知道代码提供的信息，而且能够经过当前已知的信息能够直接推断出新的信息。在这种理想状态下，当你新增一个正确的Assertion，确定不会影响他后面的Assertion的正确性。可是，VCC只完成了对基本公式的继续推断，包括相等，不等，加减乘除等简单的运算，而没有完成对全部运算公式的自动推断，是有其局限性的。否则的话，他本身所有都能推断完，咱们的工做量就很小了。

　　因此，在现实状况中，有时候，即便VCC“知道”了足够的信息，也无法证实一条Assertion。当你新增一个正确的Assertion，有可能会影响他后面的Assertion的正确性。固然，这个几率是比较低的，并且每每是涉及非线性算法的代码会出问题。

　　因此，VCC验证顺序代码或者条件语句时通常不会丢失信息，可是VCC验证循环语句的时候，容易丢失信息。这里的丢失是指他没有继续推断出更多信息，提供注释有助于减小这种状况。若是VCC没有经过你认为确定能经过验证的代码，那就有多是VCC不知道或者忽视了你觉得它确定知道的东西。这时候一个Assertion也是一个提醒，VCC验证他的时候可能就会恍然大悟，这个条件也是要成立的啊！