<VCC笔记> Assumption
2015-12-05 10:27
204 查看
接下来是第二种注释语句类型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
例:
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
相关文章推荐
- RecyclerView介绍(一)----简单概述
- 融合通信(中移动)----微信的强力竞争者来了----阿冬专栏!!!
- php实现微信发红包
- 求子数组的最大和
- 安装Hadoop系列 — eclipse plugin插件编译安装配置
- Shell脚本
- 【SSH项目实战】国税协同平台-33.quartz&SimpleTrigge
- svn使用常见问题
- iOS应用开发中SQLite的初步配置指南
- 斐波那契数列数组递推,普通递归,记忆化搜索,矩阵快速幂,和公式法
- 10.缺陷跟踪系统Mantis介绍及安装
- C语言问题总结
- Linux的常用命令1---网络相关(不断添加中)
- javaweb学习总结(四)——Http协议
- 无优先级运算问题
- python mmap使用记录
- CCBPM高级开发之类设计与数据库设计命名规则
- 最佳调度问题
- 如何在高并发分布式系统中生成全局唯一Id
- 在HTML中用Javascript接收参数