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

苏 昭

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

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

苏 昭

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

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

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

1 概述

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

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

著名的形式化PAR(Partition-and-Recur)[5-11]方法是由中国知名计算机科学专家、江西师范大学薛锦云教授及其领衔的软件形式化与自动化团队研究的一种新型形式化方法学，其着重研究软件的核心-算法程序的形式化开发。形式化PAR方法[11]由自定义的泛型算法设计语言Radl、泛型抽象程序设计语言Apla、系统的形式化开发算法程序技术及转换工具集构成。其中Radl又是形式化规约描述语言，规约是形式化软件开发的逻辑起点，是程序正确性证明、形式化推导的关键，本文主要介绍Radl规约及规约精化机理。

2 形式化PAR方法

2.1 规约

PAR方法对从软件形式规约说明Radl到可执行语言程序的软件(半)自动开发提供有力支持。Radl语言不但适应传统数学之习惯,而且具备引用的透明性,十分有利于形式化规约说明的推导。

Radl语言的主要功能在于描述问题的形式化规约说明、规约说明变换规则以及描述算法。Radl提供了足够抽象的机制,可集中刻画问题的功能,而不为设计和实现所涉及的问题(如效率)所干扰[12]。

我们采用如下Radl算法规约说明的刻画形式[11]:

|[标识符说明]|

AQ:谓词表达式；

AR:谓词表达式。

其中,标识符说明部分主要用于声明在前、后置断言中出现的变量和函数的属性及类型。属性有 3种[11]:一是输入变量,用关键字IN标识；二是输出变量,用关键字OUT标识；三是辅助变量,用关键字AUX标识。类型可以是Radl语言中的标准数据类型(integer,real,char,string,boolean)、自定义简单类型(数组类型，记录类型，子界类型，枚举类型)、预定义ADT类型(序列类型，集合类型，树类型，图类型)和自定义ADT类型。

以AQ和AR开头的谓词表达式分别称为算法程序的前置断言和后置断言,用于表示算法程序的输入参数必须满足的条件、输出参数必须满足的条件,均为一阶谓词逻辑公式[11-13],其中AQ是一般的一阶谓词表达式，AR有两种表达形式:

一般形式:问题的定义式。

标准形式:(Qi:r(i):f(i))),表示“在范围r(i)上,对函数f(i)施行 q运算所得到的量”,其中,Q是q运算的一般化,可以是∃(存在量词),∀(全称量词),MAX(求最大值量词),MIN(求最小值量词),∑(求和量词),∏(求积量词)等,所分别对应的q运算分别是∨,∧,max,min,+,*等，标准形式是对问题的更进一步的逻辑抽象[11]。

选取一般形式亦或标准形式来刻画描述问题的原则是:刻画问题直观简洁和有利于探寻隐含在问题之中的深层递推关系。

下例是一个使用标准形式(Qi:r(i):f(i))描述的计算图单源最短路径问题的形式化Radl规约说明[7,12]:

2.2 分化递推思想及规约精化机理

根据PAR方法,解决问题是通过分划出子问题并对子问题求解的基础上来完成的。在构造递推关系时，必须将子问题分划出来并揭示出它们之间的逻辑关系。规约是对问题的形式化描述,问题的分划体现在规约变换上即为分划规约。

2.2.1 分化递推

为了构造问题的递推关系，首先必须对问题进行科学合理的划分。

石海鹤[14]深入研究了子问题规模间的关系,将问题分划成两种方式：平衡分划与非平衡分划,并定义如下（P(n)表示问题,n为问题规模）：

定义1.平衡分划是指将问题P(n)分成k个

规模相等或相差最多不超过1的子问题,这里1〈k≤n/2，具体地说,设n mod k=s,则平衡分划时将P(n)分成k-s个规模为的子问题和s个规模为的子问题；

不符合定义1的分划称为非平衡分划。

人们对于原问题的划分往往蕴含算法设计的策略,并为进行后续的规约变换以构造递推关系提供整体方向。通过推导大量算法程序的实践发现,影响算法效率的首要因素在于对问题的分化,提高问题求解的效率往往可以通过改变问题分划的方式而轻易获得，如排序问题,从相同的形式化规约出发,经不同的分划方式变换,可开发出多个复杂度不同的算法。

