中国科学技术大学：《程序分析与程序验证》课程教学资源（PPT课件讲稿）第4章 抽象解释（补充）

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

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

第4章 抽象解释 内容概述 用“伽罗瓦连接和伽罗瓦插入”来把代价较大的 属 性空间用代价较小的属性空间来代替 有时，属性完全格L上的计算代价太大，甚至不 可计算，因此需用较简单的完全格M来代替L 必须有一种用M来描述L的方法，并将采用M的 分析替代采用L的分析 伽罗瓦连接和伽罗瓦插入是用来表达程序的属性 空间L、属性空间M之间联系的一种工具

第4章 抽象解释 • 内容概述 用“伽罗瓦连接和伽罗瓦插入”来把代价较大的 属 性空间用代价较小的属性空间来代替 – 有时，属性完全格L上的计算代价太大，甚至不 可计算，因此需用较简单的完全格M来代替L – 必须有一种用M来描述L的方法，并将采用M的 分析替代采用L的分析 – 伽罗瓦连接和伽罗瓦插入是用来表达程序的属性 空间L、属性空间M之间联系的一种工具

第4章 抽象解释 抽象解释 在程序静态分析中，用于构造和逼近程序不动点 语义的理论 使用抽象对象域上的计算抽象来逼近程序指称的 具体对象域上的计算，使得程序抽象执行的结果 能够反映出程序真实运行的部分信息 本质上是在计算效率和计算精度之间取得均衡， 以损失计算精度来求得计算的可行性，再通过迭 代计算来增强计算精度

第4章 抽象解释 • 抽象解释 – 在程序静态分析中，用于构造和逼近程序不动点 语义的理论 – 使用抽象对象域上的计算抽象来逼近程序指称的 具体对象域上的计算，使得程序抽象执行的结果 能够反映出程序真实运行的部分信息 – 本质上是在计算效率和计算精度之间取得均衡， 以损失计算精度来求得计算的可行性，再通过迭 代计算来增强计算精度

第4章 抽象解释 4.1节 将“程序分析对语言的语义是正确的”这个 概念公式化 。 方式1：正确性关系 R:VxL→{true,.false -正确性标准：R在程序计算过程中保持 可接受的正确性关系 增加两个条件 1、属性值1越小（偏序）越精确 2、存在描述一个值y的最好属性值1

第4章 抽象解释 4.1 节 将“程序分析对语言的语义是正确的”这个 概念公式化 • 方式1：正确性关系 – R : V  L → {true, false} – 正确性标准：R在程序计算过程中保持 – 可接受的正确性关系 增加两个条件 1、属性值 l 越小（偏序）越精确 2、存在描述一个值 v 的最好属性值 l

第4章 抽象解释 4.1节 将“程序分析对语言的语义是正确的”这个 概念公式化 方式2：表示函数 -B:V→L,将v映射到表示它的最好属性值 两种方式之间的等价 -从B可以定义相关的可接受R 从可接受R可以定义相关的B

第4章 抽象解释 4.1 节 将“程序分析对语言的语义是正确的”这个 概念公式化 • 方式2：表示函数 –  ： V → L， 将 v 映射到表示它的最好属性值 l • 两种方式之间的等价 – 从可以定义相关的可接受R – 从可接受R可以定义相关的

第4章 抽象解释 4.1节 将“程序分析对语言的语义是正确的”这个 概念公式化 举例 数据流分析：常量传播 一控制流分析：运行时变量所指称的函数 适度的推) 语言语义：程序参数和结果属于不同的论域 程序属性：描述它们的属性则也属于不同的论域 正确性关系：相应地，由两个关系R和R2组成 表示函数：相应地，由两个表示函数B和B组成

第4章 抽象解释 4.1 节 将“程序分析对语言的语义是正确的”这个 概念公式化 • 举例 – 数据流分析：常量传播 – 控制流分析：运行时变量所指称的函数 • 适度的推广 – 语言语义：程序参数和结果属于不同的论域 – 程序属性：描述它们的属性则也属于不同的论域 – 正确性关系：相应地，由两个关系R1和R2组成 – 表示函数：相应地，由两个表示函数1和2组成

第4章 抽象解释 4.2节 用加宽和收缩技术来获得最小不动点的较好 近似，并使所需计算步数得到限制 加宽算子 上界算子 上界算子作用到一个序列，得到一个上升序列 加宽算子 1、对上升序列加宽得到的序列能够稳定 2、对单调函数f的迭代序列(f(L)n,用加宽算 子加宽后得到的序列会稳定，并且 Lp(f)

第4章 抽象解释 4.2 节 用加宽和收缩技术来获得最小不动点的较好 近似，并使所需计算步数得到限制 • 加宽算子 – 上界算子 上界算子作用到一个序列，得到一个上升序列 – 加宽算子 1、对上升序列加宽得到的序列能够稳定 2、对单调函数f 的迭代序列(f n (⊥))n，用加宽算 子加宽后得到的序列会稳定，并且 lfp(f )

第4章 抽象解释 4.2节 用加宽和收缩技术来获得最小不动点的较好 近似，并使所需计算步数得到限制 收缩算子 受f(fvU) )的启发 注意，收缩算子并不是一个下界算子 一对下降序列收缩得到的序列能够稳定，稳定后的 值 yp(f)

第4章 抽象解释 4.2 节 用加宽和收缩技术来获得最小不动点的较好 近似，并使所需计算步数得到限制 • 收缩算子 – 受f (lfp(f)) lfp(f)的启发 – 注意，收缩算子并不是一个下界算子 – 对下降序列收缩得到的序列能够稳定，稳定后的 值 lfp(f )

第4章 抽象解释 4.3节 伽罗瓦连接和伽罗瓦插入是表达程序的属 性空间L和属性空间M之间联系的一种工具 L和M的例子 (P(Z),)(Interval, )(Range,)(P(Sign), 伽罗瓦连接的定义 -抽象函数和具体函数 它们以及它们的复合要满足的性质 1、一种表示方式称为伽罗瓦连接 2、另一种表示方式称为adjunction

第4章 抽象解释 4.3 节 伽罗瓦连接和伽罗瓦插入是表达程序的属 性空间L和属性空间M之间联系的一种工具 • L和M的例子 (P(Z), ), (Interval, ), (Range, ), (P(Sign), ) • 伽罗瓦连接的定义 – 抽象函数和具体函数 – 它们以及它们的复合要满足的性质 1、一种表示方式称为伽罗瓦连接 2、另一种表示方式称为adjunction

第4章 抽象解释 4.3节 伽罗瓦连接和伽罗瓦插入是表达程序的属 性空间L和属性空间M之间联系的一种工具 伽罗瓦连接的定义 -抽象函数a和具体函数y 它们以及它们的复合要满足的性质 1、一种表示方式称为伽罗瓦连接 2、另一种表示方式称为adjunction 用表示函数β来定义伽罗瓦连接 -用抽取函数来定义伽罗瓦连接

第4章 抽象解释 4.3 节 伽罗瓦连接和伽罗瓦插入是表达程序的属 性空间L和属性空间M之间联系的一种工具 • 伽罗瓦连接的定义 – 抽象函数和具体函数 – 它们以及它们的复合要满足的性质 1、一种表示方式称为伽罗瓦连接 2、另一种表示方式称为adjunction – 用表示函数来定义伽罗瓦连接 – 用抽取函数来定义伽罗瓦连接