（应用数学专业论文）程序正确性验证的几个问题(1).pdf

湖南大学 学位论文原创性声明 本人郑重声明：所呈交的论文是本人在导师的指导下独立进行研究所 取得的研究成果。除了文中特别加以标注引用的内容外，本论文不包含任 何其他个人或集体已经发表或撰写的成果作品。对本文的研究做出重要贡 献的个人和集体，均已在文中以明确方式标明。本人完全意识到本声明的 法律后果由本人承担。 作者躲蕾洳 蹶洲钏月矽曰 学位论文版权使用授权书 本学位论文作者完全了解学校有关保留、使用学位论文的规定，同意 学校保留并向国家有关部门或机构送交论文的复印件和电子版，允许论文 被查阅和借阅。本人授权湖南大学可以将本学位论文的全部或部分内容编 入有关数据库进行检索，可以采用影印、缩印或扫描等复制手段保存和汇 编本学位论文。 本学位论文属于 l 、保密口，在年解密后适用本授权书。 2 、不保密团。 ( 请在以上相应方框内打“”) 作者签名：协柏 导师签名 日期：够年1 1 月孑日 日期：p 、f 年，月，z 目 插图索引 图1 1 程序的可靠性建模的基本思想 图1 2 软件生存期的模型 图1 3 各种程序验证方法的效率比较 图2 1 静态类型检查的时间效率 图2 2 顺序结构的证明 图2 3 分支结构的证明 图2 4 循环结构的证明 图2 5 例2 2 1 验证示意图 图2 6 例2 2 2 验证示意图 图2 7 循环结构的等价证明 图3 1 a 的共轭格h a s s e 图 图3 2t u r i n g 机的一步计算示意图 图5 1 金融保险系统的类图 图5 2 状态图 图5 3 传统的进出栈f s m 的改进 图5 4 ( a ) 进栈两带状态机 图5 4 ( b ) 出栈两带状态机 图5 5 出栈两带状态机改进图 图5 6 栈操作s t a t e c h a r td i a g r a m 图5 7 m k + 1 叉树 1 1 1 卫_ ，控m m他伸阳弭弛卯弛鲫印印矾甜 程序正确性验证的几个问题 表4 1 四种程序计算模型 表4 2 两类程序设计语言的对比 表5 1 只( 女) 的计算 表格索弓 4 8 4 9 6 5 博上学位论文 摘要 计算机软件的发展受着许多因素的影响，它滞后于硬件，其安全性、可 靠性和稳定性一直是人们关注的几个重要问题。 随着大型软件的快速发展，以及安全性要求极高的航天航空技术的需 要，人们对软件质量的要求起来越高，尤其是对软件的正确性要求，因而出 现了软件的正确性验证与测试两个重要领域。软件的正确性验证讨论的是确 保程序是没有错误的，并且满足用户需求，软件测试则是要找出程序中存在 的错误，两者有着本质的区别，也有着密切的联系，它们贯穿软件的整个生 命周期。人们在不同的领域构造了许多不同的模型，如：可计算函数模型、 谓词演算模型、代数模型等。不同的模型适用于不同的范围，它们在一定的 范围内解决了许多问题，但都存在一定局限性，当然试图用一种模型解决复 杂的软件可靠性问题也是不现实的。程序的实质是有限状态机f s m ，本文将 对几种不同的状态机模型进行讨论，从传统的f s m 到目前流行的 u m l ( u n i f i e dm o d e l i n gl a n g u a g e ) 状态机，并给出一个状态机的矩阵模型，从 而可用纯数学的方法讨论计算机领域中的有关问题，在此基础上，可得到相 应的代数性质，并借助完善的代数理论对计算机领域所关心的代数问题，例 如：可靠性问题、完备性问题及可解性问题等进行讨论；同时，本文也将借 助面向对象的程序设计理论，讨论u m l 语言扩展机制，从设计的源头入手研 究程序的正确性问题。 本文将针对以下几个方面，进行程序正确性的讨论： 1 程序正确性的定义：长期以来，人们对程序的正确性的定义一直未 给出准确的陈述，本文将对此进行必要的讨论，从而可克服长期以来形成的 某些误区。 2 模型的正确性：针对用例、u m l 的状态机进行一些讨论，用例不仅用 于测试，同时也用于建模。用例规模往往很大，使得测试、建模很困难，本 文将对栈的用例规模进行讨论，并得到一个递归推导公式；u m l 的状态机不 同于传统的f s m ，本文试图将两者结合起来用于建模，这样将更利于编制高效 而又可靠的程序。 3 类型与类型系统的正确性：类型系统是算法语言的一个组成部分， 它监视程序中变量的类型，包括所有表达式的类型；类型检验是保证程序正 确性的重要手段。本文将对类别代数中经典的有限基问题进行讨论，从而可 得到具有共轭可置换代数具有有限基的结论：另外利用图灵机的矩阵模型给 程序正确性验证的几个问题 出一个具有可解，但不一致可解字问题的代数；本文还将讨论抽象数据类型 的可靠性与完备性，在此基础上，给出含空类别的类型系统的可靠性定理。 4 算法与程序的正确性：本文将对施用性语言的副作用问题进行讨论， 并得到其副作用是非良性的结论：也对函数式语言，在引入赋值语句后的副 作用问题进行讨论，得到其副作用是良性的结论，另外，对传统的结构化程 序的正确性进行研究，并给出一个一直困扰人们的，关于循环结构的正确性 证明的解决方案。 关键词：形式化验证；统一建模语言；模型检验：函数式语言；副作用；抽 象数据类型；类别代数； 图灵机 博士学位论文 a b s t r a c t t h ed e v e l o p m e n to fc o m p u t e rs o f t w a r ei sa f f e c t e db ym a n yf a c t o r sa n di s d e l a y e dc o m p a r i n gw i t hh a r d w a r e t h es a f e t y ，r e l i a b i l i t ya n ds t a b i l i t yo f s o f t - w a r eh a v eb e e ni m p o r t a n tp r o b l e m sa n da t t r a c t e dp e o p l e sm u c ha t t e n t i o nf o ra l o n gt i m e w i t ht h ef a s td e v e l o p m e n to ft h eh u g es o f t w a r ea sw e l la st h eh i g hs a f e t y d e m a n df r o mh i g ht e c h n i q u es u c ha ss p a c e f l i g h ta n da v i a t i o nd e s i g n ，t h eq u a l i t y o fs o f t w a r e ，e s p e c i a l l yt h ec o r r e c t n e s so fs o f t w a r e ，h a sb e c o m em o r e a n dm o r e i m p o r t a n t t h e r e f o r e ，t h ep r o o fo ft h ec o r r e c t n e s so fs o f t w a r ea n dt h et e s to f s o f t w a r eh a v e b e e na t t r a c t i v er e s e a r c hf i e l d s t h ea i mo fp r o o fo ft h e c o r r e c t n e s so fs o f t w a r ei st oe n s u r et h a tt h e r ei sn oe r r o r si np r o g r a ma n dt o m e e tt h ed e m a n d so ft h eu s e r s o nt h eo t h e rh a n d ，t h ea i mo ft e s to fs o f t w a r ei s t of i n dp o s s i b l ee r r o r si np r o g r a m b o t ha r ec l o s e l yr e l a t e dt ot h ew h o l el i f e c y c l eo fs o f t w a r e h o w e v e r ，t h e ya r ee s s e n t i a l l yd i f f e r e n tw i t he a c ho t h e r t h e r e h a v eb e e nd e v e l o p e dv a r i o u sk i n d so fm o d e l ss u c ha st h ec o m p u t a b l ef u n c t i o n m o d e l ，p r e d i c a t e w o r dc a l c u l u s ，r u r i n gm a c h i n e ，a l g e b r am o d e le t c i nt h e r e l a t e df i e l d s e a c hm o d e lh a si t so n ea d v a n t a g ea n dl i m i t a t i o n i ti sp r a c t i c a l l y i m p o s s i b l et ol i s t 2o n yo n em o d e lt os o l v et h er e l i a b i l i t yp r n b l e m sd u et o i t s c o m p l e x i t 7 t h ec o r eo fap r o g r a mi saf i n i t es t a t em a c h i n e ( f s m ) i nt h i st h e s i s w ed i s c u s ss e v e r a ld e f e r e n tk i n d so ff s mm o d e li n c l u d i n gt h et r a d i t i o nf s ma n d t h ec u r r r e n t l yp o p u l a rs t a t em a c h i n ei nu m i “j n i f l e dm o d e l i n gia n g u a g e ) ，w e p r o p o s eam a t r i xm o d e lo ff s m w et h e nu s ep u r em a t h e m a t i c a lm e t h o da s a t o o lt oa n a l y z er e l a t e dp r o b l e m si nt h ef i e l d so fc o m p u t e ra n dd e r i v er e l a t e d a l g e b r a i cp r o p e r t i e s b yt h eu s eo fc o m p l e t ea l g e b r at h e o r y ，w ed i s c u s sa l g e b r a i c p r o b l e m s c o n c e r n e dw i t h c o m p u t e rt h e o r y t h e s ep r o b l e m s i n c l u d et h e r e l i a b i l i t y ，t h ec o m p l e t e n e s sa n dt h es o l v a b i l i t ye t c m e a n w h i l e ，w i t ht h eh e l po f t h eo b j e c t o r i e n t e dd e s i g nt h e o r y ，w ed is c u s st h ee x t e n s i b i i i t ym e c h a n i s mi n u m ll a n g u a g e i no t h e rw o r d s ，w es t u d yt h er e l i a b i l i t yf r o mt h es o u r c eo f d e s i g n i nt h i st h e s i s ，w es t u d yt h ec o r r e c t n e s so fp r o g r a mf r o mt h ef o l l o w i n g a s p e c t s ： 程序正确性验证的几个问题 】t h ed e f i n i t i o no ft h ec o r r e c t n e s so fp r o g r a m s of a r ，t h e r ei sn o tas t r i c t d e f i n i t i o na b o u tt h ec o r r e c t n e s so fp r o g r a m i nt h i st h e s i s ，w eg i v eas t r i c t d e f i n i t i o na n dp o i n to u ts o m em i s u n d e r s t a n d i n gf o r m e df o ral o n gt i m e 2 t h ec o r r e c t n e s so fm o d e l w ed i s c u s st h eu s ec a s ea n ds t a t em a t h j n eo f 【j m li nt h i st h e s i s u s ec a g ei su s e f u ln o to n l yf o rt e s t i n g 。b u ta l s of o tm o d e l i n g t h ep l o b l e mo fu s ec a s ei sg e n e r a l l yv e r yl a r g e a sar e s u l t ，nb r i n g sd i f f i c t d t y i nt h ec o ns t r u c t i o no ft h em o d e a n dt h et e s to fp r o g r a m w ed i s c u s st h ea n l o u l _ l t o fu s ec a s ea b o u ts t a c k ，a n do b t a i nar e c u r r e n c ef or m u l a t h es t a t em a c h i n ei n u m li sd i f f e r e n tf r o mt h et r a d i t i o n a lf s m i nt h i st h e s is v v ee s t a b l i s ham o d e l t h a tc o n h i n e st h es t a t c c h a r td i a g t a mw i t ht r a d i t i o n a lf s m i td r o v i d es a c o n v e n i e n tt o o lt oc o d ee f f i c i e n ta n dr e l i a b l ep r o g r a m s 3 t y p e ss y s t e ma n dc o r r e c t n e s so ft y p e ss y s t e m t y p e ss y s t e m isp a r to f p r o g r a ml a n g u a g e i tf o l l o wt h et r a c k st y p eo ft h ev a r i a b l e si n c l u d i n gt y p e so f e x p r e s s i o n s ，c h e c k i n go ft y p ec o u l de n s u r et h ec o r r e c t n e s s o fp r o g r a m w e a n a l y z e f i n i l eb a s e si nc l a s s i c a l g e b r a a n do b t a i nac o n c l u s i o nt h a t c o n g r u e n c e p e r m u t a b l ea l g e b r av a r i e t i e sh a sf i n i t ee q u a t i o nb a s e s b ym e a n s o fm a t r i xm o d e lf o rt u r i n gm a c h i n e ，w ed e r i v ea na l g e b r at h a tp o s s e s e ss o l v a b l e w o r dp r o b l e m sb u tn o t r e c u r s i v e l ys o l v a b l e w o r dp r o b l e m s w e s t u d yt h e s o u n d n e s sa n dc o m p l e m e n to ft h et y p e ss y s t e m ，i na d d i t i o n ，w ee s t a b l i s ha t h e o r e mf o rt h et y p e ss y s t e mt ob es o u n d n e s s 4 c o r r e c t n e s so fp r o g r a m sl a n g u a g ea n dt h ea l g o r i t h m s w es t u d y c o r r e c t n e s so fp r o g r a ml a n g u a g ea n dg i v eaw a yt os o l v et h ec o r r e c t n e s so ft h e c y c l es t r u c t u r ep r o g r a m a f t e rg i v i n gt h eg o o ds i d ee f f e c ti d e aw eg e tt h er e s u l t s t h a ts i d ee f f e c to fa p p l i c a t i v el a n g u a g ei sn o tg o o da n dt h a t s i d ee f f e c to f i m p e r a t i v el a n g u a g ea f t e ra d d i n ga s s i g ns e n t e n c ei sg o o d k e y w o r d s ：f o r m a lv e r i f i c a t i o n ；u n i f i e dm o d e l i n gl a n g u a g e ；m o d e lc h e c k i n g ；f u n c t i o n a ll a n g u a g e ；s i d ee f f e c t ；a b s t r u c td a t at y p e ；t y p e sa l g e b r a ； t u r i n gm a c h i n e 博士学位论文 1 1 研究背景 第1 章绪论 计算机软件的发展受着许多因素的影响，它滞后于硬件。软件的重用和自动生 成及其安全性、可靠性和稳定性一直是人们关注的几个重要问题。2 0 世纪6 0 年代 末期，以i b m 3 6 0 机的操作系统为标志，出现了软件危机1 2 7 ，使得计算机理论及 相关研究发生了根本的变化，相应地产生了软件工程，程序设计方法学等理论研究， 其中关于程序的正确性验证和测试就是一个研究热点。自上世纪7 0 年代中期以来， 形成了软件生存期概念，软件产业的发展经历了三个不同的阶段。第一阶段是7 0 年代中期至9 0 年代中期的软件结构化生产阶段，该阶段是以结构化分析与设计、 结构化评审、结构化程序设计以及结构化测试为特征。从8 0 年代中期开始，软件 生产开始进入以过程为中心的第二阶段，以个体软件过程p s p ( p e r s o n a ls o f t w a r e p r o c e s s ) 、过程成熟度模型c m m ( c a p a b l i t ym a t u r i t ym o d e l ) 和群组软件过程 t s p ( t e a ms o f t w a r ep r o c e s s ) t l 】为标志，这个阶段将在近期结束。而从1 9 9 5 年开始， 国际上已经逐步进入以软件过程、面向对象和构件重用等三项技术为基础的软件工 业化生产的第三阶段。我国一些先进的软件公司也已经开始从第二阶段过渡到第三 阶段。 目前，我国的软件开发行业大部分还处于软件结构化生产阶段，刚刚开始向以 过程为中心的第二阶段过渡，这也就是说，我国的大部分软件开发组织的过程能力 成熟度还有待于进一步提高和改进，这主要表现在： 第一、相当多的软件开发单位对软件开发的过程管理不规范，所生产的软件系 统质量达不到客户方的要求，容易产生因质量问题所引起的软件危机，软件开发中 还存在比较大的潜在风险。 第二、软件开发单位的开发过程混乱而无序，只重视先进技术在软件开发中的 作用，忽视了软件开发过程对于软件质量的影响。开发过程的不标准性既不利于组 织自身软件过程能力的提高，同时也妨碍了软件开发组织与国际先进开发管理规范 的接轨。 第三、各软件开发单位在软件产品的开发中不遵循软件工程的要求，软件开发 过程能力的不成熟，不利于软件项目开发中做出正确的决策。并且，客户方对软件 开发组织的开发过程也不能进行很好地监控1 5 j 。 为了解决以上问题，在软件的开发过程中，人们通过对实际问题进行分析，将 问题形式或半形式的转换成程序要求和说明，再将其转换成程序，因此可以说程序 程序正确性验证的几个问题 的诈确性，不仪是对源程序进行正确性验证，而且要对开发前期的各个阶段进行正 确性进行验证。目前，软件的测试及i f 确性验汪在国外开展得比较普及，在美国以 a t & tb e l l 实验室为中一心的研究机构，对软件的可靠性研究已比较深入，在欧洲， 对软件的正确性验证以大学和研究机构为主体，在国内，也己开展了对软件的可靠 性研究，部分高校对形式化工程及u m l 进行了研究，大部分研究还基本停留软件 测试层面，而对软件的诈确性验证只是局部得到了展开。 1 2 程序正确性验证概述 随着大型软件的快速发展以及安全性要求极高的航天航空技术的需要，对软 件的质量的要求也越来越高，特别对软件的可靠性要求越来越高，因而出现了软件 的正确性验证与测试两个重要领域 3 - 7 。它们贯穿软件的整个生命周期，相应产生 了许多不同的模型 9 1 。日前，计算机硬件发展相对比较成熟，而软件发展滞后，主 要原因是没有一套适合软件工业化的标准，使之稳步、健康、快速发展。 程序的可靠性定义的三个要素为：失效( f a i l u r e ) 、叫间( t i m e ) 和操作环境 o p e r a t i o n a le n v i r o n m e n t ) ，图1 】给出厂程序的可靠性建模的基本思想6 ”。保证程 序的可靠性有很多方法，主要分为测试与验证，测试的方法有许多，相应模型有上 百种，程序的正确性验证在软件的不同生存周期中采用不同的方法。 失效率f 出现失效 指定目标 试时间t 出现时间 计划完成时闯 图1 1 程序的可靠性建模的基本思想 软件的应用开发可以被划分为：需求调研、系统分析、系统设计、编码实现、 系统测试和系统维护等六个阶段。 除测试和维护以外的其他四个开发阶段的关系和顺序如图12 所示，图形的顶 层是第一阶段一一需求调研，这一阶段主要通过调研获取需求。图形的中层是第二 阶段一系统分析，这阶段主要通过用例分析、对象建模和界面设计等构建分析 模型( a n a l y s i sm o d e l ) 。该阶段的主要成果是对象模型( o b j e c tm o d e l ) 和动态模 博士学位论文 型( d y n a m i cm o d e l ) ，c r c ( c l a s sr e s p o n s i b i l i t yc o l l a b o r a t o r ) 卡在这一阶段中起着 校正对象模型和动态模型的作用。 图1 2 软件生存期的模型 对象分析之后，很自然的便是第三阶段一系统设计，这一阶段的主要工作是 将分析对象模型中的类映射到应用类，构建服务类和关系类，设计用户界面和数据 库结构。该阶段的主要成果是视图( v i e w ) 、模型( m o d e l ) 、关系数据库( r e l a t i o n a l d a t a b a s e ) ，它们恰好对应着三层结构的客户端、业务服务层和数据库服务层。图 形的最后一行文字代表着第四阶段一一系统实现，这一阶段通过编程建立实现模 型( i m p l e m e n t a t i o nm o d e l ) 。 在第四阶段中程序正确性验证，前人已有许多工作3 1 ，并且大部分都比较成 熟，这方面的工作大致可分为两种，其中一种是静态检验，另外一种是动态检验。 静态检验有程序结构和数据类型的检验。动态检验有编译程序的自动检验，也包括 程序测试等方法。不同的方法有不同的适应范围，其效果也各有不同，软件的正确 性验证讨论的是确保程序是没有错误的，软件测试则是要找出程序中存在的错误。 各种方法的效率比较见图1 3 。 图1 3 各种程序验证方法的效率比较 蓦器 程序正确性验证的几个问题 静态类型检查是防止引入错误和进行错误检测的强大武器库中的重要武器之 。通过早期错误检测一一静态类型检查，提高健壮性，通过在最佳的时候作所需 的检查， 程序的正确性验证越来越受到重视，研究的方法也越来越多5 卜川，3 5 。4 ”，本文研 究的是程序的i e 确性验证中的几个富有特色的问题，首先，讨论程序的正确性的概 念，然后，介绍几个常用的方法，最后给出本文的几点工作。 “正确”的含义在通常的用法中有很大的差别，大体可分为以下四个层次：程 序不含语法错误；程序对于几组输入数据能够得出满足规格说明要求的结果； 程序对于精心选择的典型、苛刻而带有刁难性的几组数据能够得出满足规格晚明要 求的结果：程序对一切合法的输入数据都能产生满足规格说明要求的结果。第一 条讨论语法问题，当然，包括相应文档的语法问题，后三条讨论的是语义问题。其 中二、三条讨论的是程序的测试问题，第四条属于程序的正确性验证的范畴。 任何语言均包括语法、语义和语用三个方面，计算机软件是计算机系统中程序 及其有关文档。计算机软件语言是用以描述软件、软件开发过程中间结果，以及软 件开发过程本身。计算机语言又分为需求级语言、功能级语言、设计级语言以及实 现级语言【8 1 。并且就其级别而论，由低抽象语言向高抽象级语言发展，由顺序语言 向并发语言发展，由单机语言向网络语言发展，各级语言各有相应的语法规则，其 文法的正确性基本上可由计算机自动验证得以保证，其数据结构以及算法的正确性 仍有许多可以研究的l ”o “。 语义有外部语义和内部语义之分，内部语义的正确性是指逻辑匕内在的一致性 和完整性。 软件的正确性有可跟踪性、完备性及致性三大属性。对软件的正确性验证可 用验证和测试的方法，包括对文档、模型、算法以及代码的验证。 为了对程序进行i f 确性验证，首先要对程序的正确性给予准确的定义。m c c a l l 等给出的定义如下： 在预定环境下l ，软件满足设计规格说明及用户预期目标的程序。它要求软件没 有错误。 显然这个定义0 i 能完全满足人们的需求，因为往往环境在变化，而且，规格说 明自身是否l e 确? 用户的预期目标是否存在定量标准? 这些都需要讨论，基于诸 多原因，本文对程序的i i _ = 确性的定义进行了讨沦。 长期以来，程序的j e 确验证的方法，直未引起工业界的重视，人们宁愿用测 试的方法，也不愿用证明的方法。一方面，证明所用的理论艰涩难懂；另一方面， 未给出【f 确性一个准确t 形式化) 的定义。逻辑理论艰涩难懂，证明过程冗长繁锁， 有时它比源代码还要长。 自统一建模浯占问世以来，证明难确性方法又引起了人们的重视，重要原因为 博士学位论文 该语言重视程序正确性的三个基本属性：可跟踪，一致性和完备性6 4 1 ”。 目前，利用u m l 文法对模型的正确性进行检验，广泛为学术界和工业界所接 受，一方面是因为其高度的可视化；另一方面，它解决了长期以来困扰人们的难 题，从问题的源头抓起，从工程或项目的设计阶段开始就进行其正确性检验 2 4 , 4 3 - 4 5 】， 就如同建筑工程一样，从设计阶段开始，设计人员用客户和编程人员都乐意接受的 语言，设计出一个完美无缺的模型，剩下的事情就好办了。 总之，程序的正确性验证是软件可靠性工程中一个重要课题，有着广阔的前景， 需要广大理论工作者付出巨大的努力、艰辛的工作，同时，也需要广大实践工作者 在软件开发的各个阶段付诸实施。目前，从事程序正确性验证的人员越来越多，加 之有已为工程接受的u m l 建模语言，我们坚信这领域会有个飞速的发展。 1 3 本文的一些结果与创新点 本文在充分地讨论程序的正确性的概念之后，给出了结构化程序的正确性证 明，另外，在充分考虑软件的生存周期中，各个阶段的特点后，指出了各个阶段的 程序正确性验证的必要性，克服了长期以来困绕着人们的一些误区。第一，正确性 验证不应仅局限源代码的正确性验证，而应从设计阶段就加以充分地考虑，据统计 程序的错误中，功能错误占2 7 ，系统错误占1 6 ，而编码错误占1 4 ：第二， 以往程序的正确性验证方法与数据类型联系不紧密，试图从一组公理出发，推演出 所有真理，这当然是十分困难。为此，需要寻找描述抽象数据类型的方法一这就 是代数方法 4 7 - 5 0 , 5 5 - 6 3 】。 根据规格说明书和程序，构造出一个抽象数据类型a = ( s ，e ) ，s 表类型的有 限集合，表示其操作的有限集合，占表示等式公理集，由此推演出一系列的性质 ( 代表程序所期望的性质) 。 另外，视程序为一个有限状态机，将程序转换成状态机，根据其扩展状态图， 利用u m l 的静态语义和动态语义【6 8 。7 ”，描述一个类的实例对接受到的事件所发生 的反应，进而对其正确性进行验证。 归纳起来，主要有以下几个方面： 1 3 1 程序的正确性的定义 为了讨论程序的正确性，将指定框图程序和拟a l g o l 程序为程序的描述形 式。程序变量分为三种类型： 输入向量量= ( x ，x ：，x 。) ，由给定的输入值组成； 程序向量萝= ( y ，y ：，y 。) ，计算过程中，用作暂时存储的工作单元； 输出向量j = ( 互，z ，z c ) ，计算终止时产生的输出值。 另外，变量的取值域也分为三种类型：输入域d 。，和程序域d ，和输出域d 。 程序正确性验证的几个问题 每个域都是些子域的筲夤儿积，比如d 。= d 。d 。：d 。 程序的语句分为四种类型： s t a r t 语句，即开始语句； a s s i g n 语句歹= g ( i ，歹) 或= f ( z q ，其中g ( 亍，夕) ，厂( i ) 是把d 。d ，d 。映射到d ，的完 全函数： l e s t 语句r ( i ，歹) ，其中，( 孟，歹) 是d ，d ，上的全谓词，它取真，f ( t r u e ) 或假f ( f a l s e ) 为值； h a l t 语句，即终l = 语上j ， 框图程序就是由这些语句( 只加一个s t a r t 语句后) 组成的流程图，其中每一 a s s i g n m e n t 语句或t e s t 语句，都在从s t a r t 语句到某h a l t 语句的路径上，换句话说， 框图程序不允许含有“死循环的”t e s t 语句。 框图程序的验证依赖于两个给定的谓词： ( 1 ) d 。上的全谓词妒( j ) ，称为输入谓词，它描述了d ，中，可作为输入元素的 性质： ( 2 ) d 。d ：上的全谓词叭j ，歹) ，它描述了程序执行终止时，输入变量和输出变 量之问必须满足的关系。 在此基础上，讨论了程序正确性的概念。 1 3 2 正确性的证明方法 程序正确性证明( p r o o f o f p r o g r a m m i n gc o r r e c t n e s s ) ，是通过数学证职来验证 程序正确性的一种方法，确认( v a l i d a t i o n ) 与验证( v e r i f i c a t i o n )一样都是软件工 程中尚不f 分明确的术语，我们在本文作。些讨论。 程序的测试( t e s t ) 和验证是用来说明程序正确与否的两种常用的方法，两者 密不可分，相辅相成，但两者之间存在本质的区别。 验证是通过数学证明来验证程序正确性的一个方法，它要求对没有错误的程序 能证明其正确性，而对于有错误的程序，则能指出其错误所在。 在软件1 ：程中，程序l f 确性验证，即先定义若干断言，而后利用这些断言达到 验证程序正确性 6 ) 。 通过某种手段确认、“个已完成的程序及数据符合某些具体的要求，这包括软件 要求和软件规格说明书。 确认与验证有联系+ 也有明显的差别，确认指如何决定最后的软件产品是否正 确无误，而验证指如何决定软件开发的每个阶段，每个步骤的产品是否正确无误， 并且与前面的开发阶段和开发步骤的产品相一致。 13 21 算法设计语言程序的证明 软件语言可分为需求级，功能级，设计级和实现级语言，在这一节，讨论实现级 6 博士学位论文 语言，即算法设计语言的正确性。 最早期提出程序正确性的证明方法是f l o y d j ，采用不变式断言法。 f l o y d 不变式断言法，是将程序流程中分割成若干断点，开始时，设立一个断 点，终止时设立一个断点，而每一循环的公共点设一个断点，每处附加一个断言。 程序p 的切割点集为s ，如果对于s 中每个切割点i ，从s t a r t 到点i 的路径上所有 切割点都属于s ，则称切割点集s 称为完全的。 本文就三种结构的结构化程序给出了正确性证明，特别是对长期困扰人们的循 环结构加以讨论，并给出一个解决方案“。 1 3 2 2 程序设计语言的副作用问题 函数式程序设计的概念和表处理，在人工智能领域广泛使用，函数式语言的最 大特点是引用透明，无副作用，一旦引入赋值语句，那么它将失去这一特性【2 9 32 1 ， 同样，由于命令式语言有赋值语句，因而它有副作用问题。 由于副作用的问题给程序正确性验证带来了困难，为此，作者在文1 3 2 1 中对各 种程序的副作用做了一定的讨论，文中，作者首先给出了良性副作用的概念，并证 明了命令式语言的副作用问题是非良性的，而函数式语言在引入赋值语句后，其副 作用是良性的。 1 3 2 3 类别代数与等式理论 将数据与其操作分离，试图用一组公理建立一个系统，以此来证明程序的正确 性，这是以往程序正确性证明的方法，这当然十分困难。建立在类别代数理论基础 上的抽象数据类型理论克服了这一困难，类别代数理论已构成一个系统，对提高软 件重复使用能力和软件生产能力极为重要，但仍存许多问题值得探讨。 1 有穷可公理化问题 一个类别代数是一个三元组：a = ( s ，e ，e ) ，其中s 表值集，表示在s 上的操 作，e 表示中所定义的操作应满足的条件的等式集合( 称之为公理) 。 设v 是变量的可数集合，t ( ，v ) 是项的有限集合，e 是一个给定的等式集合， e 是由e 经使用反身、对称、传递、等量替换和实例说明作为推理规则，进行有 限证明得到的集合，e + 称之为由e 表示的等式理论，记为t h ( v ) ，v 是变量的可数 集合。t h e ( v ) 何时是有穷公理化的? 这是一个古老的问题，目前又重新被计算机理 论工作者所重视。 给定代数a 和变量的有限集合v ，映射o r ：v 专a 称为a 赋值，如果t t ( ，v ) ， v a r ( t ) 表示项t 中变量出现的集合，称a ：v a r ( t ) - - ) a 为对于项t 的a 赋值。 s , t t ( ，v ) ，s = t 是一等式，当且仅当对任一a 一赋值a ：v a r ( s ) uv a r ( t ) 一 a 有 q ( s ) = 伍( t ) ，就说s = t 是在a 中被验证的，记为afs = t 。 a e 当且仅当s = t e 等a b = t 。 7 程序正确性验证的几个问题 作者在这里证明了：当a 是一个具有共轭可置换，且是有限次直不司约的，那 么它有有限基 37 , 3 8 , 6 2 1 。 2 具有穷公理且有递归可解字问题 在文 3 9 1 中，构造了个有限基的簇( 称之为拟递归簇) 其方程理论是不可挟 定的，但其字问题是递归可解的，它是解决了g m c n u l t y ( 1 9 9 2 ) 陈述的问题4 ”， 同时也极大地简化了d e j a n d e i c ( 2 0 0 0 ) 的构造方式 4 8 1 。其结果是b w e l l sf 1 9 8 2 ) 与 a m e k l e f n e l s o n 和ss h e l a h ( 1 9 9 3 ) 4 9 j 的结论的般化。 3 可靠性与完备性问题 可靠性与完备性是抽象数据类型系统的一对孪生兄弟，所谓可靠性是指抽象数 据类型的每个模型满足的定理m e ( 即m e = p j p ) 是否能由公理p e ( 即 p e = p lp ) 推出( 这罩m e 、p e 仅表示一个集合，以下类似) 而完备性是指由 公理推出的定理能否被它满足。 在一个证明系统p s - 中，令m e 为d 的每个模型都能满足的那些公式 的集合，若p e g m e ，则称p e 是可靠的，反之若m e p e ，则称p e 是完备的。 在齐性代数中每个抽象数据类型的完备系统是可靠的，并且存在一个完备的证 明系统。但是在非齐性代数中则不一定，我们介绍了一个这样的例子。那么究竟什 么系统才能具有这样的性质呢? 文献【53 1 ”。9 3 1 介绍了一个完备而有可靠的系统 p c f ( p a s s a b l ec o u n t a b l ef u n c t i o n ) 。b i r k h o f f 给出了等式逻辑的完备性的证明，本文 给出了多类别等式逻辑的可靠性的一个条件【8 ”。 1324u m l ( u n i f i e dm o d e l i n gl a n g u a g e ) 1 模型验证( m o d e l c h e c k i n g 、 面向对象技术具有许多特色：一是方法的唯性，二是高度连续性，三是把 o o a ( o b j e c t 。o r i e n t e da n a l y s i s ) 、o o d ( o b j e c t o r i e n t e dd e s i g n ) 、o o p ( o b j e c t o r i e n t e d p r o g r a m m i n g ) 集成到生存期的各个阶段。 u m l 是一种用于对软件密度型系统进行可视化、详述、构造和文档化的建模 语言，主要适用丁| 分析与设计阶段的系统建模，目前为工业界广泛莺视。 u m l 包括概念的语义、表示法和说明，提供了静态、动态、系统环境及组织 结构的模型，它可被交互的可视化建模工具所支持，这些工具提供了代码生成器和 报表生成器。 u m l 是。种半形式化的语言，因此对它建立的模型进行进一步的检验是必要 的，这里作者就以下两方面进行了研究： 1 基于用例规模的讨论【5 l 】 用例模型用于需求分析阶段，首先，它描述了待开发系统的功能需求；其次， 它将系统看作黑盒，从外部执行者的角度来理解系统；第三，它驱动了需求分析之 后各阶段的丌发工作，不仅存开发过程中保证了系统所有功能的实现，而且被用_ 丁 博士学位论文 验证和检验所开发的系统。用例从本质上讲，是用户或其它系统与被设计系统之间， 为了获取某种目标的一次典型交互作用。本文对栈的用例规模进行了讨论，并得到 了一个递归推导公式。 2 基于动态机制的模型检验 状态机是展示状态与状态转换的图，通常一个状态机依附于一个类，并且描述 一个类的实例对接受到的事件所发生的反应。状态机也可依附于操作、用例、和协 作，并描述它们的执行过程，本文结合传统的状态机，构造了u m l 的一个状态机 模型，并对其正确性加以了证明。 1 4 论文的结构 有人曾经给出了一个关于程序的公式： 程序= 算法+ 数据结构。 尽管这一提法具有一定的片面性，但也基本反映了程序的特征，因此，讨论程 序的正确性，就是讨论算法及数据和相应的操作的正确性，当然，还有建立模型及 其正确性，关于算法的正确性在此不准备作深入地讨论，本文，主要讨论数据和相 应的操作的正确性。 第2 章，讨论静态数据分析和三种结构的程序的正确性；