接下来是第二种注释语句类型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