苏 昭

（江西科技学院 信息工程学院，江西 南昌 330098）

形式化PAR方法及其算法程序规约精化机理

苏 昭

（江西科技学院 信息工程学院，江西 南昌 330098）

用形式化方法开发软件是提高软件生产效率和可靠性的革命性途径，是实现软件自动化的决定性关键。文章介绍了一种新的支持作为软件开发核心的算法设计的形式化方法PAR，分析了其理论基础及算法程序规约精化机理，并结合一个经典实例开发展示了PAR的具体使用，给出PAR的实际应用项目，最后对PAR进行了评述。

形式化PAR方法；规约精化；算法程序

1 概述

形式化方法是建立在严格数学基础上的软件开发方法。软件开发的全过程中，从需求分析、规格说明、设计、编程、系统集成、测试、文档生成直至维护各阶段，凡是采用严格的数学语言、具有精确的数学语义的方法称为形式化方法。软件自动化在未来软件工程中占据着重要的位置，用形式化方法开发软件，被当今计算机界誉为克服“软件危机”、提高软件可靠性和生产效率的革命性途径，是实现软件自动化的关键。

形式化方法的一个十分重要的研究内容就是形式规约，即应用具有精确语义的形式化语言书写的程序功能描述，它是论证程序正确与否的依据。在从高层形式规约至最终代码实现的过程之中,选用恰当的、以形式化方法作为基础的工具进行辅助的验证和设计,对提升安全攸关系统的可信度有着极其巨大的帮助。20世纪90年代以来,在国际上,形式化方法已成为软件开发中重要的可信软件技术之一。……