（计算机科学与技术专业论文）基于抽象解释的数值程序分析技术研究.pdf

国防科学技术大学研究生院硕十学位论文 摘要 随着计算机软件越来越多地渗透到社会经济生活的各个方面，人们的衣食住 行都离不开软件。软件失效特别是一些关键系统的软件失效会引发巨大的损失， 构造可信软件已经成为现代软件技术发展和应用的重要领域和必然趋势。 程序的正确性验证一直以来都是计算机科学中的一个挑战性问题，抽象解释 理论为程序静态分析提供了一个通用框架，可以在编译时自动地推导程序的动态 性质。基于抽象解释的数值程序分析可以自动推导程序中数值变量间的不变式关 系，这对于编译优化、程序错误检查至关重要。本文建立了一个面向c 和f o r t r a n 程序并支持过程间分析的数值程序分析框架，c 或f o r t r a n 源程序经过预处理后转 化为具有统一格式的中间表示形式，然后基于该中间表示抽取与源程序语义等价 的语义等式，最后在该语义等式上进行不动点迭代计算从而得到程序不变式，在 得到的程序不变式基础上可以检查程序的运行时错误或者证明系统满足某种约束 条件。 在该原型系统框架中，本文还对数组和过程间调用等复杂语法结构进行了建 模和抽象。通过将分析时的循环展开策略扩展到抽象解释的框架下，不仅提高了 分析精度，而且能够处理大部分因数组使用而带来的程序分析上的问题；针对过 程间分析，通过“变量名替换 将实际参数之间的关系传递到形式参数中，可以 有效的提高分析精度。 根据以上思想，我们在l l v m 编译平台上实现了一个面向c 和f o r t r a n 数值程 序的静态分析工具c f a i e r ，c f a i e r 采用模块化的设计，具有良好的可扩展性， 我们对一些相对简单但具有代表性的程序进行了实验，实验结果表明，c f a i e r 的 分析结果在保证一定效率的前提下具有较高的精度。 主题词：静态分析，抽象解释，值范围分析，过程间分析，数值抽象域，数组抽 象，数组越界 第i 页 国防科学技术大学研究生院硕士学位论文 a b s t r a c t a l o n gw i t hm o r ea n dm o r ea p p l i c a t i o n so fs o f t w a r ei ne c o n o m ya n ds o c i e t yl i f e ， s o f t w a r ei n v a l i d a t i o ni ns o m ek e ys y s t e m sm a yb r i n gt r e m e n d o u sl o s s c o n s t r u c t i o no f r e l i a b l es o f t w a r eh a sb e c o m ea ni m p o r t a n ta r e aa n di n e v i t a b l et r e n di nm o d e ms o f t w a r e t e c h n o l o g yd e v e l o p m e n t t h ev a l i d a t i o no fp r o g r a m sc o r r e c t n e s si sa l w a y sac h a l l e n g ep r o b l e mi nc o m p u t e s c i e n c e t h et h e o r yo fa b s t r a c ti n t e r p r e t a t i o np r o v i d e sag e n e r a lf r a m e w o r kf o rs t a t i c a n a l y s i sw h i c hc a nd e d u c et h ep r o g r a m sd y n a m i cp r o p e r t ya u t o m a t i c a l l y v a l u er a n g e a n a l y s i sb a s e do na b s t r a c ti n t e r p r e t a t i o nc a ng i v et h ei n v a r i a n tr e l a t i o n s h i po fv a r i a b l e s a te v e r yp r o g r a mp o i n tw h i c hi sv e r yi m p o r t a n tt oc o m p i l a t i o no p t i m i z a t i o na n de r r o r e x a m i n a t i o n w ep r o p o s e da ni n t e r p r o c e d u r a lf r a m e w o r kt h a ta n a l y s e sv a l u er a n g e i n f o r m a t i o no fn u m e r i c a lp r o g r a m s ，i tc a np r o c e s sca n df o r t r a np r o g r a m s co rf o r t r a n s o u r c ep r o g r a m sa r ef i r s tp r e p r o c e s s e dt oa nu n i f o r mr e p r e s e n t a t i o n s ，a n dt h e nw ed r a w t h es e m a n t i ce q u a t i o nw h i c hi se q u i v a l e n tt ot h es o u r c es e m a n t i c s ，a tl a s t ，t h ei t e r a t i v e c o m p u t a t i o ni sd o n eo nt h i ss y n t a xe q u a t i o nt og e tt h ep r o g r a m1 n v a r i a n t b e s i d e s ，w em o d e l e ds o m ec o m p l e xs y n t a xs t r u c ts u c ha sa r r a ya n di n t e r p r o c e d u r a l f u n c t i o n c a l l i n g v i ab r i n g i n gl o o pu n r o l l i n g i n t ot h ef r a m e w o r ko fa b s t r a c t i n t e r p r e t a t i o n ，t h ep r e c i s i o no fa n a l y s i sr e s u l ti sg r e a t l yi m p r o v e da n dm o s tp r o g r a m a n a l y s i sp r o b l e m sb r o u g h tb yt h eu s a g eo fa r r a y t ot h eq u e s t i o no fi n t e r p r o c e d u r a l a n a l y s i s ，v i ar e p l a c e m e n to f t h ef o r m a lp a r a m e t e r sb yt h ea c t u a lp a r a m e t e r s ，t h ea n a l y s i s p r e c i s i o nc a n b ei m p r o v e d b a s e do nt h eu p w a r di d e a ，w ei m p l e m e n tas t a t i cp r o g r a ma n a l y s i st o o lo r i e n t e dt o ca n df o r t r a ns o u r c ep r o g r a m i t sn a m e dc f a i e r ( ca n df o r t r a np r o g r a ma b s t r a c t i n t e r p r e t a t e r ) ，c f a i e ru s e sm o d u l a r i z e dd e s i g n m e n t ，t h ee x p e r i m e n ti n d i c a t e st h a to u r f r a m e w o r ki sv e r ye x t e n s i v ea n dp r e c i s e k e yw o r d s ：s t a t i ca n a l y s i s ，a b s t r a c ti n t e r p r e t a t i o n ，i n t e r p r o c e d u r a ia n a i y s i s ， n u m e r i ca b s t r a c td o m a i n ，v a l u er a n g ea n a l y s i s ，a r r a ya b s t r a c t i o n 第i i 页 国防科学技术大学研究生院硕士学位论文 表目录 表3 1图3 2 左侧程序中各程序点的抽象值2 2 表3 2 p r 0 9 2 程序中各程序点的抽象值2 2 表3 3p r 0 9 3 中各程序点的抽象值2 3 表3 4p r 0 9 3 在加宽延迟策略下的取值分析3 6 表3 5 p r 0 9 3 应用循环展开和加宽延迟策略的取值分析3 7 表4 1 数组初始化程序“桕结点处在迭代分析中各结点的抽象值。4 8 表5 1 c f a i e r 和i n t e r p r o c 实验结果对比5 0 表5 2c f a i e r 和文【2 1 】工作的实验对比5 2 第1 i i 页 国防科学技术大学研究生院硕十学位论文 图目录 图1 1 系统框架6 图3 1l l v m 体系结构图2 0 图3 2 含i f - e l s e 条件测试语句的程序p r 0 9 1 ( 左) 及其对应的控制流图( 右) 2 1 图3 3i f 条件判断程序p r 0 9 2 ( 左) 及其对应的控制流图( 右) 2 2 图3 4 程序p r 0 9 3 ( 左) 及其对应的控制流图( 右) 2 3 图3 5 经典的w o r k l i s t 迭代算法3 5 图3 6 控制流图中三种不同的控制结构3 7 图3 7 基于抽象解释的不动点求解器迭代算法3 9 图4 1一段函数调用代码及其对应的控制流图4 1 图4 2 含过程间调用的数据流迭代算法4 3 图4 3 递归函数调用的控制流图4 4 图4 4 简单的数组程序4 6 图5 1由于精度损失所带来的数组越界的误报5 l 第l v 页 独创性声明 本人声明所呈交的学位论文是我本人在导师指导下进行的研究工作及取得 的研究成果。尽我所知，除了文中特别加以标注和致谢的地方外，论文中不包含 其他人已经发表和撰写过的研究成果，也不包含为获得国防科学技术大学或其它 教育机构的学位或证书而使用过的材料。与我一同工作的同志对本研究所做的任 何贡献均已在论文中作了明确的说明并表示谢意 学位论文题目： 基王抽基篮登的熬焦猩庄佥堑技盛婴究 学位论文作者签名：篷苤生 日期： 渺7 年他月节日 学位论文版权使用授权书 本人完全了解国防科学技术大学有关保留、使用学位论文的规定。本人授权 国防科学技术大学可以保留并向国家有关部门或机构送交论文的复印件和电子 文档，允许论文被查阅和借阅；可以将学位论文的全部或部分内容编入有关数据 库进行检索，可以采用影印，缩印或扫描等复制手段保存，汇编学位论文 ( 保密学位论文在解密后适用本授权书) 学位论文作者签名：堡查二至 作者指导教师签名： 2 萎 日期：即口7 年，月2 7 日 嘲：研钆硼2 7 日 国防科学技术大学研究生院硕士学位论文 第一章绪论 随着计算机技术的发展和信息化程度的提高，软件已经渗透到国民经济和国 防建设的各个领域并发挥着重要作用。软件与人们的生活息息相关，特别是在一 些关键系统如医疗器械、飞行控制和金融系统，软件的可靠性直接关系到人们的 生命财产安全，人们对软件的可靠性提出了更好的要求。 程序中数值变量的取值范围对于编译优化、错误检查至关重要，然而面向实 际程序精确的值范围分析在理论上是不可能的。抽象解释是一种构造和逼近程序 不动点的理论，其实质是在计算效率和计算精度之间的一种权衡。基于抽象解释 的数值变量值范围分析，可以给出程序中每个程序点的数值信息。本文建立并实 现了一个过程间的数值变量值范围分析框架，c 或f o r t r a n 的源程序经过编译 预处理和语义抽取，获取与源程序语义等价的基于图表示的语义等式，然后在该 语义等式上进行迭代计算得到变量的数值信息；同时，本文还对数组和过程间调 用等复杂语法结构进行了建模和抽象。 1 1 研究背景 2 1 世纪以来，随着计算机应用的不断发展，软件已经渗透到国民经济和国防 建设的各个领域，在信息社会中发挥着重要作用。目前，计算机软件已经被广泛 应用于航天航空、工业控制、金融、医疗、交通等领域。但是随着软件规模的扩 大，以及人们对软件理论认识的不足，软件质量和开发现状并不令人满意。例如 软件失效导致1 9 9 6 年6 月a r i a n e 五型火箭发射失败。因此，人们对软件的正确性、 可靠性、保密性等高可信性质提出了非常高的要求和十分的关注。据统计，即使 经过编译和测试的程序中平均每千行代码仍包含1 0 到2 0 个错误【l 】。如何提高软件 可靠性已成为一个亟待解决的问题。一方面，人们需要充分认识软件工程的特殊 规律，采用更加标准、规范、高效的模式开发软件，另一方面，对于成型的软件 进行测试和验证，以查找可能存在的错误或验证软件满足某些性质。目前，有很 多种软件查错和验证技术，包括软件测试、模型检验、定理证明和抽象解释等。 软件测试是常用的查错技术，具有极高的精度，因为它所发现的错误通常就是 程序执行时所产生的。它的可扩展性也很好，同时也具有比较高的自动化程度。然 而，覆盖率是软件测试最大的弱点。很多在边界条件下才会发生的错误不能在软件 测试过程中被发现。 形式化方法是分析软件和硬件中“b u g ”的有效方法，也是认证或者证明软件系 统是否满足某些关键性质的有力工具。定理证明和模型检验是能够自动实现的典 第1 页 国防科学技术大学研究生院硕士学位论文 型形式化方法，模型检验工具如s p i n l 2 1 、c b m c t 3 j 通过遍历系统所有状态空间，能 够对有穷状态系统进行自动验证，并自动构造不满足性质的反例。对于无穷状态 系统或状态数目超出现有计算机处理能力的复杂有穷状态系统；模型检验方法难 以解决状态空间爆炸的问题；定理证明方法能够应用于解决无穷状态系统的验证， 但是，一阶逻辑是半可判定的，机械化的定理证明过程并不能保证停机。 静态错误检测方法不需要运行程序，而是通过对程序代码的分析检查程序中 隐藏的错误，类型推导【4 】【5 1 、抽象解释【6 】【7 1 、符号执行【8 1 是常用的静态检测方法。类 型推导是指由机器自动地推导出程序中变量和函数的类型，程序中的数据可以按 照一定的规则划分为不同的集合，把一个集合作为一种数据类型，然后利用类型 理论中的算法进行推导，类型推导具有良好的可扩展性，能够处理大规模的程序， 但是不适用于控制流相关的分析。在处理控制流相关的分析时，需要引入子类型 的概念。符号执行是一种增强的程序测试技术，但是，符号执行不是将程序运行 起来测试一组输入，而是利用抽象的符号来表示程序中的变量值，以符号化的形 式，模拟程序的运行时情况，一次符号执行的结果可能等价于一组常用的程序测 试用例，符号执行常与约束求解结合使用，可以精确地静态模拟程序的执行以发 现程序中的隐藏错误。但是由于程序的执行路径会随着程序规模成指数级增长， 运用符号执行进行检查时就需要选取一定数量的路径进行分析。 抽象解释理论是一种能够处理计算机科学中不可判定问题和非常复杂问题的 有效方法。它为不可判定问题和非常复杂问题的逼近求解提供了系统性的构造方 法和有效算法。基于抽象解释的数值程序分析技术可以给出每个程序点的数值变 量取值信息，由此可以推断出源程序中是否存在除零错、数组越界、整数溢出等 多种运行时错误；如果所采用的分析方法是完备的，还可以证明软件系统中不存 在某种运行时错误。 1 2 相关工作 抽象解释首先是由ec o u s o t 和r c o u s o t 于1 9 7 7 年提出的用于构造和逼近程 序不动点的理论，它是一种逼近程序语义的静态分析技术。程序语言描述了所有 用该语言编写的程序的语义，程序语义则描述了对象域上的计算过程和结果。如 果一个程序的语义可以由函数f 描述，则我们可以通过求解不动点方程x = f ( x ) 来 研究程序的性质。抽象解释的本质是在计算效率和计算精度之间进行权衡，通过 损失计算精度来取得计算的可行性，再通过迭代提高计算的精度。当找到合适的 方法对程序具体域进行抽象后，得到的抽象域的规模大大减小，达到可计算的范 围。再通过计算找到抽象域的不动点集合，并将其映射到具体域中。因此，抽象 第2 页 国防科学技术大学研究生院硕士学何论文 解释的主要问题是如何针对某些性质找到合适的语义函数，计算得到的不动点集 合，并且使得精度在可接受的范围内。 抽象解释为用于描述计算机系统行为的语义模型提供了进行可靠近似的理论 框架，并提供了系统性的构造方法来对计算机科学中不可判定的或复杂的问题进 行近似。目前，抽象解释在软硬件系统分析与验证领域取得了广泛的应用，其应 用领域涉及静态分析、程序转换、类型推导、模型检验、语法分析与解析、信息 流安全、安全协议验证、恶意代码检测、计算生物学、量子计算等。 而基于抽象解释的数值程序分析旨在产生、发现程序中某个程序点的数值不 变式，即每次程序执行均满足的数值变量( 整型变量、实型变量、浮点型变量等) 间的关系。基于抽象解释的数值程序分析在程序分析与验证、优化等方面都有着 广泛的应用，可用来分析程序中是否有除零错、数组越界、整数溢出等运行时错 误，也可用来分析程序中的断言以及契约中的前置条件、后置条件和不变式。 基于g a l o i s 连接的抽象解释理论框架的程序验证工作主要以静态分析工具 a s t r e e 9 】为主要研究成果，研究以c 程序编写的运算密集型的嵌入式实时安全攸 关软件系统作为研究对象，检查软件系统中的运行时错误作为主要研究内容。 a s t r e e 首先对软件系统进行编译链接，得到对应的抽象语法树，针对抽象语法 树使用结构归纳法构造软件系统的不动点语义，不动点语义计算过程中使用基于 阈值的w i d e n i n g 算子，使计算过程收敛或加速其收敛。a s t r e e 以存储抽象域和 算术抽象域上的计算抽象程序运行过程中的计算。算术抽象域包括区间抽象域、 八边形抽象域等多种抽象域。在计算精度要求较高时，八边形抽象域代替区间抽 象域进行抽象计算。a s t r e e 的抽象分析过程使用了参数化的方法，用于调整抽 象计算的计算精度和计算效率之间的平衡关系。基于软件系统的抽象语法树以及 存储抽象域和算术抽象域的迭代计算得到抽象的不变式形式的后向不动点，以前 向传播的方式根据后向不动点检查软件系统是否存在运行时错误，对于虚假反例， a s t r e e 基于数据依赖和控制依赖的后向程序切片方法定位引起虚假范例的变量 集合，对变量集合中与验证性质相关并且缺少精确抽象计算结果的变量集合采用 计算精度较高的八边形抽象域进行精化。a s t r e e 在应用领域专家进行参数设置 后自动运行，它的抽象分析过程遍历软件的每一个抽象状态，不会遗漏任何一个 运行时错误，并且抽象分析的过程总是终止的。例如，空客a 3 4 0 有线飞行系统的 软件代码量为1 3 2 0 0 0 行，a s t r e e 完全自动地验证了该软件中不存在运行时错误， 在2 8 g h z 、3 0 0 m b 内存的p c 机上，验证时间仅为1 小时2 0 分钟。 n a s a 的a m e s 研究中心开发了基于抽象解释的数组越界访问检查工具 c g s ( cg l o b a ls u r v e y o r ) 1 0 】。c g s 根据航天应用程序大量通过指针操作数据的特点， 其对内存的抽象不仅包含了数值变量，还包含了用于刻画指针及其别名的符号信 第3 页 国防科学技术大学研究生院硕士学位论文 息。相应地，c g s 为待检查程序的每个函数生成两组独立的语义方程。其中，一 组描述指针的指向集合之间的包含关系：另一组使用d b m ( d i f f e r e n t b o u n dm a t r i c s ) 抽象域描述数组下标和数组大小的数值关系。指针分析和数值分析通过按需交互 提高各自的分析精度。此外，c o s 的设计初衷是在获得一定分析精度的前提下使 得程序分析的开销可以被n a s a 的软件工程师所接受。因此，c g s 采用了一些损 失精度的分析，如结构体成员不敏感的分析、不精确的指针分析等。和a s t r e e 不同，c g s 的分析结果不是完备的，即c g s 针对某些错误可能存在漏报的情况。 对程序具体语义的自动分析是比较困难的。基于完备格理论，抽象解释把程 序的具体属性和操作映射到抽象域( a b s t r a c td o m a i n ) 中。抽象解释忽略了程序中与 验证性质无关的信息，且能够得到程序语义的可靠性逼近。抽象域是抽象解释的 重要组成部分。目前，人们已经实现了若干个抽象域，如区i b q ( i m e r v a l ) 抽象域t 7 1 、 八边形( o c t a g o n ) 抽象域【1 2 j 和凸多面体( c o n v e xp o l y h e d r a ) 抽象域川等。然而，这些抽 象域实现的接口不尽相同。此外，有的抽象域实现缺少应有的功能。 a p r o n 2 0 j 项目为各种抽象域提供一组必需的公共接1 3 ，并且实现了几种典型 的抽象域。a p r o n 项目的预期成果是识别出抽象域的实现所必需的基本功能，并 详细地设计抽象域的a p i 。基于抽象解释的分析工具可以把a p r o n 用作抽象域， 从而减少了开发人员的工作量。 目前，基于a p r o n 库，国外已经实现了一个过程间的开源数值程序分析工具 i n t e r p r o c 2 2 j ，该工具用逻辑编程语言o c a m l 编写，是一个实验性的工具平台，只能 分析开发者自定义的简单语言，无法处理实际程序，实用性不强。 1 3 课题研究的主要内容和框架 传统的基于抽象解释的数值程序分析工具的分析过程一般包括编译预处理、 语义等式提取和不动点迭代计算三个步骤。以a s t i 汪e 为例，每个单独的c 程序 经过g n ug c c 编译器预处理后，被c 解析器解析并生成相应的语法树，之后所有 的c 程序语法树被合并为一个单独的语法树，该单独的语法树被转化为a s t r e e 能够处理的简化c 语言( c 程序的一个受限子集) 的中间表示形式，在这种中间 表示形式上，所有的类型转换都是显式的，经过常量表达式检测和计算以及冗余 代码消除，就开展了对中间表示的迭代计算，a s t r e e 为其所使用的几个抽象域 开发了统一的接口，可以方便地在不同的抽象域上进行转换。 本文分析工具c f a i e r 的工作流程类似于传统的数值程序分析工具框架，但是， 在编译预处理阶段c f a i e r 选用低层次的虚拟编译器l l v m 1 4 】，不仅可以处理c 程 序，也可以分析f o r t r a n 程序。抽象域的选择是数值程序分析工具的一个关键因素， 第4 页 国防科学技术大学研究生院硕士学位论文 本文选用为各种抽象域的实现提供了通用接口层的a p r o n 抽象域库，可以更加方 便的在各种抽象域间进行转换，以有效地对精度和效率进行折衷。c f a i e r 在完成 分析后，会在程序中每个程序点处给出相应的数值不变式( 数值变量间关系) 。具 体而言，分析过程主要包括如下几个步骤： 1 1 通过编译器l l v m 编译c 或f o r t r a n 语言编写的源程序，获得l l v m 自定义的 后缀名为b c 格式的中间表示形式； 2 ) 调用l l v m 提供的用来操作其中间表示的接口函数，获取与源程序语义等 价的语义等式系统，并使用类似于控制流图的图结构来表示程序的语义等式； 3 ) 在该语义等式的图表示上，通过调用抽象域库a p r o n 提供的抽象域域操作 的通用接口，采用“迭代+ 加宽 策略计算程序不动点，从而获得数值不变式。 图1 1 给出了本文数值程序分析工具c f a i e r 的系统框架图。从功能上，c f a i e r 包括如下3 个模块：前端预处理和语义抽取模块、抽象域a p r o n 库模块、不动点 求解器模块。相应地，本文的主要研究内容可归纳如下： 1 ) 前端预处理和语义抽取：l l v m 将c 或f o r t r a n 源程序编译成具有统一 格式的中间表示，本文将研究如何基于l l v m 提供的中间表示构造和源程序等价 的基于图表示的语义等式，其中图结构中有向边迁移语句通过抽象域库a p r o n 中 提供的数据结构来表示。 2 ) 数值抽象域库：数值抽象域一方面为数值程序分析所需要的表达式、约束 等元素提供了统一的数据类型，另一方面为区间抽象域、八边形抽象域、多面体 抽象域等抽象域的域操作提供了通用的接口层。本文分析了各种抽象域的实现方 法及其所关注的数值性质。 3 ) 不动点求解器算法：在与源程序等价的语义等式的图表示基础上，不动点 求解器算法负责对该图表示进行不动点迭代计算，以获取程序不变式。本文研究 了各种不同的迭代策略对效率和精度的影响，并提出了一种分析时的循环展开策 略，有效的提高了分析精度。 4 ) 复杂程序结构的处理：基于抽象解释的值范围分析为获取程序中数值变量 的不变式关系提供了系统的框架，但是针对一些复杂程序结构的抽象和分析并没 有通用的方法。本文重点研究了抽象解释理论框架下数组和过程间分析的抽象及 其处理方法，在保证一定效率的前提下获得较高的分析精度。 第5 页 国防科学技术大学研究生院硕七学位论文 ：区间( 非关系型域) ：i 工【口，纠，y 【a ，b 】： ：多面体( 关系型域) ： ；x + y - 2 z = 1 0 ； j 八边形( 弱关系型域) ： y - - x 是一个完备格当且仅当：三中任何一个子集均存在最小上 界和最大下界。完备格 一般表示为q ，e ，11 ，1 7 ，上，t ，其中，上表示上的 最小元素，t 表示三上的最大元素，u 和几分别表示最小上界算子和最大下界算子。 定义2 ( g a l o i s 连接) 设婶， 和 是两个偏序集合，其中 称为具体 偏序集合， 成为抽象偏序集合，口：p 寸q 和苁q 寸p 是两个映射，序偶 称为一个伽罗华连接当且仅当：v x 尸，v yc q ，a ( x ) c _ y 当且仅当x - - z o o ，其中 映射瓣为抽象算子，7 称为具体算子。 第8 页 国防科学技术大学研究生院硕十学位论文 由g a l o i s 连接的定义可知，如果一个具体域上的域元素x 经过抽象算子锹射 后得到的抽象域域元素嘶) 小于等于( e ) 另一个抽象域上的域元素y ，那么x 肯 定小于等于( ) y 经过具体算子厂在具体域上的映射，反之亦成立。抽象算子口 和具体算子7 具有如下性质： ( 1 ) v xe p ，x y ( a ) ) ； ( 2 ) v ye q ，口( y ( 力) 印； ( 3 ) 神厂单调递增； ( 4 ) 两个g a l o i s 连接的合成仍然是g a l o i s 连接。 证明：( 1 ) 由 和 为偏序集合可知，o f ) e 口 ) ，由g a l o i s 连接 的定义a ( x ) e _ y 当且仅当x 缈) 知：x 上的元素，且x i - - x 2 有性质( 1 ) 可知，x 2 - y ( a ( x 2 ) ) ，因为x l x 2 ，故x l z ，则因为 是g a l o i s 连接，则有o f l ) e7 2 ( z ) ，又由于 是g a l o i s 连接，则有 o f 2 ( a l g ) ) - - - 7 1 ( 舱( z ) ) ；同理可证：当x ， = ， ， 【x i f f1 z ( 2 ) 布尔表达式的具体语义 和数值表达式的具体语义类似，使用函数p ：阻b 表示从程序中某个布尔类型 变量到其实际取值的映射函数，b = t r u e ，f a l s e ，在给定的程序环境中布尔变量v 的取值可能为t r u e ，也可能位知瓜p ，因此一个布尔变量可能存在两个映射函数， 设6 为函数p 的集合，使用函数p ：6 _ 只b ) ，只b ) 表示集合b 的幂集： a ( t r u e ) p ：2 t r u e ； 第1 2 页 国防科学技术大学研究生院硕士学位论文 p ( f a l s e ) ；：= f a l s e ； p ( b ) p ：= 加( 6 ) ) ； p ( c o n s t r a i n t ) p 2 i g a e x p r lo p ta e x p r 2 ) o ：2 t r u ei f fj v l t ( a e x p r l ) p ，3 v 2 t u ( a e x p r 2 ) p ，mo p ，v 2 ) u f a l s ei f fj h l l ( a e x p r l ) p ，j 屹k t ( a e x p r 2 ) p ，v i 、也不满足关系o p ，； u ( n o tb e x p r ) p ：2 1 ff t ( b e x p r ) 口) ； ( b e x p r la n db e x p r 2 ) o ：2 乞it l u ( b e x p r l ) p ，t 2 p ( b e x p r 2 ) p ) ； z ( b e x p r lo rb e x p r 2 ) p ：2 f lv t 2f 1 “( b e x p r l ) p ，t 2 p ( b e x p r 2 ) p ) 。 ( 3 ) 迁移语句的具体语义 对程序语句的抽象计算使得程序从一个程序点状态迁移到另一个程序点状 态，首先定义程序点状态：s s = ( l a b x e n v ) ，e n v 为程序中某结点处的抽象环境， 即该结点处所有可见的数值变量及其取值情况，e n v 的定义为：尸以胁_ 彩) ，而整 个程序的状态可以用一个有限长度的字( l a b x e n v ) + 来表示： 赋值语句的迁移计算： ( 1 ) x = a e x p r ( 1 ) ，1 ，l ( a e x p r ) w ( ，s ) jw ( ，s ) ( ，s i x _ v 】) 条件测试语句的迁移计算： 可分为两种情况，当条件测试语句不包含e l s e 结构时，其迁移计算为： ( 1 ) i f b e g i n b e x p r ( 1 i ) ；( 1 2 ) ；( 1 。) e n d i f ( 1 ) ( ，s ) 寸( ，s n s ) ，s = pt r u e p ( b e x p r ) 。) ( ，s ) 哼( ，s f q s ) ，s = pf a l s e p ( b e x p r ) 口) ( 厶，) 专( i r ：) 当条件测试语句包含e l s e 结构时，其迁移计算为： ( 1 ) f b e g i n b e x p r ( 1 1 ) ；( , ) e l s e ( ) ；( 厶) e n d i f ( 1 ) ( ，s ) 寸( f l ，sn s ) ，s = pt r u e u ( b e x p r ) 口) ( ，s ) 寸( ，s o s ) ，s = pf a l s e l ( b e x p r ) 口) ( 厶，) j ( ，。，s 。) ( 厶，s 。) j ( z ，) 循环语句的迁移计算 ( 1 ) w h i l eb e x p rb e g i n ( ) ；( 1 ) e n d w h i l e ( 1 ) ( ，s ) _ ( 厶，s n s ) ，s = pt r u e t (