精化演算支撑工具的分析

ON ANALYSIS AND DESIGN FOR A REFINEMENT CALCULUS SUPPORTING TOOL

利用精化演算的方法开发软件,其过程由巨大数量的小步骤构成,由手工完成极其烦琐,也极容易出错。因此,利用机器辅助工具的支持是必要的。在分析现有的精化工具的基础上,我们提出了一个用于软件形式化开发的精化工具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.