序列折半划分问题的形式化推导*

左正康,梁赞杨,苏 崴,黄 箐,王 渊,王昌晶

(1.江西师范大学计算机信息工程学院,江西 南昌330022;2.江西师范大学软件学院,江西 南昌330022)

1 引言

形式化方法作为一种基于数学语言和精确逻辑语义的方法被广泛应用于提高软件的可靠性和正确性[1,2]，在软件开发的各个阶段发挥着不同的作用。形式化方法的研究方向可以分为形式化推导和形式化验证[3]。形式化推导是在程序正确性证明理论下所进行的程序开发，通过程序规约构造具体程序[4]。形式化验证指的是针对一个已有程序，采用证明的方式判断该程序是否满足其程序规约[5]。序列作为一种高效且常用的数据结构，在程序开发中被用于解决很多场景的实际问题，序列算法始终是人们研究的重要内容[6]。然而，通过自然语言来描述算法问题与算法设计过程，其正确性难以保证。实践证明，只有用数学方法对算法程序进行形式化推导或形式化证明，算法程序的正确性才能从逻辑上得到保证[7]。对于很多序列类问题，运用折半划分的思想可以使问题更为简单，进而开发出精妙且高效的算法。针对序列折半划分问题开发一个形式化推导方法来保证算法的正确性是一项很有意义的工作。现有的形式化推导方法将程序的开发与程序的证明交替进行，这一过程繁琐且大多都只能推导得到抽象程序，而如何将抽象程序准确地转换为可执行程序又成为一个难点。

为解决上述问题，本文提出了针对序列折半划分问题的形式化推导方法，并以2种序列折半划分问题为实例验证了该方法的可行性。因非递归算法的效率远高于其递归算法[8]的，故本文采用基于分划递推技术[9]的形式化推导方法。该方法先形式化描述问题的程序规约，通过分析问题的数学特性，对问题进行分划。再通过程序规约变换技术对程序规约进行一系列数学变换，进而获得算法程序的递推关系和循环不变式。最终得出问题的Apla(Abstract programming language)程序并转化为可执行程序。该推导方法包含了从程序规约到可执行程序的整个开发阶段，推导过程以一阶谓词逻辑为基础，应用规约变换技术严格保证了规约的前后一致性。

本文提出的推导方法有以下优点：(1)基于分划递推的核心思想，应用规约变换技术对问题进行形式化推导，过程简洁明了；(2)在构造算法过程中，循环不变式可由递推关系自然地构造得到，循环不变式构造相对容易；(3)实现了从程序规约到具体可执行程序的完整程序求精过程。使用该方法推导程序可以将重点放在设计算法上，更多地考虑算法内部的逻辑，使推导与求精同步进行。

本文第2节对相关工作进行介绍和比较。第3节对序列折半划分问题形式化推导方法进行了详细说明。第4节介绍了转换平台：Apla到C++程序自动生成系统。第5节将第3节中提出的方法应用于“有序序列搜索特殊下标”和“循环序列搜索最小元素下标”这2个实例，进行推导得出递推关系式和循环不变式，由此再推导出对应问题的非递归Apla算法并通过“Apla到C++程序自动生成系统”自动生成C++可执行程序。第6节对全文进行总结。

2 相关工作

程序的形式化推导相较于形式化验证，较多强调在演绎系统内工作的能力，通过形式化描述的断言来“发现”程序[10]。该方法从问题的精确规约出发，在程序正确性证明理论的指导下进行程序开发，使整个程序的开发及其正确性证明同时进行，边求精，边推导，程序开发过程完成的同时，它的正确性也得到了保证。

