一种从Z到精化演算的软件开发方法

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