计算机软件的发展受着许多因素的影响,它滞后于硬件,其安全性、可靠性和稳定性一直是人们关注的几个重要问题。 随着大型软件的快速发展,以及安全性要求极高的航天航空技术的需要,人们对软件质量的要求起来越高,尤其是对软件的正确性要求,因而出现了软件的正确性验证与测试两个重要领域。软件的正确性验证讨论的是确保程序是没有错误的,并且满足用户需求,软件测试则是要找出程序中存在的错误,两者有着本质的区别,也有着密切的联系,它们贯穿软件的整个生命周期。人们在不同的领域构造了许多不同的模型,如:可计算函数模型、谓词演算模型、代数模型等。不同的模型适用于不同的范围,它们在一定的范围内解决了许多问题,但都存在一定局限性,当然试图用一种模型解决复杂的软件可靠性问题也是不现实的。程序的实质是有限状态机FSM,本文将对几种不同的状态机模型进行讨论,从传统的FSM到目前流行的UML(Unifled Modeling Language)状态机,并给出一个状态机的矩阵模型,从而可用纯数学的方法讨论计算机领域中的有关问题,在此基础上,可得到相应的代数性质,并借助完善的代数理论对计算机领域所关心的代数问题,例如:可靠性问题、完备性问题及可解性问题等进行讨论;同时,本文也将借助面向对象的程序设计理论,讨论UML语言扩展机制,从设计的源头入手研究程序的正确性问题。 本文将针对以下几个方面,进行程序正确性的讨论: 1.程序正确性的定义:长期以来,人们对程序的正确性的定义一直未给出准确的陈述,本文将对此进行必要的讨论,从而可克服长期以来形成的某些误区。 2.模型的正确性:针对用例、UML的状态机进行一些讨论,用例不仅用于测试,同时也用于建模。用例规模往往很大,使得测试、建模很困难,本文将对栈的用例规模进行讨论,并得到一个递归推导公式;UML的状态机不同于传统的FSM,本文试图将两者结合起来用于建模,这样将更利于编制高效而又可靠的程序。 3.类型与类型系统的正确性:类型系统是算法语言的一个组成部分,它监视程序中变量的类型,包括所有表达式的类型;类型检验是保证程序正确性的重要手段。本文将对类别代数中经典的有限基问题进行讨论,从而可得到具有共轭可置换代数具有有限基的结论;另外利用图灵机的矩阵模型给