摘要
软件的规范说明阶段(specification phase)对于软件整体开发过程来说是一个非常重要的阶段，它可以被认为是需求分析的一部分。用自然语言来说明软件需求的优点是直观易懂、方便交流，但是会带来很多弊病，如二义性和不精确等。因此必须研究需求分析和规范说明技术以获得一致、完备和准确的软件规范说明书。形式化需求分析和软件规范说明技术就是在需求获取的基础上用建立系统的逻辑模型，从而对复杂实际问题进行分析和抽象、消除错误、去粗取精，最终将用户需求转化为软件规范说明的方法。
软件系统的需求分析和规范说明阶段的多种方法和技术已被提出。这些方法大体上可被分为两类：形式化方法和非形式化方法。非形式化方法一般是采用图表的方式来描述系统。UML就是一种非形式化的方法，该方法是目前比较流行的软件工程开发方法，它对软件整体开发过程提供了一套有用的模型。UML方法已被广泛的应用于软件开发过程的各个阶段。被证明是一种行之有效的方法。但是它有所有非形式化方法所共有的缺点：表达的不严格和不精确，并且和规范的一致性和完整性不能被形式证明。
本文为了解决UML的以上缺点，根据UML和谓词转换，以一阶逻辑和时序逻辑为基础提出一种面向对象的形式化规范说明方法，并给出一组和UML相对应的数学模型。本文的方法吸收了UML和一般形式化方法的优点，具有数学的严谨性和精确性，并且更加易于理解和表达。本软件规范说明方法的研究目标是使其能够最终实现目标代码的自动与半自动生成和程序的自动与半自动验证。
The specification phase is of great importance to the whole process of the software development, which is always considered as part of the requirement system. Using nature language as specification method has many advantages, for instance it can be easily understood and the communion between the customers and programmer become easy. But it can also brings in a lot of disadvantages, for example nature language brings in misconception and imprecision. Consequently it is important to develop a precise method which can be used as a means of software verification. Formal specification is precise method by giving a mathematical model which provides laws to refine and verify the software.
A great numbers of methods of requirements analysis and specification have been put forward, which usually can be categorized into two classes: The formal methods and informal methods. Informal methods generally describe a software system through tables and graphs. UML, as one of the informal methods, is very popular and has been proved as a effective through the process of software development.
This paper put forward a formal method of software specification and a set of mathematics models, which is based on UML and the program semantics of predicate transformer. With the advantage of both UML and formal specification, Application of the method in this paper can be easily expressed and understood together with the mathematic rigorism.
引文
[1]唐稚松 时序程序设计与软件工程 科学出版社 2002.1~64
[2]陆汝钤 计算机语言的形式语义科学出版社 1992.121~212
[3]缪淮扣 李刚 朱关铭 软件工程语言——Z 上海科学技术出版社 1999.23~109
[4]胜德成 抽象代数 科学出版社 1999.75~90
[5]周之英 现代软件工程科学出版社 1999.24~88
[6] Caroll Morga 从规范出发的程序设计 裘宗燕 译 n 机械工业出版社 2002.70~86
[7]周礼全 模态逻辑引轮 上海人民出版社 1986.167~185
[8]陆钟万 面向计算机科学的数理逻辑 科学出版社 2002.200~238
[9]沈复兴 模型论引论 北京师范大学出版社 1994.26~68
[10]冯树春 许六通 程序设计方法学 浙江大学出版社 1987.57~150
[11]冯玉琳 仲萃豪 陈友君 程序设计方法学 北京科学技术出版社 1988.59~126
[12]刘叙华 基于归结方法的自动推理 科学出版社 1992.58~91
[13]C.A.R.Hoare 通讯顺序进程 周巢尘 译 1992.121~158
[14]Dijkstra A discipline of programming Prentice Hall 1976.1~71
[15] R Goldbatt Axiomatising the Logic of Computer Programming. Author: R Goldbatt Springer-Verlag NewYok 1983.213~292
[16] Norain Gehani,Andrew MeGettrick Software Specification Techiques. Addison-Wesley Publishing Company.45~102
[17]Sharam Hckmatpour Software prototyping, Formal methods, and VDM. Addison-Wesley Publishing Company.45~63
[18]Hartmat Ehig, Bernd Mahr Fundament of Algebraic Specification
Spinger-Verlag 1990.49~171
[19] R.Schatch Object-Orient and Classical Software Engineering (Fifth Edition) McGraw-Hill 2002.319~393