由于对算法问题求解时,已知的内容仅有问题及其形式化规约,我们就必须从问题特征以及问题的形式化规约入手,采用具体分划方式以获取较高效率的算法。石海鹤[14]通过大量问题分划的深入研究,提出了从问题形式化规约确定分划方式的问题分划法则(Partition Rules,PR),用来指导面向效率的问题分划，并有以下两个重要定理：

定理1.问题分解出的子问题相互独立时,对问题做平衡分划所设计出的算法效率要比非平衡分划时高；

定理2.问题分解出的子问题存在相互重叠时,对问题做非平衡分划所设计出算法的效率要比平衡分划时高。

2.2.2 基本规约变换法则[11]

2.2.3 规约精化

记问题为P(n),它的解记为SP(n)，n为问题

2.若CSp包含有(Qi:r(i):f(i))的部分,即量词Q仅含一个约束变量i,则根据分划之形式对r(i)运用范围分裂变换法则,将CSp尽量展开；

3.范围为单点时，运用单一范围变换规则；

4.据上下文对CSp进行谓词演算或运用与量词函数相关的性质进行变换；

7.根据再做深入分析：

3 实例研究

应用本文结果,我们为求解圆周率问题开发一个算法程序，阐述的重点放在问题的规约及其规约精化上，即问题分化、递推关系构造上,对于生成可执行程序的过程仅做简要叙述。问题[13,16-17]：求解圆周率π

(1)问题形式化规约的构造

(2)原问题分划

根据数列知识，采用非平衡分划:

把初始条件(2)与递推关系(1)结合,得求解问题的Radl算法:

(4)循环不变式的开发

根据循环不变式的新定义及新的开发策略[11],变量P存放Sm的值,则可机械地写出循环不变式:

(5)抽象算法程序（Apla）

在转换工具Radl-Apla的支持下可自动生成Apla抽象程序 (核心代码)：

(6)算法程序代码

把上述程序加上输入语句和输出语句,用PAR方法转换工具可将其自动地生成C++或Java等语言程序,这里不再赘述。

4 应用项目

这里简单介绍使用形式化PAR方法及其规约精化技术开发的一个实际应用项目[18]。

装备保障决策支持系统用于对装备保障数据库中的大数据及其它可用的情报数据进行实时、迅速地在线整合分析，使装备保障内外的大数据转化为科学的管理决策信息。构建装备保障决策支持系统，对平时和战时装备保障数据的存储与分析，为装备指挥决策提供科学支撑，是实现现代化装备保障的需要。系统的效率、智能化水平和可靠性，将对决策的效果产生重大影响。在装备保障智能决策支持的开发过程中引入形式化方法，能够实现部分开发过程的自动化，并有助于从根本上提高软件系统的质量，提高我军装备保障工作的整体水平[19-20]。进而，文献[18]基于形式化PAR方法，提出一类离散最优化问题的结构模型和算法推演技术,形式化求解了一系列典型的装备保障算法。

5 结束语

本文介绍的形式化PAR方法是薛锦云教授及其领衔的软件形式化与自动化团队在算法程序设计自动化方面作出的研究。PAR方法将分化递推思想巧妙地运用到算法程序自动化设计之中，具有严格的数学理论基础和平台支撑。本文结合PAR的最新研究成果[10,12,14-15]，着重介绍了形式化PAR方法的规约及其规约精化机理，并通过对简明经典实例的开发展示了使用PAR求解算法问题时分划问题、构造递推关系的特征。整个推导过程采用通俗易懂的数学知识、严谨的量词等价变换,体现了递推关系构造的简明性与严谨性,提高了基于递推关系所生成的算法程序的正确性，用支持算法程序形式化开发的PAR方法与PAR平台求解算法问题的过程,也自然地、科学地揭示出了算法程序的来源问题[13]。

