- 商品参数
-
- 作者:
弗莱明·尼尔森(Flemming著|
无编|
詹博华,冀振燕,孙文辉译
- 出版社:机械工业出版社
- 出版时间:2022-06
- 页数:无
- 开本:16开
- ISBN:9787111706885
- 版权提供:机械工业出版社
-----
该书共分为6章,其中第1章为介绍,第2~5章依次为数据流分析、基于约束的分析、抽象解释、类型和作用系统,第6章为分析算法介绍。该书内容基本囊括了程序分析领域中的经典方法和技术,配以严谨的形式化系统,全书思路清晰、逻辑性强,是不可多得的经典书籍。
-----
前言 第1章概述1 11什么是程序分析1 12设置场景2 13数据流分析3 131等式方法3 132基于约束的方法5 14基于约束的分析6 15抽象解释8 16类型和作用系统11 161注释类型系统12 162作用系统14 17算法16 18程序转换17 结束语18 迷你项目18 练习20 第2章数据流分析22 21过程内数据流分析22 211可用表达式分析24 212到达定值分析26 213很忙的表达式分析29 214活跃变量分析31 215派生数据流信息33 22理论性质34 221结构操作语义34 222活跃变量分析的正确性38 23单调框架41 231基本定义43 232案例回顾44 233一个不可分配的例子46 24等式系统的求解47 241MFP解47 242MOP解50 25过程间分析53 251结构操作语义55 252过程内分析与过程间分析56 253显式使用上下文58 254调用字符串作为上下文61 255假设集作为上下文63 256流敏感与流不敏感64 26形状分析66 261结构操作语义67 262形状图70 263分析的描述73 结束语82 迷你项目84 练习86 第3章基于约束的分析90 31抽象0CFA分析90 311分析的描述91 312分析的明确定义96 32理论性质97 321结构操作语义98 322语义正确性101 323解的存在性104 324余归纳和归纳的比较106 33语法引导的0CFA分析108 331语法引导的规范108 332解的保持110 34基于约束的0CFA分析111 341解的保持113 342约束的求解113 35添加数据流分析117 351抽象值为幂集117 352抽象值为完全格119 36添加上下文信息122 361均匀kCFA分析123 362笛卡儿积算法127 结束语128 迷你项目130 练习132 第4章抽象解释135 41一种普通的正确性定义135 411正确性关系136 412表示函数138 413一个较小的扩展139 42不动点的近似141 421加宽算子143 422变窄算子146 43Galois连接149 431Galois连接的性质152 432Galois插入155 44Galois连接的系统的设计方法157 441组件上的组合159 442其他组合方式162 45衍生的操作165 451沿着抽象化函数衍生165 452数据流分析中的应用168 453沿着具体化函数衍生171 结束语174 迷你项目176 练习177 第5章类型和作用系统182 51控制流分析182 511底层类型系统183 512基于类型的分析184 52理论性质187 521自然语义187 522语义正确性189 523解的存在性191 53类型推导算法193 531一个底层类型系统的算法193 532一个控制流分析的算法196 533语法可靠性和完备性200 534解的存在性204 54作用205 541副作用分析206 542异常分析210 543区域推导213 55行为219 551通信分析219 结束语225 迷你项目228 练习231 第6章算法234 61工作列表算法234 611工作列表算法的结构235 612LIFO和FIFO迭代238 62逆后序迭代239 621循环算法242 63在强分量里迭代243 结束语245 迷你项目247 练习248 附录A偏序集合250 附录B归纳和余归纳258 附录C图和正则表达式265 参考文献272 符号索引283 术语索引287
1