精化演算支撑工具的分析  

ON ANALYSIS AND DESIGN FOR A REFINEMENT CALCULUS SUPPORTING TOOL

作　　者：王云峰[1,2] 庞军[1,2] 查鸣[1,2] 杨朝晖 郑国梁 

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

出　　处：《计算机应用与软件》2002年第2期1-5,53,共6页Computer Applications and Software

基　　金：国家自然科学基金(编号:69673006);国家"九五"攻关(子专题合同编号:98-780-01-06-07)项目的资助

摘　　要：利用精化演算的方法开发软件,其过程由巨大数量的小步骤构成,由手工完成极其烦琐,也极容易出错。因此,利用机器辅助工具的支持是必要的。在分析现有的精化工具的基础上,我们提出了一个用于软件形式化开发的精化工具RT(RefinementTool),对精化工具进行了需求分析和功能分析。在精化工具的设计中,分析了精化工具的设计目标、总体结构、精化与证明的表示方法、用户界面和工具的扩充性等问题,通过对精化和证明的表示方法的分析,提出了一种精化与证明的表示相结合的方法。In software development,using the refinement calculus requires a large number of small steps;it is tedious and error prone to do this by hand.To achieve a larger scale development, certainly we have to consider computer- based tool support for the refinement calculus. By analyzing the tools new availaele a refinement tool RT is given in the paper. The requirements and functions for the tool are analyzed. In the design of the tool, the goals, the whole architecture, the presentations of refinements and proofs, the user's interface and the extensibility are analyzed. By analyzing the presentations of refinements and proofs, a combination way of them is put forward.

关 键 词：形式方法 精化演算支撑工具 软件工具 计算机 

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