基于PAR的算法形式化开发

《计算机学报》2009年5期1基于PAR的算法形式化开发*石海鹤1,2,3薛锦云1,21（中国科学院软件研究所计算机科学国家重点实验室北京100080）2（江西师范大学高性能计算技术重点实验室南昌330022）3（中国科学院研究生院北京100049）摘要：形式化方法是构建可信软件的重要途径。基于对算法问题的分析，针对形式化方法PAR开发算法的特征，刻划了问题分划、递推关系构造方面的规律。从一类问题的形式化功能规约出发，可机械的完成问题的分划及规约的变换，自然的揭露出求解问题的算法思想，在相关工具的支持下自动生成算法程序。研究结果将算法设计中尽可能多的创造性劳动转化为非创造性劳动，降低了形式化求解算法问题的难度，提高了算法程序的可靠性和形式化开发效率。关键词：算法；形式化方法；PAR；规约；可信软件*本课题得到国家自然科学基金（60573080,60773054）、江西省自然科学基金（2008GQS0056）资助.石海鹤,女,1979年生,博士研究生,主要研究方向为软件形式化与自动化.E-mail:[e-mail].薛锦云,男,1947年生,教授,博士生导师,主要研究领域为软件形式化与自动化,可信软件.《计算机学报》2009年5期21引言随着社会对信息技术的依赖性日益增长，处于信息技术核心的计算机软件的可信性被提到一个新的高度，国内外都很重视并已开展大量的研究工作。作为学术界的领袖人物之一，Hoare在欧、美同行的支持下，正组织关于软件验证（VerifiedSoftware）的国际性项目，这被认为是计算机科学界本世纪的一个重大挑战性问题[1]；美国政府制定的2006-2015国家软件发展战略——“下一代软件工程”中，也将提高软件可信性放在四大战略任务的首位。对软件可信性的需求已从安全性至关重要的领域，如国防、航空航天、医疗器械等扩展到能源、通信、财经、制造业等关键领域。而正确性被一致认为是可信软件的极其重要的性质。算法作为软件的核心，被誉为“计算的灵魂”[2]，保证算法的正确性对提高安全攸关系统的可信度有很大帮助。统计表明，传统的非形式化方法对软件质量的保证具有一个难以逾越的顶点，而形式化方法的实践证明形式化方法是提高软件质量的重要途径[3]。20世纪90年代以来，在国际上，形式化方法已成为软件开发中重要的可信软件技术之一，它在保证算法的正确性、展示算法设计的过程、揭示算法设计的本质特征和一般规律方面具有重要的意义，对自动程序设计的探索将有很大的帮助[4,5]。由于算法求解涉及到创造性劳动，形式化开发算法仍然是计算机领域中最具挑战性的问题之一。本文针对形式化方法PAR（Partition-and-Recur）[6-11]开发算法的特征，刻划了问题分划、递推关系构造方面的规律，使得从问题的形式化功能规约出发，问题的分划及规约的变换可机械的完成，自然的揭露出求解问题的算法思想，自动的生成高效的求解问题的算法程序。接下来我们首先介绍了PAR方法，重点介绍和分析了其中的形式化功能规约机制和开发算法程序的方法；然后结合对问题的分析，详细阐述了我们提出的问题分划法则和规约变换策略；在第5节通过一个代表性的算法开发实例展示了该模式的应用效果；第6节和相关工作进行了比较；于文章最后作了总结和讨论。2PAR方法PAR方法是一种统一的算法设计方法，涵盖了多种已知的算法设计技术，例如，动态规划法、贪心法、分治法、穷举法等等，支持算法程序开发的全过程。这里，算法程序是指用已实现的或抽象的程序设计语言描述的算法。如图1所示，该方法由自定义泛型算法设计语言Radl(Recurrence-basedAlgorithmDesignLanguage)、泛型抽象程序设计语言Apla(AbstractProgrammingLanguage)、系统的算法和程序设计方法学及转换工具集组成。其中，PAR对从问题出发设计出Radl算法的过程提供了形式化支持；对从Radl算法经Apla程序到可执行语言程序的生成提供了自动化的支持。图1.PAR2.1形式化功能规约形式化功能规约是算法程序开发的起点。Radl语言的主要功能是描述问题的规约、规约变换规则和描述算法，由算法规约语言和算法描述语言两部分组成。Radl提供了足够抽象的机制，可集中刻划问题的功能，而不为设计和实现所涉及的问题（如效率）所干扰。我们采用如下Radl算法规约的刻划形式：|[标识符说明]|AQ:谓词表达式；AR:谓词表达式；其中标识符说明部分主要用于说明前、后置断言中出现的变量和函数的属性及类型。属性有三种：一是输入变量，用关键字in标识；二是输出变量，用关键字out标识；三是辅助变量，用关键字aux标识。类型可以是Radl语言中的标准数据类型（integer,real,boolean,char,string）、自定义简单类型（记录类型，数组类型，枚举类型和子界类型）、预定义ADT类型（集合类型，序列类型，树类型，图类型）和自定义ADT类型。以AQ和AR开头的谓词表达式分别称为算法的前置断言和后置断言，用于表示算法的输入参数《计算机学报》2009年5期3必须满足的条件和算法的输出必须满足的条件，均为一阶谓词逻辑公式。使用统一的格式(Qi:r(i):f(i))表示“在范围r(i)上，对函数f(i)施行q运算所得的量”，其中Q是q运算的一般化，可以是A(全称量词)，E(存在量词)，MIN(求最小值量词)，MAX(求最大值量词)，∑(求和量词)，∏(求积量词)等，分别对应着的q运算是∧，∨，min，max，+，*等。利用量词的性质可以对规约做等价变换，以揭露问题求解的思想。本文用到的性质有：(1)交叉积(Qi,j:r(i)∧s(i,j):f(i,j))≡(Qi:r(i):(Qj:s(i,j):f(i,j)))(2)范围分裂(Qi:r(i):f(i))≡(Qi:r(i)∧b(i):f(i))q(Qi:r(i)∧﹁b(i):f(i))(3)单点范围(Qi:i=k:f(i))≡f(k)(4)一般分配律若二元运算符⊙满足交换律，且对q满足分配律，i不是g的自由变量，则有(Qi:r(i):g⊙f(i))≡g⊙(Qi:r(i):f(i))2.2开发算法程序的方法问题求解序列递推关系的定义为[7]：定义2.1.假定问题P的解可由n个计算步产生的结果序列S1,S2,…，Sn得到。对于由计算步产生的每一Si,1≤i≤n，都是P的一个子解，则Sn就是问题P的解。构造等式：Si=F(Sj)，表示Si是其子解Sj的函数，其中,1in,1ji,Sj表示多个子解Sj的序列。我们称等式Si=F(Sj)为问题求解序列的递推关系或简称为递推关系。基于递推关系的概念，使用PAR开发算法、循环不变式及程序的全过程可分成5步[7]：(1)构造求解问题的Radl功能规约。（规约可以是形式化的，也可以是非形式化的。形式化规约使得算法程序的形式推导和证明成为可能。对于不追求算法形式化开发的情况，可以使用非形式化的规约，而本文的研究，要求构造的规约必须是形式化的Radl规约。）(2)把需求解的问题分划成若干和原问题结构相同但规模更小的子问题。(3)依据分划的形式对功能规约进行变换，以构造问题求解序列的递推关系。(4)基于递推关系，生成Radl算法，并基于我们提出的循环不变式新定义及新开发策略构造循环不变式。(5)基于所得的Radl算法和循环不变式开发Apla抽象程序，并进一步转换成可执行语言程序。2.3分析与小结PAR开发算法程序时，首先构造形式化规约，下一步便是如何根据形式化规约设计出正确（即满足规约）且高效的算法程序，用到的关键技术是分划和递推。不同的分划及不同变换规则的选取会构造出不同的递推关系，从而对应到不同的算法，直接影响到最终算法的形式及效率。然而，如何进行面向效率的问题分划和规约变换以构造出递推关系，在PAR中还没有给出具体的指导策略。本论文基于PAR，以结果算法的效率作为决定问题分划和规约变换的标准，研究了问题分划、递推关系构造方面的规律，以促成从Radl规约到Radl算法的自动生成。3问题分划根据子问题规模间的关系，我们将问题分划分为平衡分划和非平衡分划两种方式，并定义如下，其中P(n)表示问题，n为问题规模：定义3.1.平衡分划是指将问题P(n)分成k个规模相等或相差最多不超过1的子问题，这里1k≤n/2。具体地说，设nmodk=s，则平衡分划时将P(n)分成k-s个规模为n/k的子问题和s个规模为n/k的子问题。不符合定义3.1的分划称为非平衡分划。对原问题的分划体现了初始的算法设计策略，且为后续进行规约变换以寻找递推关系提供了总体方向。通过大量算法的推导实践发现，问题分划方式是影响算法效率的首要因素，改变问题分划的方式可大幅度提高问题求解的效率。如排序就是一个典型的例子，从一个公共的问题规约出发，通过使用不同的分划方式，可以开发出很多不同复杂度的求解算法。为了追求算法的效率，我们需要更多关于问题分划的启发性规则。由于求解算法问题时，已知的内容仅有问题及规约，这就要求我们从问题特征和问题的形式化规约，得到导致高效率算法的具体分划方式。通过对问题分划已开展的大量研究，我们形成了从形式化问题规约确定分划方式的问题分划法则（PartitionRules，简记为PR），用以指导面向效率的问题分划。下面，我们先给出关于子问题及变量值的定义：《计算机学报》2009年5期4定义3.2.分划问题P时，将其自顶向下分解成若干和P结构相同但规模更小的子问题，再按同样的方式把子问题分划成更小的子问题，直到每一个子问题能直接求解为止。我们将问题P分解过程中产生的子问题集合称为P的子问题空间。定义3.3.若问题P1和P2的子问题空间不包含相同的子问题，则称P1和P2互相独立。反之，称P1和P2互相重叠。定义3.4.变量值是指简单类型变量的值，或者组合类型变量所含元素的值。记原问题为P(n)，n为问题规模。用X表示P(n)的输入变量值的集合，Y表示其输出变量值的集合，X和Y均可从P(n)规约中获得。关于P(n)的子问题间是否独立，我们有以下引理：引理3.1.若YX，则P(n)分解出的子问题互相独立。引理3.2.若YX，且Y中的值是经X的算术计算而得到，则P(n)分解出的子问题间有重叠。引理3.3.若YX，且Y中的值不是经X的算术计算而得到，同样有（3.1）的结论。证明：令X={x1,x2,…,xn}，Y={y1,y2,…,ym}，1≤m≤n。当m=1时，输出仅为一个值。为描述方便，我们考虑将问题分划成两个规模更小但结构相同的子问题：第一个子问题的输入值集合X1={x1,x2,…,xi}，输出值的集合Y1={y11,y12,…,y1s}，第二个子问题有X2={xi+1,…,xn}，Y2={y21,y22,…,y2t}，1≤s≤in，1≤t≤n-i，这里X1和X2分别表示X的前i部分和后n-i部分。对于（3.1），YX，则有Y1X1Y2X2X1∩X2＝，Y和Y1、Y2间的关系为：Y＝Y1Y＝Y2Y＝Y1∪Y2，且Y1∪Y2X。由Y、Y1和Y2间的关系可以看出两个子问题解Y1和Y2独立的用于构建最终解，这两个子问题互相独立。对于（3.2），设输出是输入的F算术计算，则有Y=F(X)，且Y1=F(X1），Y2=F(X2)。由YX有Y1X1∧Y2X2。由于Y是整个输入集X上的函数，而Y1、Y2则分别是X的子集X1、X2的函数，故Y和Y1、Y2间的关系是：Y=G(Y1,Y2)，此处的G是一个新的函数，即两个子解还需要经过计算才能得到最终解，而这里的计算过程中所求解的子问题与求解两个子问题的过程中分划出的子问题有重复，图2形象地表示了这个过程。(3.2)刻画了最优化问题的特征，该类问题计算最优值的规约涉及(MINi:r(i):f(i))或(MAXi:r(i):f(i))等量词，而f(i)部分通常是对输入值进行某种运算，如求和等。图2问题分解过程示意图引理（3.3）实际上刻画了判定性问题和计数问题的特征。判定性问题