程序正确性验证的几个问题

《程序正确性验证的几个问题》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、湖南大学博士学位论文程序正确性验证的几个问题姓名：范年柏申请学位级别：博士专业：应用数学指导教师：周叔子;张大方20051020博士学位论文摘要计算机软件的发展受着许多因素的影响，它滞后于硬件，其安全性、可靠性和稳定性一直是人们关注的几个重要问题。随着大型软件的快速发展，以及安全性要求极高的航天航空技术的需要，人们对软件质量的要求起来越高，尤其是对软件的正确性要求，因而出现了软件的正确性验证与测试两个重要领域。软件的正确性验证讨论的是确保程序是没有错误的，并且满足用户需求，软件测试则是要找出程序中存在的错误，两者有着本质的区别，也有着密切的联系，它们贯穿软件

2、的整个生命周期。人们在不同的领域构造了许多不同的模型，如：可计算函数模型、谓词演算模型、代数模型等。不同的模型适用于不同的范围，它们在一定的范围内解决了许多问题，但都存在一定局限性，当然试图用一种模型解决复杂的软件可靠性问题也是不现实的。程序的实质是有限状态机FSM，本文将对几种不同的状态机模型进行讨论，从传统的FSM到目前流行的UML(UnifiedModelingLanguage)状态机，并给出一个状态机的矩阵模型，从而可用纯数学的方法讨论计算机领域中的有关问题，在此基础上，可得到相应的代数性质，并借助完善的代数理论对计算机领域所关心的代数问题,例如：可

3、靠性问题、完备性问题及可解性问题等进行讨论；同时，本文也将借助面向对象的程序设计理论，讨论UML语言扩展机制，从设计的源头入手研究程序的正确性问题。本文将针对以下几个方面，进行程序正确性的讨论：1.程序正确性的定义：长期以来，人们对程序的正确性的定义一直未给出准确的陈述，本文将对此进行必要的讨论，从而可克服长期以来形成的某些误区。2．模型的正确性：针对用例、UML的状态机进行一些讨论，用例不仅用于测试，同时也用于建模。用例规模往往很大，使得测试、建模很困难，本文将对栈的用例规模进行讨论，并得到一个递归推导公式；UML的状态机不同于传统的FSM,本文试图将两者

4、结合起来用于建模，这样将更利于编制高效而又可靠的程序。3．类型与类型系统的正确性：类型系统是算法语言的一个组成部分，它监视程序中变量的类型，包括所有表达式的类型；类型检验是保证程序正确性的重要手段。本文将对类别代数中经典的有限基问题进行讨论，从而可得到具有共轭可置换代数具有有限基的结论；另外利用图灵机的矩阵模型给i程序正确性验证的几个问题出一个具有可解,但不一致可解字问题的代数；本文还将讨论抽象数据类型的可靠性与完备性，在此基础上,给出含空类别的类型系统的可靠性定理。4．算法与程序的正确性：本文将对施用性语言的副作用问题进行讨论，并得到其副作用是非良性的结论

5、;也对函数式语言，在引入赋值语句后的副作用问题进行讨论，得到其副作用是良性的结论，另外，对传统的结构化程序的正确性进行研究，并给出一个一直困扰人们的,关于循环结构的正确性证明的解决方案。关键词：形式化验证；统一建模语言；模型检验；函数式语言；副作用；抽象数据类型；类别代数；图灵机ii博士学位论文AbstractThedevelopmentofcomputersoftwareisaffectedbymanyfactorsandisdelayedcomparingwithhardware.Thesafety,reliabilityandstabilityofso

6、ft-warehavebeenimportantproblemsandattractedpeople’smuchattentionforalongtime.Withthefastdevelopmentofthehugesoftwareaswellasthehighsafetydemandfromhightechniquesuchasspaceflightandaviationdesign,thequalityofsoftware,especiallythecorrectnessofsoftware,hasbecomemoreandmoreimportant.

7、Therefore,theproofofthecorrectnessofsoftwareandthetestofsoftwarehavebeenattractiveresearchfields.Theaimofproofofthecorrectnessofsoftwareistoensurethatthereisnoerrorsinprogramandtomeetthedemandsoftheusers.Ontheotherhand,theaimoftestofsoftwareistofindpossibleerrorsinprogram.Botharecl

8、oselyrelatedtothewholelife