（系统分析与集成专业论文）基于符号计算方法的程序验证技术研究.pdf

2 0 1 0d o c t o rt h e s i s s c h o o lc o d e ：10 2 6 9 s t u d e n tn u m b e r ：5 2 0 715 0 0 0 01 e a s c 皿n an 瓜m a lu n v i i l 瓜v s t u d yo np r o g r a mv e r i f i c a t i o n b a s e do ns y m b o l i cco m p u t a t i o n d e p a r t m e n t ： m a j o r ： s u b j e c t ： t u t o r ： a u t h o r ： s o f t w a r ee n g i n e e r i n gi n s t i t u t e s y s t e ma n a l y s i sa n di n t e g r a t i o n h i g h e f f i c i e n ta l g o r i t h mf o r a l g e b r a i ca n ds e m i - a l g e b r a i cs y s t e m p r o f l uy a n g b i nw u 2 0 1o 3 发表或撰写过的研究成果。对本文的研究做出重要贡献的个人和集体，均已在文中 作了明确说明并表示谢意。 作者签名：丛丛日期：铷f 。年f 月伽日 华东师范大学学位论文著作权使用声明 基于符号计算方法的程序验证技术研究系本人在华东师范大学攻读学位期 问在导师指导下完成的硕士博影( 请勾选) 学位论文，本论文的研究成果归华尔师 范大学所有。本人同意华东师范大学根据相关规定保留和使用此学位论文，并向主 管部门和相关机构如国家图书馆、中信所和“知网”送交学位论文的印刷版和电子 版；允许学位论文进入华东师范大学图书馆及数据库被查阅、借阅；同意学校将学 位论文加入全国博士、硕士学位论文共建单位数据库进行检索，将学位论文的标题 和摘要汇编出版，采用影印、缩印或者其它方式合理复制学位论文。 本学位论文属于( 请勾选) ( ) 1 经华东师范大学相关部门审查核定的“内部”或“涉密”学位论文奉， r 年月同解密，解密后适用上述授权。 ( ) 2 不保密，适用上述授权。 翩签名：耀) 本人签名：丛邀 7 q 年f 月 k e 日 涉密”学位论文应足已经华东师范大学学位评定委员会办公室或保密委员会审 定过的学位论文( 需附扶批的华尔师范大学研究生申请学位论文“涉密”审批表 方为有效) ，未经上述部门审定的学位论文均为公开学位论文。此卢明栏不填写的， 默认为公开学位论文，均适用上述授权。 武斌博士学位论文答辩委员会成员名单 姓名职称单位备注 周巢尘研究员中国科学院主席 张晓东教授上海交通大学 朱惠彪教授华东师范大学 刘静教授华东师范大学 郁文生教授华东师范大学 摘要 程序验证足计算机程序设计领域的前沿研究课题，如何保证程序正确性足计算 机科学的一个重大挑战近年来，随着符号计算理论的不断完善和程序验证中使用 精确无误差的数学方法的要求，使用符号计算理论来解决程序验证中的相关问题被 认为足一种有效途径本文利用符号计算的思想和方法研究了程序验征领域的三个 基本问题：循环不变式生成、程序终止性分析以及前置条件生成 循环不变式在程序的部分j 下确性验证中起着非常重要的作用，如何生成循环不 变式也足程序验证领域的挑战之一本文主要研究了多项式循环程序的不变式生成 问题首次将有限点集消去理想的思想和方法应用于多项式循环程序的不变式生 成，设计了一个多项式时问复杂度的循环不变式自动生成算法，可生成多项式等式 型循环不变式 程序的终止性分析问题也是长期以来为众多计算机科学家所关注的问题之一 本文主要研究了- 类带有非线性循环条件和线性赋值的循环程序的终止性分析问 题通过计算线性赋值矩阵的约当标准型，确定循环条件在循环次数充分大时的符 号，将这类循环程序的终止性分析问题转化为判断参系数半代数系统有无实解的问 题如果参系数半代数系统中的左端函数个数有限或者左端函数都具有整数周期， 则这类非线性循环程序的终止性问题足可判定的 另外一个值得研究的问题足如何计算合理的前置条件，使得循环程序在满足该 条件的前提下是终止的本文基于一阶常系数差分方程组的求解技术，设计了一个 高效、实用的前置条件生成算法我们将程序的循环赋值语句转化为程序变量关于 循环次数的差分方程组，计算差分方程组的闭形式解然后将闭形式解代入循环条 件，在循环次数充分大时，判断循环条件的符号，进而生成循环程序合理的前置条 件针对线性赋值程序给出了一个高效、实用的前置条件自动生成算法进而，对于 可求出闭形式解的非线性赋值循环程序以及运算可交换的多分支循环程序，也做了 相应研究 研究结果表明，符号计算足验证程序j 下确性的一种行之有效的方法我们期待 将符号计算中的一些经典算法更深入、广泛地应用到程序验证，并集成、研发新的 有前途的验证工具 关键词：程序正确性，程序验证，循环不变式，终止性分析，前置条件，归纳断言 映射 a bs t r a c t p r o g r a mv e r i f i c a t i o ni so n eo ft h ef r o n t i e rr e s e a r c ht o p i c si np r o g r a md e s i g nf i e l d ， w h i c hh a si m p o r t a n tt h e o r e t i c a ls i g n i f i c a n c ea n da p p l i c a t i o nv a l u e i nt h i sd i s s e r t a t i o n ，w e i n t r o d u c es o m ec l a s s i c a la l g o r i t h m si ns y m b o l i cc o m p u t a t i o ni n t op r o g r a mv e r i f i c a t i o n ， a n dm a i n l yd or e s e a r c h e so np r o g r a mv e r i f i c a t i o ni nt h r e eb a s i ca s p e c t s ：g e n e r a t i o no f p r o g r a mi n v a r i a n t s ，t e r m i n a t i o na n a l y s i sa n dg e n e r a t i o no fp r e c o n d i t i o n s l o o pi n v a r i a n t sp l a yav e r yi m p o r t a n tr o l ei np r o v i n gp a r t i a lc o r r e c t n e s so fp r o - g r a m s w em a i n l ys t u d yt h ei n v a r i a n tg e n e r a t i o no fp o l y n o m i a ll o o pp r o g r a m s w ef i r s t l y p r e s e n tan e wm e t h o df o rg e n e r a t i n gp o l y n o m i a li n v a r i a n t so fp o l y n o m i a ll o o pp r o g r a m s b yc o m p u t i n gv a n i s h i n gi d e a lo fs a m p l i n gp o i n t s ar e l i a b l ep o l y n o m i a lt i m ea l g o r i t h m f o rg e n e r a t i n gp o l y n o m i a li n v a r i a n t si se s t a b l i s h e d t e r m i n a t i o na n a l y s i so fl o o pp r o g r a m si sv e r yi m p o r t a n ti nm a n ya p p l i c a t i o n s ，e s - p e c i a l l yi nt h o s eo fs a f e t yc r i t i c a ls o f t w a r e i nt h i sd i s s e r t a t i o n ，w em a i n l ys t u d yt h et e r - m i n a t i o no fp r o g r a m sw i t hp o l y n o m i a lg u a r d sa n dl i n e a ra s s i g n m e n t s t h ed i s c u s s i o ni s b a s e do ns i m p l i f y i n gt h el i n e a rl o o p sb yi t sj o r d a nf o r m a n dt h e nt h ep r o c e s st of i n dt h e n o n t e r m i n a t i n gp o i n t sf o rg e n e r a lp o l y n o m i a lg u a r d sb er e d u c e dt os e m i a l g e b r a i cs y s t e m ( s a sf o rs h o r t ) s o l v i n g i ft h en u m b e ro ff u n c t i o n si ns a sa r ef i n i t eo rt h ef u n c t i o n sa r e i n t e g e rp e r i o d i c ，t h e nt h et e r m i n a t i o no fp r o g r a m si sd e c i d a b l e h o w e v e r , i n s t e a do f c o n s i d e r i n gc o m p l e t et e r m i n a t i o no f p r o g r a m s ，i e ，t e r m i n a t i o n f o ra l li n p u t s ，w ea r em o r ec o n c e m e dw i t ht h ef o l l o w i n gq u e s t i o n s ：h o wi ft h ec o d eo n l y t e r m i n a t e sf o rs o m ei n p u t s ? i nt h i sd i s s e r t a t i o n ，ar a p i da n dr e l i a b l ea l g o r i t h mf o rg e n e r - a t i n gp r e c o n d i t i o n so fl o o pp r o g r a m sw i t hl i n e a ro rn o n l i n e a ra s s i g n m e n t s i se s t a b l i s h e d c l e a r l y , al o o pp r o g r a mc a nb ee l e g a n t l ye x p r e s s e db ym e a n so fas y s t e mo fd i f f e r e n c e e q u a t i o n s ，w h i c hd e s c r i b e st h eb e h a v i o ro ft h el o o pv a r i a b l e sc h a n g i n ga te a c hi t e r a t i o n t h em e t h o di sb a s e do ns o l v i n gs y s t e m so fd i f f e r e n c ee q u a t i o n sc o r r e s p o n d i n gt ot h el o o p a s s i g n m e n t s ，a n dt h e ns u b s t i t u t i n gt h es o l u t i o n si n t ot h el o o pg u a r d st oc o m p u t ep r e c o n - d i t i o n st h a te n s u r et h et e r m i n a t i o no ft h el o o pp r o g r a m s t h er e s u l t si n d i c a t et h a ts y m b o l i cc o m p u t a t i o ni sav a l i dt o o lf o rs t u d y i n gp r o g r a m v e r i f i c a t i o n w eh o p et h a tm o r ea n dm o r ec l a s s i c a la l g o r i t h m si ns y m b o l i cc o m p u t a t i o n c a nb ei n t r o d u c e di n t or e s e a r c ho np r o g r a mv e r i f i c a t i o n k e yw o r d s ：p r o g r a mc o r r e c t n e s s ，p r o g r a mv e r i f i c a t i o n ，i n v a r i a n t ，t e r m i n a t i o na n a l - y s i s ，p r e c o n d i t i o n ，i n d u c t i v ea s s e r t i o nm a p n 第一章 1 1 1 2 1 3 1 4 第二章 2 1 2 2 2 3 2 4 第三章 3 1 3 2 3 3 第四章 4 1 4 2 4 3 口三王 目豕 绪论 程序正确性研究方法概述 程序f 确性研究概况 符号计算简介。，。 本文的选题和主要工作 循环不变式的自动生成 参系数半代数系统的实解分类及应用 有限点集消去理想的g r 6 b n e r 基 基于消去理想的循环不变式自动生成 本章小结。 一类非线性循环程序的终止性分析 齐次多项式函数循环条件的程序终止性分析 一般情形 本章小结 循环程序终止的前置条件的自动生成 差分方程组的求解。 前置条件的自动生成算法 本章小结 第五章结束语 参考文献 致谢 攻读博士学位期间发表论文和参与科研情况 1 2 8 挖 侈侈拍记牾 铅舛钞的 卯矽卯 好 好 b ：2 第一章绪论 程序验证( p r o g r a mv e r i f i c a t i o n ) 是研究程序正确性的理论，足计算机程序设计 领域的传统研究课题，但迄今为止，对常见的绝大多数程序而言，实现完全的f 确性 验证还足很困难的 4 5 1 然而，随着计算机应用范围的同益扩大和计算机程序设计 语言的迅速发展，如何保汪程序的正确性、提高软件的可信度一直足计算机科学界 高度关注的一个重要问题，也足推动计算机科学发展的主要动力之一 一段程序足正确的，是指这段程序能正确无误地完成程序设计时所期待的功 能目前，为了检测一个程序足否正确地实现了预定的目标，通常使用两种方法：程 序测试( p r o g r a mt e s t i n g ) 和程序验证程序测试通常足规定些初始数据，试验性地 执行这个程序，测试其足否能产生所要的答案如果发现有误，就检查和修改所编写 的程序，直至对所有规定的初始数据，都能产生预期的结果但是，程序对不同的初 始数据的加工过程足不同的，而初始数据的取值范围往往又十分广泛因此，使用测 试方法穷尽程序的各种可能加t t 过程以确保程序的正确性，几乎足不可能实现的 因此，“测试方法只能发现程序的错误，而不能确保程序无误 7 5 ? 而程序验证足研 究程序正确性的理论，是研究如何使用数学方法严格证明程序所有可能的初始数据 都足符合其预定目标的，因而足正确无误的 虽然程序测试不能保证待测程序没有错误，但这并没有阻碍它在实际中的应 用程序测试是面向目标代码( o b j e c tc o d e ) 的，因此程序员可以利用测试方法很快 找到错误并加以改正面对检测需求不明确的软件，程序测试也体现了其速度上的 优势相对测试而言，通常程序验证的工作量更大，但足验证技术也具有更多的优 点： 应用程序验证技术，我们可以在更深地层次洞察程序，并且能够帮助我们真正 理解程序的思想以及它的局限性 4 6 】； 程序验证技术可以更好的支持面向目标的程序开发( g o a l - o r i e n t e dp r o g r a m d e v e l o p m e n t ) 8 4 】； 由此可见，程序验证足保证程序正确性的一个基本而重要的手段，也足计算机软件 工程方法和技术中不可或缺的重要组成部分 1 华东师范大学博士学位论文第。章绪论 由于e d i j k s t r a ，c a r h o a r e ，r m i l n e r 以及a p n u e l i 等一大批计算机科学 家关于程序验证理论的出色工作，使得程序验证这一研究方向取得了广博的发展， 也产生了大量具有实用价值的理论和技术到上世纪八十年代，由于程序验证中数 学证明的复杂性，研究热度有所下降，甚至许多悲观的研究者认为程序验证的理论 和方法没有应用前途 符号计算作为一种精确、无误差的计算方法，正好符合程序验证使用正确无 误的数学方法的要求目前，随着符号计算理论与方法的迅猛发展，诸如量词消去 5 6 ，5 7 ，1 5 0 l ，多项式代数 1 2 0 ，1 2 1 ，1 2 3 ，1 2 4 ，1 4 6 1 ，g - r f b n e r 基【2 3 ，3 1 ，4 2 ，4 3 ，4 4 ，7 1 ， 7 2 ，8 1 1 ，参系数半代数系统的实解分类 1 3 ，2 0 ，5 1 ，1 5 7 ，1 5 8 ，1 6 3 ，1 6 4 】等等，为程序 验证提供了强有力的理论基础，验证技术及其应用的研究也随之活跃起来 众所周知，我们正处在信息时代，随着计算机应用范围的n 益扩大，软件系统 不仅仅出现在航空、医药、军事等安全攸关领域，我们的日常生活也与软件产品息 息相关但足，软件产品中的“b u g ”层出不穷，有些还导致了严重后果如何保证程 序的正确性、提高软件的可信度就显得尤为重要甚至，国际著名的计算机科学家、 图灵奖得主c a r h o a r e 提议将程序验证作为计算机科学中的一个重大挑战性 问题，希望能像人类基因组计划那样，通过国际合作，以求在该方向取得重大进展 【9 1 在如此严峻的形势下，我们将符号计算作为一种新的思想和方法应用于程序 验证研究，期待验证技术能有所创新正是基于上述考虑，本文将结合符号计算的思 想和方法，展开对程序验证理论和技术的研究 本章将从程序正确性研究方法、程序正确性研究现状、符号计算及其应用等方 面进行简要综述 1 1 程序正确性研究方法概述 本节将介绍几种目前较为常用的程序正确性检测技术，并且较详细地叙述在后 续几章中涉及到的重要概念和定义特别地，重点介绍e t 前最流行的程序正确性证 明和验证的方法之一公理化方法 1 1 1 程序测试 测试足目前工业界普遍采用的提高软件质量的重要手段，也是软件工程学术界 研究的主要内容之一虽然目前有不少工具能帮助用户统计测试过程中的各种信 息但是测试用例的设计( 或者说测试数据的生成) 是难题之一如何在给出比较少 的测试用例的条件下达到比较高的覆盖度，将足一个长期研究的课题 2 华东9 币范大学博士学位论文 1 1 2 模型检验( m o d e lc h e c k i n g ) 这类方法主要针对可归结为有限状态的程序这罩所谓的“状态”是指程 序变量的一种取值例如，假设程序中共有两个变量：布尔变量b 以及取值范 围为1 1 0 1 的整型变量n 那么该程序可以有2 0 个状态：( b = f a l s e ，7 , = 1 ) ， ( b = t r u e ，n = 1 ) ，( b = f a l s e ，n = 1 0 ，( b = t r u e ，佗= 1 0 ) 通过枚举所有的 状态，可以检查程序是否具有某些性质一般来说，程序可表示为状态机( 赋值语句 对应于状态迁移) ，其性质可用时序逻辑公式表示用模型检验方法可以自动地验证 很多通信协议和并发控制算法的正确性 i i 3 静态分析( s t a t i ca n a l y s i s ) 静态分析足指，不执行程序，通过类型推导( t y p ei n f e r e n c e ) ，抽象解释( a b s t r a c t i n t e r p r e t a t i o n ) 等手段检查程序中足否具有某种错误( 比如内存泄露) 有些工具也 使用特定的规则对程序进行检查比如在多线程程序中要求在使用共享变量时遵 守“使用前先加锁，使用后解锁”的规则 1 1 4 公理化方法 上面介绍的三种程序正确性检测方法都是以发现错误为主要目标的，接下来， 重点介绍一种以证明程序正确性为目标的验证技术公理化方法 公理化方法是目前最流行的程序j 下确性证明方法之一这种方法最早足1 9 6 7 年山r w f l o y d 基于流程图的验证而提出的 8 0 随后，c a r h o a r e 经过不断 发展和完善，于1 9 6 9 年提出程序验证的公理系统( 当时主要足针对w h i l e 型程序) 9 0 这个系统为使用严格的数理逻辑推理计算机程序的正确性提供了组逻辑规 则这种方法依赖于对程序的每个成分定义断言( a s s e r t i o n ) ，而我们可以应用这些 断言，建立程序与其语义( s e m a n t i c ) 之间的联系，换言之，可以建立程序与程序规约 ( p r o g r a ms p e c i f i c a t i o n ) 所表达的需求行为之间的联系 程序( p r o g r a m ) 描述了一个确定的输入状态如何转化为一个所需求的输出状 态，而程序规约准确地描述了程序所应实现的具体功能为了更好地利用规约来说 明程序，使用h o a r e 三元组( h o a r et r i p l e ) 来表示程序的执行h o a r e 三元组具有如下 形式： p ) s q ) ( 1 1 ) 其中 s 是一段程序； 3 华东师范大学博士学位论文 第。章绪论 p 是一个逻辑公式，被称作前置条件( p r e c o n d i t i o n ) 或s 的输入断言( i n p u t a s s e r t i o n ) ； q 足一个逻辑公式，被称作后置条件( p o s t c o n d i t i o n ) 或s 的输出断言( o u t p u t a s s e r t i o n ) 直观上，一段程序足正确的，足指它能满足给定的输入、输出关系，即满足程序 规约这里，给出程序正确性的定义： 定义1 1 1 ( 3 3 】) h o a r e 三元组( p ) s q ) 是部分正确的( p a r t i a lc o r r e c t n e s s ) ，是指如 果程序s 执行前满足断言p ，则当程序终止后，它一定蕴含断言q 定义1 1 2 ( 3 3 1 ) h o a r es - t l 组 p 】s q 是完全正确的( t o t a lc o r r e c t n e s s ) ，是指如 果程序s 执行前满足断言p ，并且程序s 终止，则它的最终状态一定蕴含断言q 由丁一段程序s 并不一定总是终止的，从上述定义可知，程序的部分正确性足 在假设程序终止的前提下证明的，而 程序的完全正确性= 程序的部分正确性+ 程序终止性 例1 1 3 考虑h o a r e 三元组 z = 5 ) 。：= 2 z z o ) 在本例中， 2 7 = 5 是前置条件； z ：= 2 x 是一段程序： z 0 是后置条件 显然这个三元组是部分正确的，也是完全正确的因为如果。= 5 ，并且执行z 乘以 2 ，我们得到z = 1 0 ，这是肯定蕴含z 0 的 例1 1 4 给定两个自然数z 和y ( o ) ，计算z 除以的商q u o 和余数r e m 计算q u o 和r e m 的程序的前置条件可以理解为“给定两个自然数z 和可( 0 ) i 如果规定取值范围是自然数n ，则前置条件可以用如下逻辑公式表示： ( z20 ) a ( y 0 ) 后置条件可以理解为“z 除以y 的商q u o 和余数r e m ：根据商和余数的性质， 后置条件可以用如下的逻辑公式表示： ( q u o y + r e m = z ) a ( 0 r e m ) a ( r e 订t o ) ) r e i n ：= r e m 一可； ( q u o y + r e m = z ) 八( o r e m ) a ( r e m 0 ； 1 ab a r = r s r 0 w h i l ez 0d o i fz 0t h e n z ：= 1 一z e l s e z ：= 一z 一1 e n di f e n dw h i l e 终忆但是没有线性秩函数，却有非线性秩函数z 2 或4 2 2 + z + 2 ，详细分析过程见 5 5 1 除了构造秩函数的方法，众多科学家还研究了其他程序终止性分析方法，以便 在实际应用中和秩函数方法互相补允a t i w a r i 针对无分支线性循环程序，研究发 现其终止性仅与线性赋值矩阵的正特征值所对应的特征向量有关，从而证明了这类 取值于实数的线性程序的终止性是可判定 1 4 1 m b r a v e r m a n 在a t i w a r i 工作的 基础上，证明了该类线性程序在取值于整数时，其终止性问题足可判定的 4 1 1 杨 路等进一步改进了a t i w a r i 的工作，利用计算机代数工具d i s c o v e r e r 计算符号约 当矩阵( j o r d a nm a t r i x ) ，从而避免了数值计算带来的误差 1 6 0 ，1 6 6 a b b r a d l e y 等 4 0 】针对多分支多项式程序( m u l t i p a t hp o l y n o m i a lp r o g r a m ) ，将其终止性证明问 题规约到希尔伯特第1 0 问题( h i l b e r t s1 0 一t hp r o b l e m ) ，最终证明该类程序的终止性 证明不存在完备算法同时，他们利用有限差分树( f i n i t ed i f f e r e n c et r e e ) 的方法对这 类程序的终止性分析进行了验证s l e u e 等针对多分支线性程序，利用构造和分 析区域图( r e g i o ng r a p h ) 的方法证明其终止性【1 1 3 】a p o d e l s k i 和a r y b a l c h e n k o 利用变迁不变式( t r a n s i t i o ni n v a r i a n t s ) 作为辅助断言( a u x i l i a r ya s s e r t i o n s ) 去证明程 序的终止性，并且这一方法也在他们开发的终止性分析工具r a n k f i n d e r 中得到了 应用另外，d b a b i c 等利用发散性质( d i v e r g e n c e ) 对一类特殊的非线性循环程序 ( n o n 1 i n e a ra n t i c h a i nw h i l el o o p ) 的终止性进行了分析 3 4 】 此外，a g u p t a 8 6 】以及毕忠勤等 2 8 ，3 7 】还对循环程序的非终止性( n o n t e r m i n a t i o n ) 问题，即循环程序终1 i ：的反例生成问题做了研究，有效地弥补了终lj ：性 分析的缺陷 华东师范大学博士学位论文 第。章绪论 1 2 3 前置条件研究概况 在上一小节，我们综述的研究方法基本都是针对循环程序的完全终止性问题， 即对于程序所有可能的初始值，判断程序足否终止但是，我们更加关心这样的问 题：( 1 ) 对于给定的初始值，循环程序是否终止；( 2 ) 如何计算合理的前置条件，使得 循环程序在满足该条件的前提下足终止的；( 3 ) 针对带有明确后置条件的循环程序。 如何计算合理的前置条件，使得循环程序在满足该条件的前提下终止，而且到达后 置状态由此可见，前置条件的研究对程序的验证、分析以及设计足非常重要的 目前，这一研究领域的挑战是如何生成合理的前置条件：由于平凡的前置条件 ( 即前置条件为空) 总足正确的，但是没有实用价值；而一个程序，甚至足非常简单的 程序，其最弱前置条件的生成也是很困难的 7 7 ，8 2 】在这种情况下，人们引入了最 弱充分前置条件( w e a k e s tl i b e r a lp r e c o n d i t i o n ) 的概念，对于给定的程序s 和后置条 件q ，通常记作叫i p ( s ，q ) 以w z p ( s ，q ) 为初始状态，程序s 要么不终止，要么s 的 输出状态蕴含条件q 注意，w l p ( s ，q ) 并不能保证程序s 的终止性由于研究最弱 前置条件的文献比较少，有些文献中也直接将w z p ( s ，q ) 称为w p ( s ，q ) ，如【11 2 】b c o o k 等利用构造潜在秩函数( p o t e n t i a lr a n k i n gf u n c t i o n s ) 的方法生成保证程序终止 的合理的前置条件 6 2 s g u l w a n i 等在文献 8 5 】中第一次提出了利用约束求解的 方法计算程序的最弱前置条件而且，a r b r a d l e y 在文献 3 8 】中利用约束求解的 方法构造程序的线性秩函数，将此方法改良后，也可用于计算程序的前置条件然 而，这两种方法都要求解非线性约束r l e i n o 11 2 】和c c a l c a g n o 4 8 】针对程序的 最弱充分前簧条件展开了研究 1 3 符号计算简介 本节首先介绍符号计算的概念和目前的进展，在此基础上，我们将阐述程序正 确性验证中引入符号计算方法的必要性和可行性 1 3 1 数学与科学计算 ， 数学是一切科学与技术的基础，是一切关键技术中的关键在古代，人类的原始 活动如狩猎以及猎物的分配就已离不开数的概念，而人类赖以生存的三维世界又离 不开各种形体引进数( 自然数继而整数和有理数) 以及它们之问的四则运算，研究 形( 点、线、圆、三角形等) 以及它们之间的相互关系导致了原始的数学数学的诞 生足人类生存和认识自然界的必然产物这门处理和研究数和形的学科伴随着人类 的进化，见诸于各种古代文明它的发展满足了各种社会活动的需要，如观天测地和 1 2 华东师范大学博士学位论文 商品与货币流通毋庸置疑，“计算”在数学中发挥着及其重要的作用 人类的文明不足停留在对生存的基本物质需求和实用上人们认识的不断提高 和对物质世界的探索导致了天文学、物理学和化学等这些学科的建立和发展都离 不开数学同时，人们还需要物质之外的意识和精神生活，从而导致了古典哲学和美 学这些自然科学和社会科学的发展和进步给数学提出了更高的要求，使其不能停 滞在简单的“计算”上随之而来，数系统不断地得到扩充，从而有了实数和复数数 学家对这些复杂的数系统进行了深入地研究，探讨它们的结构、性质和其中的运算 机制，并给出有效的计算方法数学家不满足_ 丁数的基本运算，他们进而追求数学的 优美和完善，探讨数系统的相容性和完备性，建立几何学、公理系统和逻辑推理机 制，引进有理函数、三角甬数和其它超越函数，创建和研究各式各样复杂的数学系 统如此一来，便形成了众多数学分支和各种数学理论、体系与流派但无论如何， “计算”是贯穿数学发展的一根主线 在现代，数学的一个重要特征和发展趋势，是数学学科自身的高度发展和其它 学科以及整个外部世界的联系、交叉、渗透与融合在不断地加强更重要的足，数 学的应用已经拓展到几乎每个科学领域和应用部门，而且在其中起着关键的不可替 代的重要作用 2 5 ，2 6 目前，数学应用的范围逐渐扩大，已从以往的传统领域( 天文 学、物理学和化学等) 扩展到非传统的领域( 如生物、医学以及高新技术领域) ，甚至 进入经济、金融、保险及很多社会科学的领域，深入到各行各业，可以说足无所不 在，且发挥着越来越重要的作用与之相对应的，在现代经济建设、科技发展过程中， “计算”也扮演者举足轻重的角色在对自然界和人类社会各种食物发展规律的研究 中，当从定性分析过度到定量分析时，就必然涉及计算小到每天的天气预报，大到 载人航天、核能开发以及各种矿藏的勘探与开采等高科技活动都离不开计算因此， 计算能力的强弱直接制约着一个国家的经济和科技发展速度 1 3 2 符号计算与数值计算 从上- , b 节的分析，我们可看出，数学特别足“计算”在解决灾际问题时扮演 着极端重要的角色然而，科学计算常常足一项非常繁琐的工作早期的计算主要 足靠人的大脑和纸笔演算来完成，计算效率低，可靠性也差进而，众多科学家致力 于“计算”的机械化及计算机械的发明创造，如算盘、对数计算器、计算尺、加法 机、l e i b n i t z 演算机、差分机等等直到计算机的出现和发展才大大提高了人类的计 算能力，从而也促进了科学技术的迅猛发展 从计算机发明垒今的六十年问，用计算机进行的科学计算主要足数值计算 ( n u m e r i c a lc o m p u t a t i o n ) ，即浮点数之间的运算在现行的计算机编程语言中很容易 1 3 s y m b o l i cc o m p u t a t i o n 是发表符号计算方面研究成果的主要国际期刊还有a p p l i e d m a t h e m a t i c sa n dc o m p u t a t i o n 。a p p l i c a b l ea l g e b r ai ne n g i n e e r i n g 和c o m m u n i c a t i o n a n dc o m p u t i n g 除以上杂志外，从大量的会议论文集中也可以查阅到各种符号计 算的研究成果和研究趋势另外，美i 垂i a s s o c i a t i o nf o rc o m p u t i n gm a c h i n e r y ( a c m ) 1 4 华东师范大学博士学位论文 支持的学术研讨会i n t e r n a t i o n a ls y m p o s i u mo ns y m b o l i ca n da l g e b r a i cc o m p u t a t i o n ( i s s a c ) 每年定期举行在亚洲各国举办的a s i a ns y m p o s i u mo f t e c h n o l o g yo n m a t h e m a t i c s ( a s t m ) 和a s i a ns y m p o s i u mo nc o m p u t e rm a t h e m a t i c s ( a s c m ) 也逐渐 成为国内外计算机数学工作者学术交流和报告研究成果的一个园地 同时，符号计算软件系统也在不断地发展、提高和完善其为数学的教学、研究 和应用开辟了新天地，即使数学实验成为可能，又使数学成果直接为实际服务以及 使数学的大众化成为可能 目前，一部分符号计算软件系统发展成为完整的计算机数学软件，如m a t h e m a t i c a 11 】，m a p l e 【6 等，以及以高小山为首席科学家领导研发的独立、完整、高效、具有 自主知谚 产权的数学机械化自动推理平台m m p 7 】，它们为科学研究、工程应用、教 学中的计算和推理提供了一个强有力的应用和开发甲台 1 3 3 符号计算研究现状 由丁符号计算在科学与工程技术以及高科技等领域应用范围的不断扩大，吸 引了越来越多专家学者的研究兴趣，也取得了丰厚的研究成果如量词消去【5 6 ，5 7 ， 1 5 0 ，多项式代数 1 2 0 ，1 2 1 ，1 2 3 ，1 2 4 ，1 4 6 ，g r 6 b n e r 基 2 3 ，3 l ，4 2 ，4 3 ，4 4 ，7 l ，7 2 ，8 1 】 等 吴文俊院士在二十世纪七十年代末提出了数学机械化的设想，为国内符号计算 的发展指明了研究方向f 2 1 ，1 5 5 在吴文俊院士开创性工作的影响下，经过国内外 专家、学者近三十年的努力，已经成功地将吴文俊院士首创的“吴方法”用于解决 力学 1 5 4 】、化学 1 5 3 】等传统领域及几何造型 1 5 5 、连杆设计【1 5 2 ，1 5 5 等高科技 领域的问题“吴方法”还被用于多项式因式分解【2 4 ，1 6 】，几何造型中的曲面形式转 换问题 5 2 ，1 2 】，逻辑公式的证明【1 5 1 ，计算机视觉 9 7 ，组合恒等式自动正明 5 3 】 等，逐渐形成了具有中国特色的数学机械化和自动化推理理论，不仅成功应用- 丁一 些相关科学分支，且成功地解决了一系列高新技术领域中的关键基础理论问题，获 得了国内外学术界的高度称赞和广泛重视 现阶段数学机械化研究主要关注的足科学研究与高新技术应用中经常遇到的 两类问题：方程求解和自动推理在非线性方程组求解方向上，吴文俊院士提出的 “吴方法”与结式消元法、g r 6 b n e r 基消元法同为国际通用的三大求解非线性方程组 的最完整的消元算法 2 4 我国很多学者在这领域取得了出色的成果杨路、候 晓荣、曾振柄提出了对任意次数的实系数多项式建立完全判别系统的一个通用算 法 1 4 ，1 5 】，使这个实代数问题得到圆满的回答张景中、梁松新解决了复系数多项 式完全判别系统的问题 1 9 】王东明基于“吴方法”研发了用于多项式消元和分解 的应用软件e p s i l o n 【3 ，1 4 7 】等等 1 5 华东师范大学博士学位论文第一章绪论 在自动推理方面，张景中、杨路、高小山、周咸青提出了几何定理机器可读性 证明