Dijkstra[11]提出的最弱前置谓词方法提供了赋值语句、选择语句和循环语句的形式化推导方法，通过给出问题的精确程序规约，并以此作为程序设计的出发点，然后在程序验证系统的指导下求解出所需的程序。将程序开发及其正确性证明“手拉手”地解决。程序每个片段的证明总是先于该片段代码得到，这种方法的重点在开发程序而不是设计算法，它将程序正确性证明的理论融合到开发过程中，边开发边保证程序的正确性，自动化程度低。另外，用程序演算方法不能直接形式化推导出程序语句，且对于复杂程序难以进行推导。

文献[12,13]从程序规约出发给出了最大分段和等问题的计算推导步骤，突出显示了程序派生会话中涉及的典型步骤。其推导步骤基于最弱前置谓词方法，并将后置断言拆分成多个规约，再组成循环不变式，最终推导出正确的程序。这种方法依赖于后置断言拆分分解后的规约，在面对较复杂程序规约时，寻找子规约的难度较大，并且随着子规约的增多，推导过程会愈加繁琐。

Kourie等[14]设计了一种基于构建正确性的程序开发风格，这种开发风格结合了Dijkstra[11]的GCL(Guarded Command Language)语言和Morgan的精化演算规则，从问题的形式化规约开始，逐步将规约精化为代码。其推导过程的难点在于这些算法的推导基于循环不变式，其循环不变式在推导开始时通过推测得来。然而，循环不变式的开发是循环程序的难点，复杂程序的循环不变式往往较难获得[15]。

在文献[16]中，作者使用PAR(Partition-And-Recur)方法[9,17]从形式规约出发，使用量词的性质等作为规则构造出一组问题求解的递推关系，从而推导出一组查找算法程序。其推导过程揭露了线性查找和折半查找的思想，在保证程序正确性的同时，提高了相关算法程序的设计效率。文献阐述了常见的搜索算法的分划方式，但是并没有形成一套针对查找类问题的形式化推导方法。

综上所述，对算法的形式化推导的研究是一项很有意义的工作，以上针对形式化推导方法的研究都取得了相应成果，为该领域研究提供了重要参考。

3 序列折半划分问题的形式化推导方法

折半划分的前提要求为待划分序列必须有序。为将折半划分思想更加有效地应用到序列划分问题中，本文将序列进一步细分为“有序序列”和“循环序列”2种类型。针对这2种序列提出了序列折半划分问题的形式化推导方法。该方法结合程序求精思想，将推理与形式化方法相结合，从抽象程度高的程序规约出发，经过一系列的规约变换步骤，逐步降低规约的抽象程度，最终得到正确的Apla程序。整个过程可以概括为5个步骤，如图1所示。

Figure 1 Flow chart of formal derivation method forsequence dimidiate partition problem图1 序列折半划分问题的形式化推导方法流程图

图1中，步骤1通过Spec1或Spec2和相应的初始条件构成问题规约；步骤2根据问题本身的特点以及序列中间元素的值对问题的可能情况进行分划；步骤3对分划的结果进行规约变换与化简，形成问题的递推关系式；步骤4将递推关系式与初始条件结合得到问题的Radl(Recurrence-based algorithm design language)算法与循环不变式；步骤5将Radl算法等价转换为Apla程序。接下来对这5个步骤进行详细介绍。

3.1 构造程序规约

构造程序规约明确序列折半划分问题的目标，程序规约由前置断言(Q)和后置断言(R)构成，用于精确地描述算法要完成的工作。

针对折半划分问题先给出有序序列和循环序列的形式化定义。

定义1(有序序列) 有序序列指的是序列长度有限，在序列元素a[1],a[2],…,a[n]中，序列元素由小到大依次递增，且不存在重复元素的序列。有序序列使用形式化定义可以描述为:

