精化演算支撑工具的分析

作     者：王云峰 庞军 查鸣 杨朝晖 郑国梁 

作者机构：南京大学计算机软件新技术国家重点实验室南京210093 南京大学计算机科学与技术系南京210093 

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

出 版 物：《计算机应用与软件》 (Computer Applications and Software)

年 卷 期：2002年第19卷第2期

页      码：1-5,53页

摘      要：利用精化演算的方法开发软件,其过程由巨大数量的小步骤构成,由手工完成极其烦琐,也极容易出错。因此,利用机器辅助工具的支持是必要的。在分析现有的精化工具的基础上,我们提出了一个用于软件形式化开发的精化工具RT(RefinementTool),对精化工具进行了需求分析和功能分析。在精化工具的设计中,分析了精化工具的设计目标、总体结构、精化与证明的表示方法、用户界面和工具的扩充性等问题,通过对精化和证明的表示方法的分析,提出了一种精化与证明的表示相结合的方法。

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

学科分类：08[工学] 0835[0835] 081202[081202] 0812[工学-测绘类] 

D　O　I：10.3969/j.issn.1000-386X.2002.02.001

馆 藏 号：203674194...