一种从Z到精化演算的软件开发方法 |
| |
引用本文: | 查鸣 王云峰. 一种从Z到精化演算的软件开发方法[J]. 计算机科学, 2000, 27(2): 14-17 |
| |
作者姓名: | 查鸣 王云峰 |
| |
作者单位: | 南京大学计算机科学系,软件新技术国家重点实验室,南京,210093 |
| |
基金项目: | 本课题得到“九五”攻关项目(98-780-01-07-06)和国家自然科学基金(69673006)资助。 |
| |
摘 要: | 一、引言形式化方法的研究和应用已有二十多年的历史,源于Dijkstra和Hoare的程序验证以及Scott、stratchey等人的程序语义研究,指为保证复杂系统的可靠性,以数学为基础对其进行精确描述和验证的语言、技术和工具。形式化方法的关键在于形式规约语言。通过语法和语义有严格数学定义的形式规约语言对系统及其各方面性能的描述,产生系统的形式规约,可以帮助开发者获得对所描述系统的深刻理解,并通
|
关 键 词: | 软件开发方法 Z语言 精化演算 形式化描述语言 |
A Software Development Method: From Z to Refinement Calculus |
| |
Abstract: | A software development method was introduced in the paper, First we wrote tormal specification in Z and implemented the data refinement. Then we translated it into the refinement calculus notation. Finally we used the laws ot the refinement calculus to develop abstract programs into executable code. Translation rules from Z specification to abstract programs were represented. |
| |
Keywords: | Z Specification Refinement calculus |
本文献已被 CNKI 维普 万方数据 等数据库收录! |
|
点击此处可从《计算机科学》下载全文 |