由于本书的研究是PAR方法的一个重要组成部分，故在此，将对PAR方法做较为详细的阐述。图1-1 PAR方法开发过程略图PAR方法是一种基于分划和递推的部分形式化算法程序设计方法，支持算法程序开发的全过程。它包括四个组成部分：算法程序设计方法、基于递推关系的算法设计语言Radl、抽象程序设计语言Apla及一系列转换系统。由PAR方法的理论及上述对算法的推导，我们可以看出，PAR方法在克服软件危机方面将大有作为。......
2023-10-26
形式化构件装配的图算法生成
【摘要】：由于本书的研究是PAR方法的一个重要组成部分，故在此，将对PAR方法做较为详细的阐述。图1-1 PAR方法开发过程略图PAR方法是一种基于分划和递推的部分形式化算法程序设计方法，支持算法程序开发的全过程。它包括四个组成部分：算法程序设计方法、基于递推关系的算法设计语言Radl、抽象程序设计语言Apla及一系列转换系统。由PAR方法的理论及上述对算法的推导，我们可以看出，PAR方法在克服软件危机方面将大有作为。
由于本书的研究是PAR方法的一个重要组成部分，故在此，将对PAR方法做较为详细的阐述。
PAR方法是薛锦云教授在多年来承担国家“863计划”和国家自然科学基金课题的基础上，通过对现存算法程序设计方法局限性和大量算法程序特性的深入研究，发现寻找问题求解序列递推关系是开发简单而高效算法程序的有效途径，进而提出的一种统一实用的算法程序设计和证明方法。它的总体思想可用图1-1表示。
图1-1 PAR方法开发过程略图
PAR方法是一种基于分划和递推的部分形式化算法程序设计方法，支持算法程序开发的全过程。它的理论基础是Floyed、Hoare和Dijkstra的程序正确性证明理论。它包括四个组成部分：算法程序设计方法、基于递推关系的算法设计语言Radl（recurrence_based algorithm design language）、抽象程序设计语言Apla（abstract programming language）及一系列转换系统。
PAR方法开发算法和程序的全过程可以分成以下6步：
第1步，用自定义的算法设计语言Radl精确地描述待求解问题的功能规约。根据不同的需要，这种描述可以是形式化的，也可以是非形式化的。
第2步，把需求解的问题分划成若干和原问题结构相同但规模更小的子问题，分解可一直进行下去直至每个子问题可直接求解。可直接求解的子问题称为最小子问题。分划是求解复杂问题，得到快速算法的一般策略。
第3步，构造问题求解序列的递推关系Si=F（Sj），并给出在递推关系中出现的变量和函数的初值，然后将所有递推关系和初始化条件结合起来成为一个用算法设计语言Radl描述的抽象算法。
第4步，基于我们提出的循环不变式的新定义和开发新策略，在第3步所得递推关系的基础上，通过引入变量记录递推关系中函数的值，并约束循环控制变量的变化范围即构成了循环不变式。
第5步，基于所得的Radl算法和循环不变式开发抽象程序设计语言Apla书写的算法程序。用我们的Radl→Apla程序转换器可以机械地、自动地把Radl算法规范和Radl算法转换成Apla程序规范和Apla程序。
第6步，用我们的一系列程序转换器机械地、自动地把Apla程序转换为可执行的高级语言程序，如：Ada、C++、Delphi、Java等。
这种方法结合形式化方法和非形式化方法，能正确区分开发过程中的创造性劳动和非创造性劳动，充分利用特殊问题中使用的分划和递推技术，为我们有效地开发出正确的算法程序提供了理论和方法学的支持。
以下给出一个本人推导的算法实例来详细阐述运用PAR方法推导算法的过程。
问题：求n的m次方的末p位数。即给定自然数n，求它的m次方所得结果的末p位数是多少。
1.构造问题的规范
AQ：给定n＞0∧m＞0∧p＞0
用f（n，m，p）记n的m次方的末p位数，则
AR：f（n，m，p）=∏（i：1≤i≤m：n）mod∏（i：1≤i≤p：10）
2.分划原问题
根据题意，将原问题进行如下划分：
f（n，m，p）=F（f（n，m-1，p），m）
3.寻找递推关系
根据问题的规范及分划，用pp来记∏（i：1≤i≤p：10），则：
于是得到递推关系：f（n，m，p）=f（f（n，m-1，p）*f（n，1，p），1，p）
根据递推关系，我们得到如下解此问题的算法：(www.chuimin.cn)
4.构造循环不变式
用谓词精确表达上述循环变量的变化规律，让变量f存放f（n，m，p）的值，得到下列循环不变式：
f=f（n，i，p）∧1＜i≤m∧f1=f（n，1，p）∧pp=∏（i：1≤i≤p：10）
5.构造对应的程序
利用上述递推关系和循环不变式，可得如下的算法程序：
6.通过我们研制的Apla-＞Java程序自动转换系统，将上述抽象算法转换成如下的Java程序，经实际运行检测这个程序，结果完全正确。
由PAR方法的理论及上述对算法的推导，我们可以看出，PAR方法在克服软件危机方面将大有作为。PAR方法是一种能够设计快速算法的算法程序设计方法，通过递推关系，推导出来的算法总是使后一步的结果建立在前一步结果的基础上，避免了许多重复性的工作和计算；PAR不仅可以用来解决一些传统算法设计方法可以解决的问题，也可以解决用传统设计方法不能解决的问题；循环不变式是理解和开发算法程序的关键，但产生循环不变式的过程仍然需要创造性劳动的参与，PAR方法在此过程中起到了关键性的指导作用：当一个问题的递推关系得到后，利用一些变量来记录递推关系中出现的函数值，并约束变量的变化范围即成为循环不变式，这克服了传统算法设计方法无法提供循环不变式的缺点。
在PAR方法中，定义了大量的泛型机制，泛型机制为设计组合数据类型及相关操作提供了可能性，主要的Apla泛型机制的实现分为：类型参数化和子程序参数化。
（1）类型参数化
在Apla语言中，如果想要对某个程序名的类型参数、类型变量、过程函数的参数返回值类型进行定义，可以采用关键字sometype来操作。如果想要泛型化的程序，也可以采用在类型声明中以参数的形式来直接说明组合数据类型的基本类型。在Apla中，可采用下列这种形式定义泛型程序的语法结构：
program＜程序名＞（sometype＜类型参数＞）；
设计好泛型程序之后，如果想要使用某个泛型程序设计具体的算法，需要对其进行实例化，即要将原本的类型参数替换为具体的类型参数。Apla中实例化的语法结构为：
program＜新程序名＞：new＜程序名＞（具体的类型参数）；
Apla类型参数化的使用为不同类型的实例化操作提供便利和简捷。
（2）子程序参数化
在Apla语言中，声明过程参数和函数参数需要分别使用func和proc这两个关键字。之所以子程序能被泛型化，是因为Apla语言允许子程序带有各种参数：普通值参或类型参数。另外，子程序也可以作为子程序的参数。当子程序作为参数时，由func和proc所定义的程序头被当作程序中过程或函数的形参表来使用。在Apla中，采用下列这种形式定义子程序参数化的语法结构：
procedure＜过程名＞|function＜函数名＞（形参表）；
如果想要使用泛型子程序，必须先对其进行实例化操作。进行实例化操作之后，才能得到原本类型和子程序参数的具体内容。在进行实例化操作的过程中，泛型子程序中的形参表必须得到具体的类型。必须强调的是，进行实例化时，无论是参数的个数还是参数的类型，实参与形参必须完全一致，否则程序就会出错。在Apla中，实例化泛型子程序的语法结构如下：
procedure［function］＜新过程名或新函数名＞：new＜泛型过程名＞（＜类型实参表＞|＜子程序实参表＞）；
基于对Apla语言的泛型特点的研究可以看出，Apla语言最显著的特点是能简洁、良好地描述和开发复杂算法程序，使用Apla泛型设计出的算法结构具有很高的可重用性。
有关形式化构件装配的图算法生成的文章
- 详细阅读
-
形式化构件装配图算法生成详细阅读
20世纪80年代以来，形式化软件开发方法的研究及应用为解决上述问题找到了一条有效的途径，使用形式化方法开发软件可以提高软件的可读性、可靠性和可维护性以及软件的开发效率，并为实现软件开发的自动化奠定基础。软件开发的形式化方法是以一般形式化方法为基础的。尤其适宜高安全性系统的开发，这也是形式化方法目前最主要的应用领域。另外，某些形式化方法缺乏描述软件结构的强有力机制，对大型软件的开发不太理想。......
2023-10-26
-
广度优先搜索在形式化构件装配中的应用详细阅读
在图领域，广度优先搜索常被用于求解图的最短路径问题中。松弛操作的伪代码如下：2.Floyd算法Floyd算法是一个经典的全源最短路径算法，适用于不包括负环的图，可以应用于计算所有城市之间的交通道路距离问题。Floyd算法利用了上述两个假设之间的关系，该关系依赖于节点k是否是路径p上的一个中间节点。k=0则表示这两个节点是直接相连的，没有中间节点。......
2023-10-26
-
深度优先搜索在形式化构件装配中的应用详细阅读
在实际应用中，很多算法都体现了深度优先搜索的思想。图3-2 有向图的邻接表表示2.拓扑排序深度优先搜索的另一个经典应用是对有向无环图进行拓扑排序。这两次深度优先搜索一次运行在图G上，一次运行在转置图GT上。算法计算的结果是深度优先森林，每一个强连通分量对应一棵深度优先树。......
2023-10-26
-
多目标进化算法形式化描述详细阅读
下面介绍进化算法的相关定义和统一的描述框架[1]。对于各种进化计算方法，存在一个非空集合I，I称为这个进化计算的个体空间。D的值域确定了进化计算的实际搜索范围。随机函数被称为随机种群变换，其中Ω为采样空间。遗传算法是目前研究的进化算法中三种典型算法之一，其他两种分别是进化规划和进化策略。进化规划的特点在于没有使用交叉算子，采用随机选择机制，因而变异在进化过程中占据重要地位。......
2023-11-26
-
多序列比对算法形式化实现详细阅读
本节根据MSAA的特征模型和渐进式比对算法构件的交互模型，利用Apla语言的高抽象性、对泛型及ADT的良好支持以及易于正确性验证等优点，来形式化实现多序列比对算法构件。prog构件该构件为ADT类型HMSAA中的泛型子程序，根据传入不同类型的计算比对步骤进行渐进式比对。result_op构件该构件为ADT类型，泛型子程序multiAlign_op在多序列比对结果的基础上，对结果进行格式化输出。......
2023-10-25
-
多序列比对算法的形式化开发方法详细阅读
变换的开始、中间到结束、产物是一符号串，这种形式化方法称为完全形式化方法。所以，目前软件开发的形式化方法主要是以部分形式化方法为主。总体上，形式化软件开发方法大致可分为以下五类：基于模型的方法。......
2023-10-25
-
生成角点标记图的方法详细阅读
标记图是一种一维函数的边界表达方法，其典型的生成方法是将从质心到边界线的距离转化成一个角度函数，如图7-8所示。本书提出的角点标记图将标记图的基本思想应用于构造角点特征的过程中，并在保存目标基本信息的同时消除其对尺寸和旋转的依赖性，使得该特征具有平移不变形、比例不变性和旋转不变性。这种模式向量的生成方法依赖于旋转和比例缩放变换。......
2023-06-28
相关推荐