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

湖南大学
博士学位论文
程序正确性验证的几个问题
姓名:范年柏
申请学位级别:博士
专业:应用数学
指导教师:周叔子;张大方
20051020
博士学位论文
摘要
计算机软件的发展受着许多因素的影响,它滞后于硬件,其安全性、可
靠性和稳定性一直是人们关注的几个重要问题。
随着大型软件的快速发展, 以及安全性要求极高的航天航空技术的需
要,人们对软件质量的要求起来越高,尤其是对软件的正确性要求,因而出
现了软件的正确性验证与测试两个重要领域。软件的正确性验证讨论的是确
保程序是没有错误的,并且满足用户需求,软件测试则是要找出程序中存在
的错误,两者有着本质的区别,也有着密切的联系,它们贯穿软件的整个生
命周期。人们在不同的领域构造了许多不同的模型,如:可计算函数模型、
谓词演算模型、代数模型等。不同的模型适用于不同的范围,它们在一定的
范围内解决了许多问题,但都存在一定局限性,当然试图用一种模型解决复
杂的软件可靠性问题也是不现实的。程序的实质是有限状态机 FSM,本文将
对几种不同的状态机模型进行讨论, 从传统的 FSM 到目前流行的
UML(Unified Modeling Language)状态机,并给出一个状态机的矩阵模型,从
而可用纯数学的方法讨论计算机领域中的有关问题,在此基础上,可得到相
应的代数性质,并借助完善的代数理论对计算机领域所关心的代数问题, 例
如:可靠性问题、完备性问题及可解性问题等进行讨论;同时,本文也将借
助面向对象的程序设计理论,讨论 UML 语言扩展机制,从设计的源头入手研
究程序的正确性问题。
本文将针对以下几个方面,进行程序正确性的讨论:
程序正确性的定义:长期以来,人们对程序的正确性的定义一直未
给出准确的陈述,本文将对此进行必要的讨论,从而可克服长期以来形成的
某些误区。
:针对用例、UML 的状态机进行一些讨论,用例不仅用
于测试,同时也用于建模。用例规模往往很大,使得测试、建模很困难,本
文将对栈的用例规模进行讨论,并得到一个递归推导公式;UML 的状态机不
同于传统的 FSM, 本文试图将两者结合起来用于建模,这样将更利于编制高效
而又可靠的程序。
:类型系统是算法语言的一个组成部分,
它监视程序中变量的类型,包括所有表达式的类型;类型检验是保证程序正
确性的重要手段。本文将对类别代数中经典的有限基问题进行讨论,从而可
得到具有共轭可置换代数具有有限基的结论;另外利用图灵机的矩阵模型给
i
程序正确性验证的几个问题
出一个具有可解, 但不一致可解字问题的代数;本文还将讨论抽象数据类型
的可靠性与完备性,在此基础上, 给出含空类别的类型系统的可靠性定理。
:本文将对施用性语言的副作用问题进行讨论,
并得到其副作用是非良性的结论; 也对函数式语言,在引入赋值语句后的副
作用问题进行讨论,得到其副作用是良性的结论,另外,对传统的结构化程
序的正确性进行研究,并给出一个一直困扰人们的, 关于循环结构的正确性
证明的解决方案。
关键词:形式化验证;统一建模语言;模型检验;函数式语言;副作用;抽
象数据类型;类别代数; 图灵机
ii
博士学位论文
Abstract
The development puter software is affected by many factors and is
paring with hardware. The safety, reliability and stability of soft-
ware have been important problems and attracted people’s much attention for a
long time.
With the fast development of the huge software as well as the high safety
demand from high technique such as spaceflight and aviation design, the quality
of software, especially the correctness of software,has e more and more
important. Therefore, the proof of the correctness of software and the test of
software have been attractive research fields. The