Assumption

接下来是第二种注释语句类型Assumption。语法_(Assume E), 这个表达式是让VCC在接下来的额推理中，无视表达式E, 直接承认表达式E。

例：

int x, y;

_(assume x != 0)

y = 100 / x;

在没有那条assumption以前，VCC确定不会经过验证，由于x可能为0。可是，加了Assumption以后，VCC就选择放弃治疗，将x!=0加入本身的资料库。可是你用assumption糊弄了VCC并无什么好处，由于当代码实际运行的时候，没有人会管那堆注释，当X刚好为0的时候，程序就要crash了。因此通常来讲，若是你但愿你的验证可靠的话，Assumption就只能是验证过程当中临时性的产物，最终仍是尽可能消除的。

听起来assumption不是个好东西，其实否则，他也是有很多做用的。

1.当你代码比较复杂，VCC难以验证的时候，你能够用assumption先跳过，assumption也是一个标记，往后再去验证他。

2.当你调试那些注释的时候，你能够用assumption缩小错误范围，帮助定位错误。

3.对于复杂的程序，VCC验证须要很长的时间，使用assumption可让VCC放弃治疗，快速经过那段代码，提升你编写调试注释的效率。

4.可使用assumption模拟程序运行环境。

甚至VCC本身验证程序的时候，也在背地里使用assumption。

int x;

_(assert x == 1)

_(assert x > 0)

好比在上面的例子中，第一个assertion会报错，可是第二个不会。由于VCC给第一个Assertion报错以后，为了继续找到更多的错误，他就写了一个_(assume x==1）。

例：

int x,y;

_(assert x > 5)

_(assert x > 3)

_(assert x < 2)

_(assert y < 3)

结果

_(assert x > 5) // fails

_(assert x > 3) // succeeds

_(assert x < 2) // fails

_(assert y < 3) // fails