这篇paper的完整题目是 Dynamically Discovering Likely Program Invariants to Support Program Evolution
注：本文标题中的序号表示这段内容出现在paper中的某个section（比如 “2、例子” 对应 paper 中的 section 2 ）
Daicon的出现背景
- 在software evolution过程中，invariants防止重要的assumptions被更改
- 但是，explicit invariants太缺乏了，所以程序员很容易引入bug
- 一个解决方法就是动态的、自动化的推断invariant
Daicon的原理
- 使用一组输入值，执行（instrumented）程序
- 从执行的程序中截取variable trace（存入data trace database）
- 从variable trace中推断invariants
Daicon与test data的关系
- Daicon算法的精度取决于test case的质量与完整度
- 额外的test case可能会提高invariant的精度
如何用program trace获得invariant？
- 如何发现invariant？
- 运行速度？
- 如何选择test case?
- 如何减少（对程序员来说）无用的invariant？
2、例子：使用规范良好的程序展示Daicon的功能
- 规范良好：展示且服从preconditions, postconditions, loop invariants
- Daicon可以找到所有的目标invariants，外加
- 原程序未明确定义的invariant
- 可以发现原定义的不足
- 受限于test case的invariant
- size(Array) < 30
- 正确却无聊的invariant（trivial解）
- 原程序未明确定义的invariant
- 填补了static分析的不足
- static会因为信息不足导致结论不完整
- static无法良好的分析pointer指向的heap
3、推断invariants
- 需解决的两大问题：
- 推断哪些invariant？
- 怎样推断？
- Daicon的三个推断点：entry, exit, (optional) loop head
- 每次执行到推断点的时候，instrumented program都会把变量的值给Daicon
- Daicon检查所有可能的invatiant：x = const, a > b, y = f(x), etc.
- 只要invariant被违反一次，那么这个invariant在之后的程序都不会再检查了（别的invariant会继续检查）
- 检查的invariant越多，Daicon运行的越慢
- 只支持有限的数据结构
- scalar number (num + character + boolean)
- sequence of scalars (array)
3.1 Invariant Confidence
- 如果输入集太少，那么输出的invatiant就会又多又无用
- 理想状况是有“完整”的输入集
- Daicon选择计算Invariant Confidence
- 使用统计推断
- test if noncoincidental，之后report
- 有些invatiant可能只出现在loop，不出现在entry和exit，因为执行的次数不够多
3.2 Derived Variables
- 显式的variable可能不够，所以Daicon自行推导一些variable
- array长度，内部元素范围
- 某variable的极值
- func被call的次数
- 没写怎么生成的
7、Test suites for Daikon
- 随机 test-case generation
- 很好的展示invalid inputs
- hand-crafted test cases
- 其实就是人工合成
8、程序instrumentation
8.1 获取variable值的过程
- 先对程序进行instrumentation
- 在每一个推断点记录所有variable的值
- 对于C语言，同时记录pointer的地址值和引用值
- 讲这些值存入data trace file
8.2 instrumentation的过程
- 解析(parse)程序到一个abstract syntax tree
- 分析所有variable的scope
- 添加代码
- 保存variable的值到指定地点
- 重新compile程序
缺点
- 不支持object-oriented programming
改进
- 测试用例：regression testing
- test suite augmentation
