| 精化演算支撑工具的分析 |
| |
| 引用本文： | 王云峰,庞军,查鸣,杨朝晖,郑国梁.精化演算支撑工具的分析[J].计算机应用与软件,2002,19(2):1-5,53. |
| |
| 作者姓名： | 王云峰 庞军 查鸣 杨朝晖 郑国梁 |
| |
| 作者单位： | 南京大学计算机科学与技术系,南京,210093,南京大学计算机软件新技术国家重点实验室,南京,210093 |
| |
| 基金项目： | 国家自然科学基金(编号:69673006)，国家“九五”攻关(子专题合同编号:98-780-01-06-07)项目的资助 |
| |
| 摘 要： | 利用精化演算的方法开发软件,其过程由巨大数量的小步骤构成,由手工完成极其烦琐,也极容易出错。因此,利用机器辅助工具的支持是必要的。在分析现有的精化工具的基础上,我们提出了一个用于软件形式化开发的精化工具RT(RefinementTool),对精化工具进行了需求分析和功能分析。在精化工具的设计中,分析了精化工具的设计目标、总体结构、精化与证明的表示方法、用户界面和工具的扩充性等问题,通过对精化和证明的表示方法的分析,提出了一种精化与证明的表示相结合的方法。
|
| 关 键 词： | 形式方法 精化演算 精化工具 |
ON ANALYSIS AND DESIGN FOR A REFINEMENT CALCULUS SUPPORTING TOOL |
| |
| Wang Yunfeng Pang Jun Zha Ming Yang Zhaohui Zheng Guoliang.ON ANALYSIS AND DESIGN FOR A REFINEMENT CALCULUS SUPPORTING TOOL[J].Computer Applications and Software,2002,19(2):1-5,53. |
| |
| Authors: | Wang Yunfeng Pang Jun Zha Ming Yang Zhaohui Zheng Guoliang |
| |
| Abstract: | 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. |
| |
| Keywords: | Formal method Refinement calculus Refinement tool |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
