第4章 抽象解释 内容概述 以一种独立于编程语言的方式，介绍抽象解释的 一些本质概念 将“程序分析对语言语义是正确的”这个概念公 式化 用“加宽和收缩技术”来获得最小不动点的较好 的近似，并使所需计算步数得到限制 用“伽罗瓦连接和伽罗瓦插入”来把代价较大的 属性空间用代价较小的属性空间来代替 伽罗瓦连接可以通过一种系统的方式来构造，可 用来从一种分析的规范导出另一种分析的规范第4章 抽象解释 • 内容概述 以一种独立于编程语言的方式，介绍抽象解释的 一些本质概念 – 将“程序分析对语言语义是正确的”这个概念公 式化 – 用“加宽和收缩技术”来获得最小不动点的较好 的近似，并使所需计算步数得到限制 – 用“伽罗瓦连接和伽罗瓦插入”来把代价较大的 属性空间用代价较小的属性空间来代替 – 伽罗瓦连接可以通过一种系统的方式来构造，可 用来从一种分析的规范导出另一种分析的规范