Spec1≡(∀k,1≤k

(1)

其中，n为序列的长度。

定义2(循环序列) 如果在序列a[1],a[2],…,a[n]中存在某个i使得a[i]是序列中的最小元素，且序列a[i],a[i+1],…,a[n],a[1],…,a[n-1]是递增的，则称序列a[1],a[2],…,a[n]是循环序列。循环序列可以看作为2段有序序列的头尾相连，并且第2段中元素的最大值a[n]小于第1段中元素的最小值a[1]，循环序列使用形式化定义可以描述为：

Spec2≡(∃i,1

(∀p,q,1≤p

a[p]

a[q+1]∧a[n]

(2)

基于上述有序序列和循环序列的形式化定义,可以得出针对有序序列或循环序列这一类划分问题的形式化规约的一般形式：

Q:(Spec1|Spec2)∧初始条件

R:搜索结果。

根据该类问题规约的一般形式并结合待解决问题可以精确地刻画出问题的程序规约。

3.2 分划原问题

根据3.1节中的程序规约一般形式得出问题的程序规约后，将原问题进行分划，分划的核心思想为每一个子问题的解都可以由更小的子问题得出。基于这一思想，根据给定序列的特点，假设原问题为s(a,1,n),其中，1和n为序列的下标，代表原问题在范围a[1]～a[n]中寻找问题的解，通过序列中间位置下标(1+n)/2将序列分为前、后2个子序列，根据具体问题与中间位置的值a[(1+n)/2]将原问题逐步分解为2个结构相同且规模更小的子问题s(a,1,(1+n)/2)和s(a,(1+n)/2+1,n)。

若子问题总是可以被解决并且可以输出查找结果，则可以通过分划递推法进行设计，通过分析子问题的特征，构造求解规约并对规约进行变换,得到问题递推关系。该过程能够逐步正确推导出原问题的解。

针对序列类问题，分析给定序列的数学性质以及具体问题，可以对原问题进行分划，根据分划过程中可能出现的情况，分划过程的状态可以分为“修改分划范围”和“分划停止”2种：

(1)修改分划范围。

问题的初始范围[1,n]即原序列的长度。在执行过程中需要对范围进行更改，通过修改下标值的范围形成子问题。

(2)分划停止。

当成功搜索到目标值或子问题区间为一个点无法进一步分划时，分划停止，输出结果。

3.3 寻找递推关系

根据3.2节中分划过程的状态，可以得到问题的递推关系F:s(a,1,n)=F(C,s(a,j,k))，其中，s(a,j,k)是s(a,1,n)的子问题，s(a,j,k)和约束条件C通过递推关系F可以得到原问题s(a,1,n)的解。由此可以得到该类问题的通用递推关系，如式(3)所示：

(3)

约束条件C1,C2,…,Cn满足:

(∀i,j,1≤i,j≤n∧i≠j:Ci∧Cj=False)∧

C1∨C2∨…∨Cn=True

(4)

3.4 得到Radl算法和循环不变式

Radl是一种基于递推关系的算法设计语言，它的主要功能是描述问题的规约、规范变换规则和算法[18]。Radl算法是使用Radl语言描述的算法,Radl语言由算法规范语言和算法描述语言2部分组成。Radl被用作Apla语言的前端语言，使用传统的数学习惯，且具有引用透明性，便于算法的形式推导和证明。

Radl语言的一般形式如下所示：

Algorithm:〈算法名称〉

|[运算变量初始化定义]|

{Q∧R}〈算法规约〉

Begin:〈递推控制变量〉;〈变量初始化赋值〉

Termination:〈递推终止条件〉

Recur:〈递推关系式F〉

End

在得到递推关系之后，将递推关系中出现的函数和变量的初始化条件刻画出来，再把所有的递推关系、递推关系要满足的初始化条件和求解问题的描述规约合并成一个Radl算法。根据递推终止条件和递推关系式，分析循环前后的信息，找出循环相关变量的变化规律，最后运用条件选择断言式可以快速得到循环不变式，其通用形式如式(5)所示：

∧1≤j≤k≤n+1

(5)

3.5 将Radl算法转换为Apla程序

Apla是为实现算法程序形式化开发的一种抽象程序设计语言[19,20]，具有功能抽象、数据抽象和简单易用等特点。Apla程序可读性强，易于进行程序开发与形式化证明，且可以转换成各种可执行语言程序。

Radl语言是抽象程序设计语言Apla的前端语言，并且Radl和Apla中的标识符、关键字和符号的表达方式完全一致。本文通过剖析Radl算法特性，揭示用递推关系组表示的Radl算法与抽象顺序程序Apla间的本质关系，将Radl算法中无序的递推语句转化为顺序程序。基于Radl语法产生式的Apla程序生成规则和Apla程序自动生成系统,可以将Radl算法正确地转换为可读性好并且易于理解和验证的Apla程序[18]。

4 工具：Apla到C++程序自动生成系统

因Apla语言不能直接编译运行得到相应的结果，为Apla语言编写一个编译器难度较大，而且难以在不同机器间移植，编译器的正确性也难以得到保证。本文开发了一个自动程序转换系统，将抽象Apla算法程序转换成一个可执行程序，这样就可以通过编译得到运行结果，由于将编译成机器代码的工作交给了第三方编译器去完成，因而实现了算法程序的机器无关性，转换系统的可靠性也易于保证。

该系统集词法分析、语法分析、语义一致性分析、转换、编译和运行为一体，并为用户提供了一个应用界面，方便用户将Apla程序转换为正确的C++程序[21]，从而实现了从抽象到具体的程序求精过程。Apla到C++自动生成系统的总体结构如图2所示。

Figure 2 Overall structure of Apla to C++program automatic generation system 图2 Apla到C++程序自动生成统总体结构

5 2个折半划分搜索实例的推导与生成

5.1 有序序列搜索特殊下标

实例1问题描述：给定有序序列a[1],a[2],…,a[n]，试确定是否存在元素等于其下标值，即a[i]=i。若存在则将i设为其下标值，否则将i设为-1。

(1)构造程序规约。

根据3.1节中的形式化规约一般形式，将初始条件设为i=0可构造出如下规约：

Q:(∀k,1≤k

R:i=-1∨((∃k,1≤k≤n,a[k]=k)→i=k)

(2)分划原问题并寻找递推关系。

分划原问题：设原问题为s(a,1,n),代表在[1,n]中搜索。利用折半划分思想，搜索特殊下标过程从数组的中间元素开始，对原问题进行如下分划:

(6)

分别使用j和k来表示搜索空间的左边界和右边界，其中1≤j≤k≤n，可以得出该问题的一般形式,如式(7)所示：

(7)

式(7)将s(a,j,k)分划成2个子问题，表示s(a,j,k)的解可以通过s(a,j,(j+k)/2)和s(a,(j+k)/2+1,k)的F运算得到。

寻找递推关系：s(a,j,k)代表在[j,k]中搜索满足条件a[i]=i的i，分划的关键在于比较a[(j+k)/2]与(j+k)/2的大小。根据中间元素下标判断特殊下标i的位置，设中间元素下标为m，在此问题中，若a[m]

①若j=k，搜索区间变为固定点，直接判断点k是否为特殊下标。若点k是特殊下标，则将i设为k，否则将i设为-1。

②若(j+k)/2>a[(j+k)/2]，则将j设为(j+k)/2+1。

③若(j+k)/2≤a[(j+k)/2]，则将k设为(j+k)/2。

根据可能情况对形式化规约进行变换：

s(a,j,k)≡s(a,j,(j+k)/2)∨

s(a,(j+k)/2+1,k)∨k∨-1

{范围分裂}

s(a,j,k)≡(j=k∧(a[k]=k∧s(a,j,k))=k∨(a[k]≠k∧s(a,j,k)=-1))∨((j+k)/2>a[(j+k)/2]∧s(a,j,k)=s(a,(j+k)/2+1,k))∨((j+k)/2≤a[(j+k)/2]∧s(a,j,k)=s(a,j,(j+k)/2))

{分配律}

s(a,j,k)≡(s(a,j,k)=-1)∨(s(a,j,k)=x∧(∃x,j≤x≤k:a[x]=x))∨(j=k∧a[k]=k∧s(a,j,k)=k)∨(j=k∧a[k]≠k∧s(a,j,k)=-1)∨((j+k)/2>a[(j+k)/2]∧s(a,j,k)=s(a,(j+k)/2+1,k))∨((j+k)/2≤a[(j+k)/2]∧s(a,j,k)=s(a,j,(j+k)/2))

{化简}

s(a,j,k)≡s(a,j,(j+k)/2)∨s(a,(j+k)/2+1,k)∨k∨-1

化简后可得到递推关系，如式(8)所示:

s(a,j,k)=

(8)

Figure 3 Automatically generating ordered sequence search special subscript program图3 自动生成有序序列搜索特殊下标程序

(3)构造Radl算法和循环不变式。

根据式(8)和初始值，构造Radl算法，如算法1所示：

算法1实例1.Radl

输入：有序序列a[1],a[2],…,a[n]。

输出：特殊下标值i。

1. |[i,j,k:integer;a:array[1..n,integer];]|;

2. {Q∧R};

3.Begin：i,j,k=0,1,n;

4.Termination：j>k;

5.Recur：Formula (8);

6.End

根据式(8)和循环终止条件，并约束j和k的变化范围，将(j+k)/2用变量m表示，可以得出该程序的循环不变式,如式(9)所示：

ρ:a[m]≥m→s(a,j,k)=s(a,j,m)∨

a[m]

s(a,m+1,k)∧1≤j≤k+1≤n+1

(9)

(4)将Radl算法转换为Apla程序。

根据算法1和式(9)可得出如下Apla算法:

算法2实例1.Apla

输入：有序序列a[1],a[2],…,a[n]。

输出：特殊下标值i。

1.j:=1;k:=n;m:=(1+n)/2;i:=0;

2.do(j≤k)→m:=(j+k) div 2;

3.if(j=k)→if(a[j]=j)→i:=k;

4.[]→i:=-1;fi;j:=j+1;fi;

5.if(a[m]

6.if(a[m] ≥m)→k:=m;fi;

7.od;

(5)实例C++算法的自动生成。

将算法2输入到Apla到C++程序自动生成系统中，可以得到图3所示的转换结果。图3中，左侧代码对应算法的Apla程序，右侧代码为验证后自动生成的C++程序。

可以发现，相较于自动生成的C++程序，抽象算法程序Apla可以通过非常简短的语句来精确描述算法功能。对生成的2段C++代码随机输入测试数据，运行结果如图4所示。

Figure 4 Execution result of ordered sequence search special subscript program 图4 有序序列搜索特殊下标程序执行结果

经过验证，程序能够执行。由于Apla到C++系统可以确保Apla代码转换到C++代码过程的语义等价性，因此可以确定生成的C++程序是完全正确的，从而免于验证繁琐的C++程序，大幅提高了软件开发效率并保证了软件的可靠性和正确性。

5.2 循环序列搜索最小元素下标

实例2问题描述：对于一个已知的循环序列，找出其中最小元素的位置i。

(1)构造程序规约。

Q:(∃i,1

R:∀k,1≤k≤n:a[k]≥a[i]

(2)分划原问题并寻找递推关系。

分划原问题：将原问题设为s(a,1,n)，代表在[1,n]中寻找最小元素的位置i，为实现该算法，对原问题进行如下分划：

(10)

分别使用j和k来表示搜索空间的左边界和右边界可得出该问题的一般形式，如式(11)所示：

(11)

寻找递推关系：针对此问题，可以比较范围边界值a[j]和a[k]，其中ja[k]，则i就一定落在区间(j,k]中，因为在这个区间内，元素的顺序发生了跳变。通过这种分划方法，能在O(logn)次比较后找到i。分划的关键在于比较a[(j+k)/2]与a[k]的大小，故有3种可能情况：

① 若j=k，代表找到最小元素下标，搜索区间变为固定点，此时将i设为k;

② 若a[(j+k)/2]

③ 若a[(j+k)/2]>a[k]，代表该范围元素顺序发生跳变，此时将j设为(j+k)/2+1。

根据可能情况对形式化规约进行变换：

s(a,j,k)≡

(s(a,j,k)=i∧(mini:1≤i≤n:a[i]))

{范围分裂}

s(a,j,k)≡(j=k∧s(a,j,k)=k)∨(a[k]>a[(j+k)/2]∧s(a,j,k)=s(a,j,(j+k)/2))∨(a[k]

{分配律}

s(a,j,k)≡(s(a,j,k=-1)∨(s(a,j,k)=x∧(∃x,j≤x≤k:a[x]=x))∨(j=k∧a[k]=k∧s(a,j,k)=k)∨(j=k∧a[k]≠k∧s(a,j,k)=-1)∨(j+k)/2>a[(j+k)/2]∧s(a,j,k)=s(a,(j+k)/2+1,k)∨((j+k)/2≤a[(j+k)/2]∧s(a,j,k)=s(a,j,(j+k)/2))

{化简}

s(a,j,k)≡s(a,j,(j+k)/2)∨s(a,(j+k)/2+1,k)∨k

化简后可得到递推关系，如式(12)所示:

s(a,j,k)=

(12)

(3)构造Radl算法和循环不变式。

根据递推关系式(12)及初始值，可得解此问题的Radl算法，如算法3所示：

算法3实例2.Radl

输入：循环序列a[1],a[2],…,a[n]。

输出：特殊下标值i。

1.|[i,j,k:integer;a:array[1..n,integer];]|;

2.{Q∧R};

3.Begin：i,j,k=0,1,n;

4.Termination：j>k;

5.Recur:Formula (12);

6.End

根据式(12)和循环终止条件，并约束j和k的变化范围，将(j+k)/2用变量m代替，可以得出该程序的循环不变式，如式(13)所示：

ρ：a[k]>a[m]→s(a,j,k)=

s(a,j,m)∨a[k]

s(a,m+1,k)∧1≤j≤k+1≤n+1

(13)

(4)将Radl算法转换为Apla程序。

根据算法3和式(13)，可得出如下Apla算法：

算法4实例2.Apla

输入：循环序列a[1],a[2],…,a[n]。

输出：最小元素下标值i。

1.j:=1;k:=n;m:=(1+n)/2;i:=0;

2.do(j≤k)→m:=(j+k) div 2;

3.if(j=k)→i:=k;j:=j+1;fi;

4.if(a[m]

5.[]→j:=m+1;fi;

6.od;

(5)实例C++算法的自动生成。

将算法4输入到Apla到C++程序自动生成系统中，可以得到图5所示的转换结果。图6为自动生成的C++程序代码正确运行的结果。

Figure 5 Automatically generating loop sequence search minimum element subscript program图5 自动生成循环序列搜索最小元素下标程序

Figure 6 Execution result of loop sequence search minimum element subscript program 图6 循环序列搜索最小元素下标程序执行结果

6 结束语

本文以序列折半划分问题为研究对象，运用分划递推的核心思想，探讨该类问题的共性，提出了序列折半划分问题的形式化推导方法。通过“有序序列搜索特殊下标”和“循环序列搜索最小值下标”2个实例验证了本文方法的可行性。与现有研究相比，本文方法具有以下特点：

(1)运用规约变换技术对问题规约进行变换并严格保证一致性，免于繁琐的证明，使得推导过程更加简洁。

(2)该方法包括了完整的程序求精过程，实现了从程序规约到C++程序的完整转换过程。

(3)相较于以往的靠灵感和经验开发算法程序，本文把算法设计过程转变为规范化的算法程序生成过程，这一过程确保了程序的可靠性与正确性。