DscvSpec

这篇paper的完整题目是 Discovering Likely Method Specifications

下载链接

Motivation

• static
  • 之前的工具生成的 pre/postconditions 过于细节，用户难以使用
  • 对于 loop 中的 invariants，之前的工具只能把 specifications 表示为 fields of classes
  • 只能分析“simple patterns”
  • 生成的 specification 结果过于抽象
• dynamic
  • Daicon 的能力受限于 input
  • Daicon 不太适合推断 conditional invariant？

背景

• 软件的 specifications 在（正式的）测试中很重要
  • 在自动化检查中，specifications 可以生成测试、检查运行结果
• 但是 specifications 总是缺失
  • 所以我们需要从现有的代码中寻找可能的 specifications
• 推断的 specifications 的质量取决于 code 本身的质量

Intro

• 以往的研究包括静态分析和动态分析
  • 前者接近白盒测试，后者接近黑盒测试
• 本文联合这两种分析模式，先静再动
  • 静分析，动归纳整理
• 本文主要分析包含 abstract data types (ADTs) 的 class
  • 程序员需要把 method 分为两类：只读(observer) 和 可写(modifier)
  • 本方法试图用 observer methods 来抽象的描述 modifier method
• 自动化的生成适合用户使用的 pre/postconditions
  • 可以直接 feed 给已有的单元测试工具使用

Steps

• 1、选择一个 method，用随机的初始参数进行符号执行
  • 试图遍历所有路径，但是只对 loop 进行有限的探索
• 2、分析 observer methods 获得 PC 的 observational abstraction？
  • 这一步获取很多的 path-specific axioms
    • 描述 observer method 在各种条件下的行为
• 3、把这些 axioms 进行合并、简化、筛选

2、例程

public class Set {
	int[] repr;
	public Set(int maxSize) { 
		repr = new int[maxSize]; 
	}
	
	public void Add(int x) {		// modifier method
		if (x == 0) 
			throw new ArgumentException();
		int free = -1;
		for (int i = 0; i < repr.Length; i++)
			if (repr[i] == 0) 
				free = i;
			else if (repr[i] == x)
				throw new InvalidOperationException();
		if (free != -1) 
			repr[free] = x;
		else
			throw new InvalidOperationException();
	}
	
	public bool IsFull() {			// observer method
		for (int i = 0; i < repr.Length; i++)
			if (repr[i] == 0) return false;
		return true;
	}
	public bool Contains(int x) {	// observer method
		if (x == 0) throw new ArgumentException();
		for (int i = 0; i < repr.Length; i++)
			if (repr[i] == x) 
				return true;
		return false;
	}
}

• 合理的 pre/postconditions

void Add(int x)
	requires x!=0
		otherwise ArgumentException;
	requires !Contains(x) && !IsFull()
		otherwise InvalidOperationException;
	ensures Contains(x);

• 这种写法需要上下文联系，一个更好的写法是上下文独立，称为 axioms

• x==0 
	⇒ future( ArgumentException )
• x!=0 ∧ ( Contains(x) ∨ IsFull() )
	⇒ future( InvalidOperationException )
• x!=0 ∧ ¬ Contains(x) ∧ ¬ IsFull()
	⇒ future( Contains(x) )

2.1 符号化遍历

• 下图表示符号化遍历的过程

• 图中的符号me表示 implicit instance argument，可以理解为Java中的this
• 如果me在上一次执行的时候有效，那么下一次一定有效
• 图中 S2, S8, S15, S16, S23, S24 表示 ArgumentException 或者 InvalidOperationException，S4, S6 表示 null dereference，S14 表示Add正常结束

2.2 从路径中推断 specifications

• 从每个路径中，我们能获得2个结果
  • heap 的状态
  • method 的返回值
• 从上面的结果中可以推断 specifications，但是会有一些问题
  • 内容会非常多细节，比如repr的状态
  • 有 loop 的存在，无法完全覆盖所有分支
• 我们使用 observational abstraction 来把上面获得的信息转化为 specification
  • 获得 ADT 层面的观测？
• 举例
  • S4 和 S6 错误源于 null dereference。但是，C#能在编译层面排除这种调用，所以我们忽略 S4 和 S6
  • S2 不需要 abstraction，所以直接获得一条 specification requires x!=0 otherwise ArgumentException;
  • S15, S23, S24 的终止源于相同的 exception：x和reprarray 中的某个值相同，于是我们发现（？）Contains(me, x)肯定返回true，于是获得requires !Contains(x) otherwise InvalidOperationException;
  • S8 可以让我们发现 bug 和IsFull相关
  • S14 与x, IsFull, Contains 相关
  • 合并以上信息，我们能够得到前文给出的 specifications

3、方法

3.1 探索 modifier method

• 有 loop 和 recursion 存在的时候，路径可能是无限的，所以我们只进行有限次数的 unroll loops and unfold recursion ？？？

3.2 Observational Abstraction

• 我们上文中的 observation 包括了对Contains的调用，但是忽略了一个隐含的参数：heap
  • 所以，我们把这个 method 写为 Contains(h, me, x)
• 看不懂相关定义：Observer equations are equations over observer terms.

3.3 总结 axioms

• 看不懂

4、Observational Abstraction

• argument 分类
  • 在 argument selection 时，简单粗暴的方法是，为每一个 argument 创建一个符号
  • 但是Hashtable.Add(Key, Value)应该和Hashtable.ContainsKey(Key)里面的 argument 应该属于同一个类别
  • 但是，ContainsKey(Value)是无意义的
  • 分类的依据是，“methods 之间是否有 information flow”
• 实现方式：没看懂

不足

• It is desirable to choose a minimal and complete set of observer methods
  • but, it is well known that the problem to determine a minimal basis for an axiomatic specification [12] is undecidable
• 只考虑单线程，没有 concurrency

• Previous
  单元测试+JUnit
• Next
  JPF安装