精化演算支撑工具的分析

• 作者: 庞军 杨朝晖 查鸣 王云峰 郑国梁
• 来源期刊: 计算机应用与软件
• 学科: 工学
• 关键词: 形式方法 精化演算 精化工具
• 年，卷（期）: 2002,（2）
• 所属期刊栏目: 基金项目论文
• 页码范围: 1-5,53
• 页数: 6页
• 分类号: TP3
• 字数: 5941字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-386X.2002.02.001

摘要

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