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