程序分析原理

前言
第1章概述1
11什么是程序分析1
12设置场景2
13数据流分析3
131等式方法3
132基于约束的方法5
14基于约束的分析6
15抽象解释8
16类型和作用系统11
161注释类型系统12
162作用系统14
17算法16
18程序转换17
结束语18
迷你项目18
练习20
第2章数据流分析22
21过程内数据流分析22
211可用表达式分析24
212到达定值分析26
213很忙的表达式分析29
214活跃变量分析31
215派生数据流信息33
22理论性质34
221结构操作语义34
222活跃变量分析的正确性38
23单调框架41
231基本定义43
232案例回顾44
233一个不可分配的例子46
24等式系统的求解47
241MFP解47
242MOP解50
25过程间分析53
251结构操作语义55
252过程内分析与过程间分析56
253显式使用上下文58
254调用字符串作为上下文61
255假设集作为上下文63
256流敏感与流不敏感64
26形状分析66
261结构操作语义67
262形状图70
263分析的描述73
结束语82
迷你项目84
练习86
第3章基于约束的分析90
31抽象0CFA分析90
311分析的描述91
312分析的明确定义96
32理论性质97
321结构操作语义98
322语义正确性101
323解的存在性104
324余归纳和归纳的比较106
33语法引导的0CFA分析108
331语法引导的规范108
332解的保持110
34基于约束的0CFA分析111
341解的保持113
342约束的求解113
35添加数据流分析117
351抽象值为幂集117
352抽象值为完全格119
36添加上下文信息122
361均匀kCFA分析123
362笛卡儿积算法127
结束语128
迷你项目130
练习132
第4章抽象解释135
41一种普通的正确性定义135
411正确性关系136
412表示函数138
413一个较小的扩展139
42不动点的近似141
421加宽算子143
422变窄算子146
43Galois连接149
431Galois连接的性质152
432Galois插入155
44Galois连接的系统的设计方法157
441组件上的组合159
442其他组合方式162
45衍生的操作165
451沿着抽象化函数衍生165
452数据流分析中的应用168
453沿着具体化函数衍生171
结束语174
迷你项目176
练习177
第5章类型和作用系统182
51控制流分析182
511底层类型系统183
512基于类型的分析184
52理论性质187
521自然语义187
522语义正确性189
523解的存在性191
53类型推导算法193
531一个底层类型系统的算法193
532一个控制流分析的算法196
533语法可靠性和完备性200
534解的存在性204
54作用205
541副作用分析206
542异常分析210
543区域推导213
55行为219
551通信分析219
结束语225
迷你项目228
练习231
第6章算法234
61工作列表算法234
611工作列表算法的结构235
612LIFO和FIFO迭代238
62逆后序迭代239
621循环算法242
63在强分量里迭代243
结束语245
迷你项目247
练习248
附录A偏序集合250
附录B归纳和余归纳258
附录C图和正则表达式265
参考文献272
符号索引283
术语索引287