精化演算支撑工具PRT的研究  

On A New Support Tool PRT for the Refinement Calculus

作　　者：杨朝晖 王云峰[1] 郑国梁[1] 

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

出　　处：《计算机科学》2000年第3期47-50,46,共5页Computer Science

基　　金：国家自然科学基金;国家"九五"攻关项目基金

摘　　要：1 引言精化演算是一种数学表示法和若干规则的集合,用于从程序规约推导出命令式程序。精化是从抽象程序向具体程序转换的过程,其中包含程序的正确性证明。精化的程序开发方法比对已有程序进行验证以保证程序正确性的方法更有效。通过精化演算中的转换规则可以演算出精化的程序。利用精化演算从规约导出程序的过程由大量步骤构成,非常适合利用机器工具进行辅助。本文对精化工具进行了需求分析和功能分析,研究了一个新的精化工具PRT(Program Refinement Tool)并与现有的一些工具进行了比较。The refinement calculus for the development of programs from specifications is suited to mechanised support. We review the requirements for tool support of refinement as gleaned from our experience with a number of existing refinement tools,and report on the design and implementation of a new tool to support refinement based on these requirements. The main features of the new tool are close integration of refinement and proof in a single tool (the same mechanism is used for both) ,good management of the refinement context.

关 键 词：程序正确性 精化演算支撑工具 PRT 程序结构 

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