[1]邹盛荣,郑国梁.B语言和方法与Z、VDM的比较[J].计算机科学,2002,29(10):136-138.

[2]Batory D.Thoughts on automated software design and synthesis.In:Proc.of the FSE/SDP Workshop,Future of Software Engineering Research(FoSER 2010).New York:ACM Press,2010.29-32.

[3]周之英.现代软件工程[M].北京:科学出版社，2000.

[4]High Confidence Software and System Coordinating Group.High confidence software and systems research needs[EB/OL].(2001-01-10).http://www.nitrd.gov/pubs/hcss-research.pdf.

[5]Xue JY.Two new strategies for developing loop invariants and their applications. Journal of Computer Science and Technology,1993,8(2):147-154.

[6]Xue JY.A unified approach for developing efficient algorithmic programs.JournalofComputerScience and Technology,1997,12(4):314-329.

[7]Xue JY.Formal derivation of graph algorithmic programs using partition-and- recur.JournalofComputerScience and Technology,1998,13(6):553-561.

[8]Xue JY,Yang B,Zuo ZK.A linear in-situ algorithm for the power of cyclic permutation.In:Proc.of the 2nd Int'l Frontiers of Algorithmics Workshop.Berlin:Springer-Verlag,2008.113-123.

[9]Xue JY.PAR method and its supporting platform.In:Proc.of the 1st Int'l Workshop on Asian Working Conf.on Verified Software.Macao:UNU-IIST,2006.10-20.

[10]DengXiaotie,HopcroftJohn E,Xue Jinyun.Frontiersin Algorithmics[M].Berlin and Heidelberg GmbH&Co.K:Springer-Verlag,2009.

[11]薛锦云,杨庆红,等.程序设计方法学[M].北京:高等教育出版社,2002.

[12]王昌晶,薛锦云.Radl形式规格说明相对正确性研究[J].软件学报,2013,24(4):715-729.

[13]苏昭,薛锦云,杨晨.形式化方法在高中算法教学中的应用研究[J].计算机与现代化,2010(7):87-92.

[14]石海鹤,薛锦云.基于PAR的算法形式化开发[J].计算机学报,2009,32(5):982-991.

[15]石海鹤,薛锦云.基于 PAR的排序算法自动生成研究[J].软件学报,2012,23(9):2248-2260.

[16]苏昭.关系代数→关系演算转换系统的研制[D].南昌:江西师范大学硕士学位论文,2010.

[17]冉小晓.Radl-Apla自动程序转换系统研究与实现[D].南昌:江西师范大学硕士学位论文,2005.

[18]郑宇军.基于PAR的高可信装备保障算法形式化推演[博士学位论文].北京:中国科学院软件研究所,2009.

[19]张子丘,郑宇军,王侃.形式化方法在装备保障决策支持系统中的应用[J].装甲兵工程学院学报,2005,19(4):13-16.

[20]郑宇军,王连来,薛锦云.面向装备联勤保障的约束程序设计框架[J].南京大学学报（自然科学）,2005,41(z1):30-34.

（责任编辑：陈 辉）

Formal Method PAR and Its Algorithmic Program Specification Refinement Mechanism

SU Zhao
（College of Information Science and Engineering,Jiangxi University of Technology，Nanchang 330098,China）

Developing software using formal method is a revolutionary way to develop software efficiently and reliably，and is key to realize software automation.This paper introduces a new formal method PAR that supported automatic algorithm design,analyzes its theoretical foundation and specification refinement theory,then presents a detailed example of using PAR is and illustrated one practical application.Finally gave the discussions and conclusions.

formal method PAR；specification refinement；algorithmic program

TP312

A

123（2014）03-0053-05

2014-03-03

苏昭(1984－)，男，安徽亳州人，江西科技学院信息工程学院，讲师，硕士。研究方向：软件形式化与自动化。

江西科技学院自然科学基金项目“基于项目反应理论的成人高考数学模块化训练系统的研制”(NO.XYKJ2011012)；江西科技学院协同创新基金项目“面向车联网的智能交通最短路径算法的优化及其应用研究”(NO.xtcx201318)。