一种精化演算支撑工具的分析与设计

ON ANALYSIS AND DESIGN FOR A REFINEMENT CALCULUS SUPPORTING TOOL

利用精化演算的方法开发软件 ,其过程由巨大数量的小步骤构成 ,由手工完成极其烦琐 ,也极容易出错 ,因此利用机器辅助工具的支持是必要的 .在分析现有的精化工具的基础上 ,提出了一个用于软件形式化开发的的精化工具 (RT) ,并对其进行了需求分析和功能分析 .在精化工具的设计中 ,讨论了作为定理证明器和精化引擎基础的窗口推理系统和用于程序精化推理的程序窗口推理系统 ,同时分析了设计中的设计目标 ,总体结构 ,精化与证明的表示方法 ,用户界面和工具的扩充性等问题 .对于工具的理论基础做了较为详细的分析 。

The refinement calculus neatly formalizes the stepwise refinement ideas using the weakest precondition formalism of Dijkstra. Using a wide spectrum language, which incorporates both specification and executable code constructs, and a set of refinement rules, the calculus enables an abstract specification to be transformed into an executable program whose correctness depends on that of each refinement step. Developing software using the refinement calculus requires a large number of small steps; it is tedious and error prone to do this by hand. To achieve larger scale development with the refinement calculus, it seems natural to consider computer aided tool support. By analyzing the existing tools for this purpose, a refinement tool RT is debated in the paper. The requirements for a refinement tool are examined and the tool is described, which is developed to meet these requirements. The distinctive features of our tool are: ① the use of a theorem prover, both for applying refinement rules and for proving obligations; ② a new logic and proof paradigm (program window inference) that handles context in both refinement and proof; ③ an extensible theory base, supporting the Z toolkit and allowing adaptation to new application domains; ④ a flexible user interface that supports construction and reuse of program derivations. In the paper,the requirements and functions for the tool are analyzed. In the design, the window inference and the program window inference are debated detailedly, which are the base for theorem prover and refinement engine .The issues of the primary design such as the goals, the architecture, structured presentation of refinements and proofs, user interface and the extensibility are analyzed. The detailed design and the implement for the tool will be the future work.