（计算机软件与理论专业论文）isabelle定理证明器的剖析及其在par方法par平台中的应用.pdf

摘要 形式化方法可以对系统进行严格的规约，并可以从不同的角度验证开发的 系统是否具有所期望的性质，在高可信软件的开发中越来越受重视。定理证明 是计算机领域中形式化验证的重要研究课题，对保证软件的正确性和可靠性具 有十分重要的意义。 i s a b e l l e 是基于高阶逻辑的交互式定理证明工具，它具有丰富的类型系统， 强大的规则库和灵活高效的命令集；它不仅支持多种对象逻辑，而且允许用户 自定义新的逻辑。 开发正确且高效的算法程序仍然是计算机科学中最具有挑战性的核心工 作。p a r 方法是薛锦云教授提出的基于分划和递推的算法程序设计方法；它是 一种简单实用的支持算法程序开发全过程的形式化方法，并对于理解和证明算 法程序十分有效，是算法程序设计和证明方法研究方面的重要突破。p a r 平台 是支撑p a r 方法的c a s e 工具。 使用定理证明工具对算法程序进行机械证明是一种发展趋势。本文分析了 i s a b e l l e 定理证明器的系统结构、验证原理和核心技术；根据p a r 方法肥a r 平 台开发算法程序的特点，探讨了如何运用i s a b e l l e 定理证明器形式化验证算法程 序的工作流程，并对一些算法程序进行正确性验证；最后，阐述了如何使用 i s a b e l l e 证明p a r 平台中部分转换代码的正确性。 本文的创新点体现在以下两个方面： 1 、提出了一种使用i s a b e l l e 定理证明器对算法程序进行机械验证的方法。 该方法既克服了传统手工验证过程的繁琐性和易错性等缺点；又达到“提高验 证效率和保证算法程序高可信”的目标，具有很好的实用价值。 2 、实现了i s a b e l l e 定理证明器和p a r 方法p a r 平台的有机结合。一方面， 算法程序的验证依赖于使用p a r 方法开发的循环不变式；另一方面，使用 l s a b e l l e 定理证明器验证了p a r 平台中部分转换代码的正确性，从而保证了a p l a 程序到可执行程序转换的一致性。 关键词：形式化方法、高可信软件、形式化验证、定理证明、高阶逻辑、交互 式定理证明器、算法程序、p a r 方法、p a r 平台 a b s t r a c t w i t ht h ef o r m a lm e t h o d ，w ec a nn o to n l yd e s c r i b et h ef o r m a ls p e c i f i c a t i o no f s y s t e m ，a n da l s ov e r i f yt h es y s t e m sp r o p e r t i e si n t h ed i f f e r e n t p o i n to fv i e w t h e r e f o r ef o r m a lm e t h o da t t r a c t sm o r ea n dm o r ea t t e n t i o n si n d e v e l o p i n g t r u s t w o r t h ys o f t w a r e a so n eo ft h ei m p o r t a n tr e s e a r c hb r a n c ho ff o r m a lv e r i f i c a t i o n ， t h e o r e mp r o o fp l a y sa ni m p o r t a n tr o l ei ne n h a n c i n gt h es a f t ya n dd e p e n d a b i l i t yo f s o f t w a r es y s t e m s 1 s a b e l l e ，b a s e do nh i g h e ro r d e rl o g i c ，i sa ni n t e r a c t i v et h e o r e mp r o v e r t h e r e a r ea b u n d a n tt y p e s ，p o w e r f u lw a r e h o u s eo fr u l e s ，f l e x i b l ea n de f f i c i e n ts e to f c o m m a n d s i s a b e l l en o to n l yp r o v i d e sv a r i o u so b j e c tl o g i c s ，b u ta l s op e r m i t su s e r st o d e f i n en e wl o g i cb yt h e m s e l v e s d e v o l o p i n gt h ec o r r e c ta n dh i g h - e f f i c i e n ta l g o r i t h m i cp r o g r a mi ss t i l lt h em o s t c h a l l e n g e n tp a r to fc o m p u t e rs c i e n c e p r o f x u ej i n y u nd i s c o v e r e dan o v e ld e s i g n m e t h o da b o u ta l g o r i t h m i cp r o g r a m ；t h i sm e t h o di sc a l l e dp a rm e t h o d ，b e c a u s e “p a r t i t i o na n dr e c u r a x ei t sf u n d a m e n t a lt e c h n i q u e s p a rm e t h o di saf o r m a l m e t h o d ，w h i c hc a nb e u s e di ni n f e t i n ga n dv a l i d a t i n gt h ec o r r e c ta l g o r i t h m i c p r o g r a m m e a n w h i l e ，p a rp l a t f o r m ，t h ec a s et o o lo fp a rm e t h o d ，w a sa l s o d e v e l o p e d i t sap r e v a l e n tt r e n d e n c yt oa u t o m a t i c a l l yv e r i f yt h ec o r r e c t n e s so fa l g o r i t h m i c p r o g r a mb ym e a n so ft h e o r e mp r o v e r i nt h i se s s a yia n a l y s e dt h es y s t e ms t r u c t u r e ， p r o o fp r i n c i p l e sa n dc o r et e c h n o l o g i e so fi s a b e l l e w i t ht h ec h a r a c t e r so fp a r m e t h o d p a rp l a t f o r m ，t h ep r o c e s sa b o u tv a l i d a t i n gt h ec o r r e c t n e s so fa l g o r i t h m i c p r o g r a mw a sa l s od i s c u s s e d ，a n dt h e nio f f e r e ds o m ee x a m p l e sa b o u tp r o o f i n gt h e a l g o r i t h m i cp r o g r a m s f i n a l l y , t h ev e r i f i c a t i o no fs o m ek e r n e lc o d e si ng e n e r a t o ro f p a rp l a t f o r mi sd i s p l a y e di nt h ee n d p a r to ft h i se s s a y t h ei n n o v a t i o n so ft h i sp a p e ra r em a n i f e s t e da sf o l l o w s ： 1 、is u m m a r i z e dam e t h o do nh o wt om e c h a n i c a l l yv e r i f ya l g o r i t h m i cp r o g r a m s b a s e do ni s a b e l l e t h em e t h o dn o to n l yo v e r c o m e st h es h o r t c o m i n g s ( s u c ha st h e c o m p l e x i t y , h i g h - c o s ta n df a l l i b l e n e s s ) o ft r a d i t i o n a l l ym a n u a lv e r i f i c a t i o n ，b u ta l s o a t t a i n st h eg o a lo fe n h a n c i n gt h ed e p e n d a b i l i t ya n de f f i c i e n c yo fv e r i f y i n gp r o c e s s a n de n s u r i n ga l g o r i t h m i cp r o g r a m s t r u s t w o r t h i n e s s t h e r e f o r e ，i t su s e f u la n d v a l u a b l ei np r a c t i c a b i l i t y 2 、ic o m b i n e dt h ei s a b e l l et h e o r e mp r o v e rw i t hp a rm e t h o d p a rp l a t f o r m t h e l i v e r i f i c a t i o no fa l g o r i t h m i cp r o g r a m sd e p e n d su p o nt h ec o r r e c t n e s so fl o o pi n v a r i a n t ， w h i c hd e v e l o p e db yp a rm e t h o d o nt h eo t h e rh a n d ，w i t hi s a b e l l et h e o r e mp o v e r ，i p r o o f e dt h ec o r r e c t n e s so fs o m ek e r n e lc o d e si ng e n e r a t o ro fp a rp l a t f o r m k e yw o r d s ：f o r m a lm e t h o d ，t r u s t w o r t h ys o f t w a r e ，f o r m a lv e r i f i c a t i o n ，t h e o r e m p r o o f , h i g h e ro r d e rl o g i c ，i n t e r a c t i v et h e o r e mp r o v e r a l g o r i t h m i c p r o g r a m ，p a rm e t h o d ，p a rp l a t f o r m 1 1 1 独创性声明 本人声明所呈交的学位论文是本人在导师指导下进行的研究工 作及取得的研究成果。据我所知，除了文中特别加以标注和致谢的 地方外，论文中不包含其他人已经发表或撰写过的研究成果，也不 包含为获得或其他教育机构的学位或证书而使用过的材料。与我一 同工作的同志对本研究所做的任何贡献均已在论文中作了明确的说 明并表示谢意。 学位论文作者签名：签字日期：年月 日 学位论文版权使用授权书 本学位论文作者完全了解江西师范大学研究生院有关保留、使 用学位论文的规定，有权保留并向国家有关部门或机构送交论文的 复印件和磁盘，允许论文被查阅和借阅。本人授权江西师范大学研 究生院可以将学位论文的全部或部分内容编入有关数据库进行检 索，可以采用影印、缩印或扫描等复制手段保存、汇编学位论文。 ( 保密的学位论文在解密后适用本授权书) 学位论文作者签名： 签字日期：年 月 日 导师签名： 签字日期：年月 日 i s a b e l l e 定理证明器的剖析及其在p a r 方法p a r 、平台中的应用 第一章绪论 1 1 研究背景和意义 随着软件系统的规模越来越庞大，复杂程度越来越高，软件出现错误的可能 性及其造成的危害也日益突出。由于软件错误而导致灾难性后果的报道屡见不 鲜，如1 9 9 6 年6 月4 日，由于软件故障造成欧共体的阿里亚娜( a r i a n e ) 5 0 1 垂d 火箭升 空3 7 秒后失事，损失几十亿美元。软件是否可信赖已成为国家经济与国防等系统 能否正常运转的关键因素之一，尤其在一些安全悠关( s a f e t yc r i t i c a l ) 领域更是如 此。于是，开发高可信软件( t r u s t w o r t h ys o f t w a r e ) 迫在眉睫。2 0 0 3 年计算机大师 t o n y h o a r e 提出要在2 1 世纪设计出能验证程序正确的编译器1 1 1 ，美政府在制定 2 0 0 6 年 - 2 0 1 5 年十年美国软件开发发展战略中把高可信软件的开发放在首位。高 可信软件应具备的四个基本属性1 2 j 为：可用行( a v a i l a b i l i t y ) 、可靠性( d e p e n d a b i l i t y ) 、 安全。 生( s a f e t y ) 和防卫。 生( s e c u r i t y ) 。代码本身的正确。l 生( c o r r e c t n e s s ) 是保证以上基本 属性的前提，也是衡量高可信软件的重要指标之一。 传统的软件测试技术能够发现计算机软、硬件系统中存在的某些特定的漏 洞和错误，但是传统测试方法的准确性很大程度依赖测试用例的设计和数量， 它们只能说明在该测试用例下系统是正确的，即“测试只能发现错误，并不能 保证没错误 。因此，计算机专家希望能够找到更有效的方法来保证计算机系统 的正确性和可靠性，于是，形式化方法应运而生。 形式化方法就是运用数学方法表达系统的规约或系统的性质，并且根据数 学理论来证明设计的系统满足相应的规约或具有所期望的性质；它主要包括形 式化规约( f o r m a ls p e c i f i c a t i o n ) 技术和形式化验h t ( f o r m a lv e r i f i c a t i o n ) 技术。形式 化方法是建立在严格的数学基础上的软件开发方法，由于数学理论具有严谨的 逻辑性、规律性和确定性，因此，形式化方法对保证软件的正确性和可靠性具 有十分重要的意义。 形式化验证是在对软件系统进行规约的基础上，分析系统是否具有所期望 的性质。在2 0 0 2 年w i n d o w s 硬件平台工程大会( w i n h e c ) 上，微软总裁b i l l g a t e s 发表的主题演洲3 j 中把“软件验证技术比作是计算机科学的圣杯 。目前比较流 行的形式化验证方法主要分为两类：可达性分析和演绎方法。各种等价性检验、 模型检测属于第一种，定理证明属于第二种。这些形式化验证技术都各有优缺 点，模型检测【4 】的优点是：自动化程度高，当系统不具备所期望的性质时，能 给出相应的反例路径；它的缺点是空间开销大，存在状态爆炸问题，并且已有 硕上学位论文 的模型检测工具只能验证软件设计的正确性，不能与软件的实现关联起来。定 理证明的优点是：能基于无穷域上的归纳法处理无穷状态空间，并且不少定理 证明工具支持代码的自动生成：它的缺点是自动化程度不高，大多数是交互式 的证明过程，需要人工干预，不能在证明失败后给出易于理解的反例。 定理机器证明也称为定理的机械证明或自动定理证明，是人工智能领域中 的一个重要分支，是数学和计算机科学的一门交叉学科。1 9 8 3 年，在美国科罗 拉多州举行了纪念自动定理证明2 5 周年的盛大活动，会上美籍华人数理逻辑学 家王浩先生荣获首届自动定理证明里程碑奖；l w o s 和s w i n k e r 两人荣获自动 定理证明当前研究成就奖。 定理证明器处理问题即是用计算机程序证明某些陈述( s t a t e m e n t ) 或推测 ( c o n j e c t u r e ) 是另外些定理或假设的逻辑结果。定理证明的原理是：首先定义 一种数学逻辑，该逻辑系统实际上是一个形式化的系统，由一系列公理和推理 规则组成；然后我们用这种数学逻辑分别表示被验证系统和其被期望的特性； 所谓定理证明就是从系统的公理出发使用推理规则逐步推导出其所期望的特性 的证明过程。证明所需要的步骤依赖于系统的公理和推理规则，在某种程度上 也依赖于其派生定义和中间引理。与模型检验不同，定理证明可直接处理无限 的状态空间，它使用类似于结构化的推导过程来证明具有无限状态的系统。 按照自动化程度可以将定理证明器分成两类：自动化定理证明器( a u t o m a t i c t h e o r e mp r o v e r ) 和交互式定理证明器( i n t e r a c t i v et h e o r e mp r o v e r ) 。人们最早设计 的定理证明系统是自动化的，这类证明器一般没有类型理论，很难用于验证规 模大的系统。随着应用复杂化，自动化定理证明系统受到了运行时间和空间上 的挑战，于是出现了交互式定理证明系统。 笔者通过对软件形式化验证技术的研究和多种定理证明辅助工具的比较， 选取i s a b e l l e 定理证明器作为验证工具，深入理解i s a b e l l e 定理证明器的系统结 构、类型和理论文件，并进一步剖析其验证方法和工作原理。 算法程序是用可执行程序设计语言或抽象程序设计语言描述的算法。开发 正确且高效的算法程序仍然是计算机科学的最具有挑战性的核心部分。使用定 理证明工具对算法程序进行机械证明是一种发展趋势。文章基于i s a b e l l e 定理证 明器，从验证算法程序的d i j k s t r a 最弱前置谓词法入手，提出了一种对算法程 序进行机械验证的方法。同时，该方法依赖于循环不变式开发的准确性，这里 使用薛锦云教授提出了一种系统的算法程序设计方法p a r 方法【5 ，6 j 开发算 法程序并构造其正确的循环不变式。 本文具有如下科学意义： ( 1 ) 理论意义：形式化方法可以对系统进行严格的规约，并对系统性能进行 不同视角的验证，因此在高可信软件的开发中越来越受重视1 7 ，8 j 。定理机器证明 2 l s a b e h e 定理证明器的剖析及j e 在p a r 方法p a r 甲台中的应用 是计算机科学领域中形式化验证的重要研究课题。本文首先分析形式化验证技 术，了解定理证明器的起源和分类；然后选择其中具有代表性的定理证明器 i s a b e l l e 进行深入的研究，剖析其验证的基本原理和关键技术。 ( 2 ) 实践意义：文章提出了一种使用i s a b e l l e 定理证明器对算法程序进行机 械验证的方法，其优点体现在：采用了数学和逻辑推导来进行验证，它对算 法程序的验证并不像测试方法，形式化验证的准确性并不依赖测试用例，实 现了机械验证替换手工证明过程，克服了传统手工验证过程的繁琐性和易错性 等缺点；验证过程直观和严谨，提高了验证效率并保证了算法程序的高可信。 目前该方法已经被运用于验证了许多算法程序及p a r 平台代码生成系统中的部 分核心代码。 1 2 相关研究情况 定理机器证明是把人们证明定理的一般知识和规则以适当的形式存储到计 算机中，让机器通过运转，自动地证明定理。最初研究的重点是如何让机器来 自动完成数学定理( 如群论) 的证明过程，这些工具通常是基于归结反演的方法， 代表性的例子有o t t e r 、s e t h e o 等工具，它们能连续数日运行并能求解一些非 常困难的定理证明问题。随后，定理证明技术被逐渐地应用于处理与计算机科 学更为相关的问题。 定理证明器是进行形式化验证必不可少的工具。在过去的几十年间，该研 究领域得到了快速的发展，计算机专家们开发了许多定理证明辅助工具，例如， 英国爱丁堡大学数学推理组1 9 j 研究开发的多个交互式的定理证明工具c l a m p r o o fp l a n n e rw i t ho y s t e r 、h o l - c l a m 、l a m b d ac l a m 和i s a p l a n n e r 等；法国国 家计算机科学及控制研究院( i n r i a ) 开发的定理证明器c o q 及图形用户界面支 撑环境p c o q 1 0 】；斯坦福研究院( s r ii n t e r n a t i o n a l ) 研究开发的规约验证系统 p v s 1 1 j ；美国康奈尔大学c o n s t a b l e 教授开发的基于证明程序求精逻辑( p r l ) 的 证明器n u p r l 1 2 l ；波兰华沙大学( s h i n s h uu n i v e r s i t y ) 的a n d r z e jt r y b u l e c 教授组 织的m i z a r 协会开发的m i z a r 系统【1 3 】：在o t t e r m a c e 2 1 1 4 1 基础上发展的 p r o v e r 9 m a c e 4 1 5 j 是关于一阶逻辑和方程式逻辑的自动定理证明器；k a u f m a n n 开发的自动推理工具a c l 2 t 1 6 i 能够验证模型的一些属性；英国剑桥大学开发的 基于高阶逻辑的交互式定理证明器h o l l l 7 】；英国剑桥大学l a w r e n c ec p a u l s o n 和德国慕尼黑技术大学t o b i a sn i p k o w 开发的支持多种逻辑理论的组合证明器 i s a b e l l e l l 8 】。目前，这些定理证明系统在数学定理证明【2 0 】、硬件验证1 2 1 】、协议验 证【2 2 】和软件验证【2 3 】等方面发挥出越来越重要的作用。为了实现自动化，证明工 具应用了许多特殊的算法、数据结构和优化算法来加快归结的效率。 在几何定理机器证明方面，我国处于国际领先地位。在非线性代数方程组研 3 硕士学位论文 究领域，竞争激烈，我国也进入先进行列。主要是因为数学机械化证明的创始者 吴文俊院士在7 0 年代所作的突t 丑- r _ 作，吴文俊方法( 吴法) 【2 4 】的提出给定理机器证 明的研究带来勃勃生机，并于1 9 9 7 年获国际自动推理领域最高奖埃尔布朗 ( h e r b r a n d ) 奖；用吴法可在微机上很快地证明困难的几何定理。周咸青发展了吴 法并把它实现为有效的通用程序，证明了5 1 2 条非平凡定理，写成英文专著【2 5 】； 这一进展是自动推理领域的重大突破，被国际誉为革命性的工作。目前，我国仍 然把几何定理机器证明和非线性代数方程组理论作为主攻方向，同时不断地扩展 机器证明的研究领域范围。 下面分析几种常用的定理证明辅助工具，并讨论其在国内的应用： ( 1 ) m i z a r m i z a r 系统是一个利用计算机进行形式化处理项目的总称，由波兰华沙大 学的a n d r z e jt r y b u l e c 教授组织的m i z a r 协会开发。m i z a r 系统的历史要追溯到 1 9 7 3 年，起始目的是设计一个软件环境来帮助数学家撰写和验证数学论文，随 着m i z a r 系统的发展，数学领域的绝大多数问题都可以是使用m i z a r 来验证。 m i z a r 的特点：除了规约语言和验证工具外，m i z a r 系统具有世界上最大的 可以被计算机检测和处理的数学知识数据库( m m l ) 。m i z a r 系统通过使用m i z a r 语言来定义、计算、推理和证明数学定理，称为m i z a r 文章，并用m i z a r 本身 提供的软件在p c 机上进行验证，通过验证的m i z a r 文章将会被收录到m m l 数 据库中；另外，当我们在撰写新的m i z a r 文章时可以参考m m l 数据库中被收 录的文章【2 6 1 。目前，m m l 数据库己收录9 6 0 多篇文章，7 0 0 0 多个数学概念， 4 0 0 0 0 多条定理1 1 3 】，同时m m l 也是期刊f o r m a l i z e dm a t h e m a t i c s 的o n 1 i n e 版本， 在i n t e r n e t 上可随时查阅。 m i z a r 的证明方式：m i z a r 系统支持两种定理证明方法，一种是使用b y 命 令通过假设或验证过的定理来验证待证定理，另外一种是使用f r o m 命令通过应 用本文章或别的本章中的模式( s c h e m e ) 作为前提来验证待证定理。 m i z a r 的应用：青岛科技大学使用m i z a r 系统对数学领域中的大量问题( 如 四元数的代数结构、布尔代数在广义f u z z y 子代数、广义循环矩阵的性质、函 数微分等) 【2 7 3 1 】进行了验证。 ( 2 ) p v s 原型验证系统p v s ( p r o t o t y p ev e r i f i c a t i o ns y s t e m ) 是由斯坦福研究机构在过 去的2 5 年中开发的基于高阶逻辑的形式化规约和验证的系统，该系统主要包括 规约语言和定理证明两部分，并且集成了预定义定理、类型检测器和多个支持 形式化的工具。 p v s 的特点：p v s 具有丰富的类型系统( 数值类型、枚举类型、元组类型、 4 l s a b e l l e 定理证明器的剖析及其0 ip a r 方法p a r 平台中的应用 记录类型、函数类型、谓词子类型等、) ：其中谓词子类型是p v s 中最具有特色 的一种类型，它允许在已有类型上附加限制条件。例如，已有类型t ，满足限 制条件p ( p 是谓词) 的t 的子类型s u b t 可以定义为s u b t = x ：t i p ( x ) 。使用谓词 子类型的优点是：可以清晰地表达出函数的定义域和值域，进而构造出简单 准确的规约；可以在全函数的逻辑框架内提供部分函数的功能。例如，引入 谓词子类型n o z c r o ：t y p e = x ：r a t i o n a l x = = 0 后，部分函数除法运算( ，在除数为零 时是无定义的) 可定义为如下全函数f r a t i o n a l ，n o z e r o - - - r a t i o n a l 】。 p v s 的证明方式：定理证明主要采用目标制导的方式，其工作原理是：一 个证明的构造从待证定理开始，递进地应用证明器提供的命令进行推理，不断 生成新的子目标，如此反复直至所有的子目标均显然为真。 p v s 的应用：在国内，p v s 的应用范围很广。上海大学计算机学院缪淮扣 教授带领的团队利用p v s 对时序逻辑公式描述的程序性质给予证明【3 2 】，并实现 了定义在时间自动机状态上的时间化分支时序逻辑规约说明的形式体系【3 3 】；上 海交通大学计算机科学与工程系探讨了u m l 状态图和u m l 类图到p v s 规约 的自动转换和验证【3 4 西1 ；基于p v s 西安电子科技大学软件工程研究所对u m l 类图和序列图的一致性进行了检测【3 6 j 。另外，p v s 也被用于到密码协议的形式 化规约和验证例。 ( 3 ) c o q c o q 是法国国家计算机科学及控制研究院( i n r i a ) 开：发的一种基于高阶逻 辑的定理证明工具，其图形用户界面支撑环境p c o q 。c o q 系统主要由两部分组 成：证明开发系统和证明检查器。证明开发系统类似于程序开发系统，其拥有 声明模式和证明模式。在声明模式里，程序员可以像设计程序一样声明变量、 假设、公理；在证明模式旱，程序员可以如同编写程序一样利用已声明的对象 和系统提供的证明策略构造引理或者定理的证明。 c o q 的特点：使用规约语言g a l l i n a 表示程序、程序的属性和这些属性的证 明。除了可以定义函数和谓词、描述数学定理和软件规约之外，c o q 系统的显 著特点是可以把验证过的程序转换成o b j e c tc a m l 、h a s k e l l 和s c h e m e 语言。 c o q 的证明方式：c o q 采用反向推理的方法构造证明，即根据待证明的定 理，选择合适的策略作用于定理，将作为当前目标的该定理划分成若干子目标， 然后再对每个子目标应用合适的策略分别证明；当所有的子目标被证明的时候， 定理证明完毕。 c o q 的应用：中国科学技术大学计算机科学技术系的陈意云教授的学术团队 研究在编译阶段利用c o q 保证程序的正确性，例如：借助形式化证明工具c o q 构 造携带证明代码p c c ( p r o o f - c a r r y i n gc o d e ) 1 3 8 1 ，验证动态存储管理安全【3 9 1 ，设计 出具证明编译器p l c c 矧，pl c c 证明生成器产生的最终输出是c o q 可以接受的程 5 硕七学位论文 序、规范、证明以及一些尚待寻找证明的验证条件。 ( 4 ) n u p r l n u p r l 是美国c o r n e l l 大学计算机科学系r o b e r tl c o n s t a b l e 教授e 1 j o s e p hl b a t e s 教授丌发的证明系统，它的一个重要技术是如何创建和展示证明。 n u p r l 的特点：n u p r l 定理证明工具集成在一个形式化的数字库f d l ( f o r m a l d i g i t a ll i b r a r y ) 中。f d l 是一个包含大部分形式化知识的一个通用数据仓库，它 收集了一些证明系统( 例如c o q ，h o l , i s a b e l l e ，n u p r l ，p v s ) 的形式化的数学知识。 n u p r l 的证明方式：n u p r l 使用自项向下的求精方式进行证明，这种自顶向下 的序列逻辑称为求精逻辑( r l ) 。n u p r l i j e 明过程是对需要证明的目标求精，细划 成一些子目标，子目标还可以进一步地求精细划得到更小的子目标，直到所有的 子目标都能够用基本公理表示或者本身已经是被证明的事实。 n u p r l 的应用：目前国内还没有n u p r l 系统的应用。 ( 5 ) h o l 高阶逻辑系统h o l 的前身是爱丁堡的可计算函数逻辑l c f ( l o g i cf o r c o m p u t a b l ef u n c t i o n ) ，目前支持的逻辑是高阶逻辑。其最突出的优点是用户可 以利用它的元语言m i _ ( m e t al a n g u a g e ) 来编写定理证明程序。 h o l 的特点：一个类型由值的集合和在该集合上定义的运算构成。h o l 系统主要有四种类型：类型变量( t y p ev a r i a b l e s ) ，原子类型( a t o m i ct y p e s ) 、组合 类型( c o m p o u n dt y p e s ) 和函数类型( f u n c t i o nt y p e s ) 。项( t e r m ) 是h o l 系统中的重 要概念，所有出现的任何合法记号都是项，每一个项都有一个类型。h o l 系统 中有四种不同的项：变元、常元、函数应用和l a m b d a 抽象。 ， h o l 的证明方式：h o l 系统使用两种证明方法，前向证明的方法和目标制 导的方法。在大多数的定理证明中采用的证明方式是以目标制导的证明为主， 辅助以前向证明。 h o l 的应用：h o l 系统是最成熟的用于硬件验证的定理证明器之一，在国 内主要使用h o l 系统验证数字硬件1 4 。 ( 6 ) i s a b e l l e i s a b e l l e 定理证明器以交互方式工作，同时又具备高度的自动化水准，琐碎 的证明细节由内部推理机制自动执行，用户仅在关键决策点上控制证明过程。 i s a b e l l e 的特点( 详细参考本文3 2 1 小节) ：与其它定理证明辅助工具不同 的是i s a b e l l e 支持多种对象逻辑，如直觉一阶逻辑i f o l 、基于序列演算的一阶 逻辑l k 、高阶逻辑h o l 和模态逻辑等，这个特点充分体现了i s a b e l l e 的通用 性和灵活性。另外，i s a b e l l e 具有丰富的类型系统、强大的规则库、灵活高效的 命令集和证明过程可读性强等优点。 6 l s a b e l l e 定理证明器的剖析及其在p a r 方法p a r 平台中的应用 l s a b e u e 的证明方式( 详细参考本文3 2 4 小节) ：以h o l 系统类似，i s a b e l l e 既支持前推证明( f o r w a r d sp r o o f ) ，又支持后推证明( b a c k w a r d sp r o o f ) 。前推证明 是从已知定理的假设条件和公理、定理、定义出发推导出新的公式或定理。更 常用的是后推证明，又称为目标制导的证明( g o a l d i r e c t e dp r o o f ) ，它是策略风格 的证明。 i s a b e l l e 的应用：i s a b e l l e 是应用最为广泛的定理证明工具，尤其是在计算 机软、硬件的j 下确性验证以及程序设计语言和协议的验证等领域。兰州大学的 李廉教授的学术团队对i s a b e l l e 的证明环境和策略的设计方面进行研究【4 2 4 引，解 放军理工大学指挥自动化学院使用i s a b e l l e 验证了s a o d v 协议【删、命题演算 形式系统【4 5 j 和电梯控制系统【矧。 1 3 主要研究工作 论文中主要研究工作体现在以下几个方面： ( 1 ) 剖析i s a b e l l e 定理证明器的系统结构、理论、验证原理和核心技术。 ( 2 ) 提出了一种用l s a b e l l e 定理证明器验证使用p a r 方法p a r 平台开发 的算法程序的方法。该方法既克服了传统手工验证过程的繁琐性和易错性等 缺点，又达到“提高验证效率和保证算法程序高可信 的目标，具有很好的 实用价值。 ( 3 ) 使用i s a b e l l e 定理证明器验证p a r 平台生成系统中的部分核心算法。 7 硕l 二学位论文 第二章形式化方法和p a r 方法 形式化方法是为了保证软硬件系统设计的正确性而寻求的一种方法。本章 简单介绍了软件形式化方法的研究内容、分类及其在高可信软件开发中的重要 性；并对p a r 方法及其c a s e 工具p a r 平台进行了概述。 2 1 形式化方法 软件形式化方法，最早可追溯到2 0 世纪5 0 年代后期对程序设计语言编译技术 的研究，即j b a c k u s 提出b n f 描述a l g o l6 0 语言的语法，出现了各种语法分析程 序自动生成器以及语法制导的编译方法，使得编译系统的开发从“手工艺制作方 式 发展成具有牢固理论基础的系统方法。形式化方法的研究高潮始于2 0 世纪6 0 年代后期，针对当时所谓“软件危机 ，人们提出了种种解决方法，归纳起来有 两类：一是采用工程方法来组织和管理软件的开发过程；二是深入探讨程序和程 序开发过程的规律，建立严密的理论，以期能用来指导软件开发实践。前者导致 “软件工程”的出现和发展，后者则推动了“形式化方法的深入研究。 形式化方法有四个主要的源头：从理( a x i o m ) 方法：最早发源于f l o y d 的框 图语义、h o a r e 逻辑和d i j k s t r a 的最弱前置谓词方法；模型( m o d e l ) 方法：起源于 图灵机( t u r i n gm a c h i n e ) 。有限自动机( f i n i t ea u t o m a t a ) 和下推自动机( p u s h d o w n a u t o m a t a ) 都是一种能力受限的图灵机，它们曾在5 0 年代和6 0 年代广泛应用于面 向语法的编译自动化理论。在形式化方法方面，v d m 方法和b 方法的规约语言均 使用了模型的方法，即先定义一个抽象的机器，然后把在这个机器上的操作做为 规约语言；演算( c a l c u l u s ) 方法：起源于c h u r c h 的a 演算，最初的a 演算是无类 型的，后来出现了一些有类型的a 演算。a 演算以函数演算为基础，允许任意高 阶的函数演算，即一个函数的输入和输出都可以是函数；代数( a l g e b r a ) 方法： 起源于抽象数据类型( a b s t r a c td a t at y p e s ) 概念。h o a r e 最早提出把数据类型和它 的实现方法分开的概念，称其为“独立于表示的数据类型 ，l i s k o v 和z i l i e s 正式 把这种数据类型命名为抽象数据类型，并把它运用于程序语言的设计中。抽象数 据类型概念被广泛应用于各种形式化方法中，o b j 和s t a n d a r dm l 等语言均支持抽 象数据类型。 对形式化方法的研究虽已开展了几十年，但至今并无一个精确而统一的定 义。通常认为形式化方法是一种以数学为基础的方法，其数学基础包括逻辑、代 数、自动机、图论等。形式化方法能够清晰、精确、抽象、简明地规范和验证软 件系统及其性质，能够极大地提高软件的安全性和可靠性。 8 l s a b e l l e 定理证明器的剖析及其在p a r 方法撇平台中的应用 2 1 1形式化方法的研究内容 形式化方法用于规范、设计和验证计算机系统，它包括各种语言、技术和工 具等。形式化方法主要研究以下两个方面的内容： ( 1 ) 形式化规约( f o 珊a ls p e c i f i c a t i o n ) 规约是一个描述系统及其特性的过程。形式化规约( 也称形式化规范或形式 化描述) 是对程序“做什么( w h a tt od o ) 的数学描述，用具有精确语义的形式语 言书写的程序功能描述，它是设计和编制程序的出发点，是验证程序是否正确的 依据。通常要讨论形式化规约的一致性( 自身无矛盾) 和完备性( 是否完全、无遗漏 地刻画所要描述的对象、) 等性质。 形式化规约语言( 也称形式化描述语言) 是用于书写形式化规约的语言，它具 有严格数学定义的语法和语义，用于描述系统的特性，如行为特性、时间特性、 性能特性和内部结构等。不同的形式化规约方法使用不同的形式化规约语言，如 代数语言o b j 、c l e a r 、a s l 、a c t o n e t w o 等；进程代数语言c s p 、c c s 、p 演算 等；时序逻辑语言p l t l 、c t l 、x y z e 、u n i t y 、t l a 等。这些规约语言由于 基于不同的数学理论及规约方法，因而也千差万别，但它们有一个共同的特点， 即每种规约语言均由基本成分和构造成分构成。前者用来描述基本( 原子) 规约， 后者把基本规约组合成大规约。构造成分是形式化规约研究和设计的重点，也是 衡量规约语言优劣的主要依据。 ( 2 ) 形式化验证( f o r m a lv e r i f i c a t i o n ) 形式化方法的另一重要研究内容是形式化验证。形式化验证与形式化规约之 间具有紧密的联系( 参考下图2 1 ) ，形式化验证就是验证已有的程序系统p 是否满 足其规约( 前置断言q ，后置断言尺) 的要求。 正确错误? 图2 1 形式规约和形式验证的关系图 传统的验证方法包括模拟( s i m u l a t i o n ) 和测试( t e s t i n 曲，它们都是通过实验的 方法对系统进行查错。模拟和测试分别在系统抽象模型和实际系统上进行，一般 的方法是在系统的某点给予输入，观察在另一点的输出，这些方法花费很大，而 且由于实验所能涵盖的系统行为有限，很难找出所有潜在的错误。为了克服传统 验证方法的局限性，计算机学者们发现可以使用数学方法严格证明一个系统或程 序，于是，出现了形式化验证。 形式化验证比形式规约向前迈进了一步，它对设计的系统进行分析，以便证 明系统具有需要的性质。一般来说，形式化验证方法可以分为等价性检验 9 硕士学位论文 ( e q u i v a l e n c ec h e c k i n g ) 、模型检验( m o d e lc h e c k i n g ) 和定理证明( t h e o r e mp r o v i n g ) 方法。 如何保证和验证软件系统的正确性始终是计算机科学领域中热门研究课题， 吸引了国内外大批计算机科学工作者。j v o