【摘要】 <正> 一、引言形式化方法的研究和应用已有二十多年的历史,源于Dijkstra和Hoare的程序验证以及Scott、stratchey等人的程序语义研究,指为保证复杂系统的可靠性,以数学为基础对其进行精确描述和验证的语言、技术和工具。形式化方法的关键在于形式规约语言。通过语法和语义有严格数学定义的形式规约语言对系统及其各方面性能的描述,产生系统的形式规约,可以帮助开发者获得对所描述系统的深刻理解,并通更多还原

【Abstract】 A software development method was introduced in the paper. First we wrote formal specification in Z and implemented the data refinement. Then we translated it into the refinement calculus notation. Finally we used the laws of the refinement calculus to develop abstract programs into executable code. Translation rules from Z specification to abstract programs were represented.更多还原