一种基于Z和精化演算的形式化开发方法  

A FORMAL DEVELOPMENT METHOD BASED ON Z AND REFINEMENT CALCULUS

作　　者：阮幼林[1] 李传湘[1] 

机构地区：[1]武汉水利电力大学计算机科学与技术系,湖北武汉430072

出　　处：《小型微型计算机系统》2001年第5期592-595,共4页Journal of Chinese Computer Systems

摘　　要：通过分析 Z和精化演算各自的特点 ,本文提出了一种使两者无缝集成的形式化开发方法 .该方法利用 Z良好的描述特性和扩充的类机制 ,将系统规约直接定义成精化演算中的抽象程序 ,然后用精化规则对抽象程序逐步精化 ,直到可执行程序 .This paper presents a formal software development method . The method combines the data structuring capabilities and the extended type mechanism of Z and the refinement calculus ,which provides a formal path from design to implementation without unnecessary transformation of notation or the definition of a new calculus .It is illustrated by the development of a simple system.

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

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