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

A Software Development Method:From Z to Refinement Calculus

作　　者：查鸣[1] 王云峰[1] 郑国梁[1] 

机构地区：[1]南京大学计算机科学系软件新技术国家重点实验室,南京210093

出　　处：《计算机科学》2000年第2期14-17,68,共5页Computer Science

基　　金：本课题得到"九五"攻关项目(98-780-01-07-06);国家自然科学 69673006

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

关 键 词：软件开发方法 Z语言 精化演算 形式化描述语言 

分 类 号：TP311.52[自动化与计算机技术—计算机软件与理论]