抽象解释

这是对于Cousot夫妇的奠基性论文的试译.

第1章 引论

一个程序指称着某个对象宇宙之中的计算. 程序的抽象解释在于使用这个指称来描述另外一个抽象对象宇宙之中的计算, 以至于抽象执行的结果可以给出实际计算的一些信息. 一个直觉性的例子是符号规则 (rule of signs). 文本$-1515⁎17$或许可以理解为指称着抽象宇宙$\{(+),(-),(\pm )\}$上的计算, 其中算术运算符的语义由符号规则定义. 抽象执行$-1515⁎17\Rightarrow -(+)⁎(+)\Rightarrow (-)⁎(+)\Rightarrow (-)$证明了$-1515⁎17$是一个负数. 抽象解释关心通常的计算宇宙的特定潜在结构 , 在我们的这个例子里是符号. 其给出了对于一个程序的实际执行的某些侧面的总结. 一般而言, 这个总结可以简单获得但是并不精确, 例如$-1515+17\Rightarrow -(+)+(+)\Rightarrow (-)+(+)\Rightarrow (\pm )$. 尽管结果从基础而言并不完备, 抽象解释允许程序员或者编译器回答一些问题, 这些问题不需要对于程序执行的完全了解或者可以容忍不精确的回答, 例如

第2章 总结

第3节描述了一个简单流程图语言的句法和数学语义. 这个数学语义在第4节被用来构建一个更为抽象的程序语义模型, 在于其忽略了控制流的顺序 (sequencing). 这个模型可以认为是程序的各种抽象解释之中最为具体的. 第5节给出了程序的抽象解释的形式定义.

抽象程序性质由完备半格所建模. 基本的程序构造由保序函数所局部解释, 这种函数用以将递归方程组和程序联系起来.

第3章 程序的句法和语义

我们将会使用有限流程图作为独立于语言的程序表示.

第3.1节 程序的句法

第3.2节 程序的语义

第4章 程序的静态语义

第5章 程序的抽象解释

第6章 一致的抽象解释

第7章 抽象解释的格

第8章 程序的抽象求值