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