【作者】 刘艳平；

【导师】 王志刚；

【作者基本信息】 湖南师范大学 ， 计算机应用技术， 2009， 硕士

【摘要】 软件开发的形式化方法被当今软件工程领域誉为克服“软件危机”,提高软件可靠性和生产效率的革命性途径。为了克服自然语言和程序设计语言描述规格说明的模糊性和歧义性缺陷,人们提出了形式化开发范型,即通过形式化、规范化的数学理论,用描述“做什么”来取代“怎么做”。Z语言就是形式化方法中具有代表性的一种形式规格说明,它语言精确、无二义性,可以用于推理和对需求规格说明求精。求精是规格说明实现可执行化的重要过程,实现规格说明求精,可以为Z语言应用于更广泛的领域奠定基础。本文重点研究Z形式规格说明的求精方法,以Z的数据型求精为基础,对Z形式规格说明进行自顶向下,逐步求精,结合C++语言、数据结构以及C++标准模板库技术,探讨Z规格说明的求精方法。Z是一个类型化的语言,有丰富的数据类型,其数据类型分为简单类型与复合类型。由于Z语言的数据类型相当复杂,现有的高级语言不支持Z语言数据类型的直接转换。但是,C++语言的标准模板库中定义的容器类型却为Z语言数据类型的转换提供了良好的支持,本文先对Z语言的各种数据类型进行分析,然后研究了将其转换为C++代码或C++容器类型,将类型的各种操作算子转换成C++函数的方法,为Z规格说明的进一步求精变换奠定了基础。本文研究的内容为软件工程设计阶段提供新思路,有助于推进形式化软件工程方法应用于软件开发实践,使软件开发过程更加合理,软件设计更加周密,软件开发的资金分配更加明确,进而达到降低软件开发成本和减少软件后期维护的目的。更多还原

【Abstract】 Formal software development method is praised as the revolutionary way of software engineering to overcome the "software crisis", and to improve the reliability and the productivity of software. In order to overcome the ambiguities of natural languages and programming languages, people proposed formal models, which describe "what to do" to replace "how to do" by using mathematical theories of formalization and standardization.Z language is a representative specification language with the qualities of exactness and unambiguity. It can be used for reasoning and refinement of requirment specification. Refinement is an important process of implementing specification to execution. To implement refinement can make the application of Z language wider. This article focuses on the refinement methods of Z formal specification. Based on the refinement of data types, we refine Z formal specification by top-down and stepwise methods. Combined with C++ language, data structure, as well as C++ Standard Template Library technology, the refinement methods of Z specification are explored.Z is a typed language and has a wealth of data types. Its data types include simple types and composite types. Because of the complexity of data types in Z language, there is no direct way to transform the data types of Z specification to the existing high-level languages. However, the standard template library container types defined in C++ language provides a good support for the transformation of Z language data types. This article first analyzed the data types of Z language, and then researched the methods to transform them to C++ codes or C++ container types, and their operators into C++ functions. The foundation for further transformation and refinement of the Z specification is set up.The researched content of this paper provides some new ideas for the design phase of software engineering and helps to promote the application of formal methods in software engineering practice of software development. It makes software development process more rational, software design more careful, and the allocation of funds for software development more definite, thus the costs of software development can be depressed and the latter maintenance can be reduced.更多还原