<VCC笔记> 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

时间: 2024-10-14 14:54:20

<VCC笔记> Assumption的相关文章

&lt;VCC笔记&gt; 推断操作符,映射和量词

推断操作符 在VCC中,==>符号意味着逻辑推理结果,即离散数学中的蕴涵关系.P==>Q等价于((!P)||(Q)).是非常常用的操作符. 量词(quantifier) 关于量词,这里指的是全称量词(universal quantifier)和存在量词(existential quantifier). 在VCC中全称量词的描述方法是 \forall  T v;E ,意思是“对于任意的T类型的v,表达式E均为真. 例如: _(assert x > 1 && \forall

JUnit4学习笔记(二):参数化测试与假定(Assumption)

一.一个简单的测试 编写一个只有一种运算的计算器: 1 public class Calculator { 2 public static double divide(int dividend, int divisor) { 3 return dividend / divisor; 4 } 5 } 为这个方法编写测试: 1 public class CalculatorTest { 2 //允许误差 3 private static final double DELTA = 0.01; 4 5

张高兴的 Windows 10 IoT 开发笔记:BH1750FVI 光照度传感器

原文:张高兴的 Windows 10 IoT 开发笔记:BH1750FVI 光照度传感器 BH1750FVI 是一款 IIC 接口的数字型光强度传感器集成电路.下面介绍一下其在 Windows 10 IoT Core 环境下的用法. 项目运行在 Raspberry Pi 2/3 上,使用 C# 进行编码. 1. 准备 包含 BH1750FVI 的传感器,这里选择的是淘宝上最多的 GY-30:Raspberry Pi 2/3 一块,环境为 Windows 10 IoT Core:公母头杜邦线 4-

加州大学伯克利分校Stat2.3x Inference 统计推断学习笔记: Section 4 Dependent Samples

Stat2.3x Inference(统计推断)课程由加州大学伯克利分校(University of California, Berkeley)于2014年在edX平台讲授. PDF笔记下载(Academia.edu) Summary Dependent Variables (paired samples) SD of the difference is $$\sqrt{\sigma_x^2+\sigma_y^2-2\cdot r\cdot\sigma_x\cdot\sigma_y}$$ whe

Data Types in the Kernel &lt;LDD3 学习笔记&gt;

Data Types in the Kernel Use of Standard C Types /* * datasize.c -- print the size of common data items * This runs with any Linux kernel (not any Unix, because of <linux/types.h>) * * Copyright (C) 2001 Alessandro Rubini and Jonathan Corbet * Copyr

加州大学伯克利分校Stat2.2x Probability 概率初步学习笔记: Section 2 Random sampling with and without replacement

Stat2.2x Probability(概率)课程由加州大学伯克利分校(University of California, Berkeley)于2014年在edX平台讲授. PDF笔记下载(Academia.edu) Summary Independent $$P(A\cap B)=P(A)\cdot P(B)$$ Binomial Distribution $$C_{n}^{k}\cdot p^k\cdot(1-p)^{n-k}$$ R function: dbinom(k, n, p) U

加州大学伯克利分校Stat2.3x Inference 统计推断学习笔记: Section 5 Window to a Wider World

Stat2.3x Inference(统计推断)课程由加州大学伯克利分校(University of California, Berkeley)于2014年在edX平台讲授. PDF笔记下载(Academia.edu) Summary Chi-square test Random sample or not / Good or bad $$H_0: \text{Good model}$$ $$H_A: \text{Not good model}$$ Based on the expected p

《算法导论》学习笔记一:课程简介及算法分析

MIT的算法导论公开课,很多年前就看到了,一直没有坚持去看,最近找暑假实习,面试基本都是算法,只好抽时间去狂刷leetcode,也借着这个机会希望把这个视频看完,把算法的基本功打扎实,这个公开课讲得还是挺不错的. 之前学习其他东西的时候,记了很多笔记,最后都丢了,想再翻看的时候已经找不到,于是想到把学习笔记放到博客上,这样方便以后自己查询. 公开课视频地址:http://open.163.com/special/opencourse/algorithms.html 第一节:课程简介及算法分析 第

USB学习笔记连载(八):FX2替换到FX2LP需要注意事项

对于使用FX2的用户,可以升级到FX2LP,上述的应用笔记<AN4078-C>中就讲解了在升级中的注意事项.   必要的修改:   1.晶振的匹配电容需要更改,FX2LP是12pF,不过笔者最近做的最小系统板,用的晶振匹配电容是22pF,没问题,反而用12pF晶振不能稳定的工作.   2.reset引脚,确认是能够保持5mS(可以参考笔者之前的博客,连载六中有提及).   3.VCC上升沿时间至少200us.   4.AVCC和AGND的改变.    手册中也列举出了对于FX2和FX2LP的不