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