论文部分内容阅读
摘要：通过对其现状和前景的介绍，引出PAR的方法，从而对构造递推关系进行研究，进行初步的探讨。
关键词：PAR；算法；形式；探讨
中图分类号：TP301文献标识码：A文章编号：1007-9599 (2013) 06-0000-02
1现状前景介绍
随着社会信息技术的逐渐增强，人们对于信息化的需求也逐渐增强。对于信息技术里面的计算机软件相关的可信性被置于一个非常重要的高度。对于计算机的软件可信性国内外都有了很重要的探讨。作为学术界重要人物之一的Hoare在他欧美同行的辅助下，组织构建了有关软件验证方面的国际性项目，这个验证软件VerifledSoftware被认为是这个世纪具有重大挑战的软件。关于软件的可信性的需求已经被放置到了重要的位置。在一些重要的国防以及航空航天和医疗器械等方面都有重要的运用，在能源以及通信和财经或者是一些制造业的关键领域，其中软件的正确性成为可信软件的重要性质。
算法是软件的核心，一直被叫做是“计算机的灵魂”，这个软件算法的正确性，是提高系统整个可信度重要环节。根据相关的统计表明，在传统的和非正式化这种方法在软件质量安全会又一个不能超越的峰点。对于形式化方法方面的实践表明，这样形式化的方法是实现软件安全性能保障的重要方法。
因为整个算法会牵涉创造性劳动方面，对于形式化方面的开发算法依然是计在算机领域之中极具挑战性的重要问题，这个方针是对形式化的方法PAR开发以及算法的重要特征，这就很好反应关于问题的分划和推递关系以及构造方面的规律，这就需要从问题的形式化相关功能规约作为出发点，对于问题的分划和规约的变换可以比较机械地完成，从而自然地揭示出求解问题方面的算法和思想，对于自然地揭示出相关求解问题的算法以及思想，也就能自动地出现高效的求解问题相关算法程序。
下面我们首先会需要介绍的是PAR方法，我们需要重点介绍和分析这里面出现的，形式化方面的功能规约机制以及拓展算法程序的重要方法。之后依据对于问题方面的分析，详细的陈述我们提出的问题，进而划分和规约变换策略。
2PAR方法
所谓PAR方法，是一种全新形式的设计方法，具有统一性特征。这种方法涉及到各种各样的算法及设计技巧，包括穷举法、贪心法等，这些都可以运用到程序开发的整个过程中。另外，应用算法程序，就是利用已经实现的程序或者相对抽象的程序，对语言进行重新描述与设计。这样的方法需要有四个有机部分组成。包括自定义泛型方面的算法设计语言以及泛型抽象相关的程序设计方面的语言，和系统的算法以及程序设计有效方法学和转换工具有效的集成组成。在这里面，PAR从问题的出发点设计出Radl算法的全过程提供了对形式化方面的支持。在Radl算法通过Apla相关的程序，就可以执行语言方面程序的生成，给这些准备了自动化方面的支持。如下图所示：
2.1形式化功能规约
算法程序的起点就是形式化相关功能方面的规约。Radl语言的重要功能就是对问题的规约进行描述，对于规约变换方面的规则和描述算法进行描述。它是由算法规约语言以及算法描述语言这两个部分有机成的。Radl能够提供丰富抽象的机制，可以对问题的功能进行足够集中的刻划。不能被设计以及现实相关的问题干扰。一般会采取如下的Radl算法相关的规约以及刻划形式：
这里面的标示符中的说明部分重要的作用是用来说明前和后置断言之中，会出现的变量以及函数的属性和类别，属性大致有三种。第一种是输入变量，需要用关键的字in进行标识。第二种是输出变量，需要用关键字out来进行标识。第三种是辅助变量，需要借助关键字aux进行标识。类型可以在Radl语言之中的相关标准数据以及类型和关于自定义方面的简单类型以及预定义重要的ADT类型和自定义ADT方面的类型。
上面提及的以AQ和AR开头相关的谓词表示意义分别是算法前置言以及后置断言，选择标识算法属于参数需要满足的条件加上算法的输出需要满足的条件都是一阶谓词逻辑方面的公式。使用的一致格式是a：r(i)：(i))表示“在范围r(i)上，对函数，(i)施行q运算所得的量”。其中Q是对q运算的一般化表示，能表述为V(也就是全称量词)，j(也就是存在量词)，MIN(也就是求最小值量词)，MAX(表示的是求最大值量词)，Σ(代表求和量词)，II(表示求积量词)等。这些每一个对应的q运算都是V，rain，max，+，*等。运用量词相关性质就可以抵御规约做以及等价方面的有效变换，运用用揭露问题求解的思想，在这里用到的性质主要有：
2.2开发算法程序的方法
基于递推相关的概念，运用PAR开发进行算法以及循环不变式和程序的全过程。可以分为5步。第一步是构造求解方面的问题。也就是Radl功能规划，第二步是把要求求解的问题分割为若干的原问题以前结构一样，但是规模需要更加细小的子问题。第三步是依照分割的形式对于功能规约做好变换，用来构造问题实现求解的序列来构建递推关系。第四步是在递推关系基础上，总结Radl算法，并依据我们涉及的循环不变式相关的新定义，以及新开发策略构造循环不变式。第五步是基于上面得到的Radl算法和循环不变式相关的开发Apla抽象程序，据此，进一步转换出一些可以执行的语言相关的程序。
3构造递推关系
我们一般都是通过对于规约相关的等价交换，来实现构造递推关系。为了减少在变换约束集中盲目地进行搜索和尝试，一个能够有效指导变换规则和适当选取以及应用的策略就变得很有必要。依据对与递推关系相关的构造整个过程已有的研究，易于得到一些启发，得到规约变换相关的策略。它所列举的规约变换时相关规则的应用方面的顺序，让变换的整个过程变得有序，除此之外，也让整个变换相关过程朝着分划指定设定的方向前行。
上面提及的工作都没能系统的进行刻划算法相关设计的规律。虽然Clark和Darling极早就指出，运用推导已知算法的方式，来实现积累以及有关推导路径方面的经验，运用更改和推导路径来发现新的算法。目前相关的研究还只能导致现在已知算法的出现。
4结束语
形式化方法，是整个软件开发之中重要的可信软件相关技术方面的一部分，但是算法对于可信性的得知和保证拥有着不能替代的作用。但是它还处在不断的实验之中，使用的用户大多是专家型用户，怎样减少形式化开发算法方面的难度，这是一件有长远利益的事。算法相关的形式开发是计算这个机领域里面极具挑战性的问题，我们需要通过实践不断积累经验，实现不断改进，来促进PAR方法对于可信软件在开发之中的运用，不断提高其在软件工程之中的实际效能。
参考文献：
[1]杨晨,薛锦云,苏昭.三个经典数学问题的形式化开发[J].计算机与现代化,2010(8).
[2]杨晨,薛锦云.关系代数派生算子语义表达式问等价性证明[J].计算机科学与探索,2008(1).
[3]万松松,薛锦云,谢武平.循环不变式开发技术研究[J].计算机工程与科学,2010(9).
[4]胡启敏,薛锦云.若干算法程序的形式化推导与生成技术研究[J].计算机研究与发展,2008(21).
[5]王昌晶,薛锦云.一类0-1背包问题算法程序的形式化推导[J].武汉大学学报(理学版),2009(6).
关键词：PAR；算法；形式；探讨
中图分类号：TP301文献标识码：A文章编号：1007-9599 (2013) 06-0000-02
1现状前景介绍
随着社会信息技术的逐渐增强，人们对于信息化的需求也逐渐增强。对于信息技术里面的计算机软件相关的可信性被置于一个非常重要的高度。对于计算机的软件可信性国内外都有了很重要的探讨。作为学术界重要人物之一的Hoare在他欧美同行的辅助下，组织构建了有关软件验证方面的国际性项目，这个验证软件VerifledSoftware被认为是这个世纪具有重大挑战的软件。关于软件的可信性的需求已经被放置到了重要的位置。在一些重要的国防以及航空航天和医疗器械等方面都有重要的运用，在能源以及通信和财经或者是一些制造业的关键领域，其中软件的正确性成为可信软件的重要性质。
算法是软件的核心，一直被叫做是“计算机的灵魂”，这个软件算法的正确性，是提高系统整个可信度重要环节。根据相关的统计表明，在传统的和非正式化这种方法在软件质量安全会又一个不能超越的峰点。对于形式化方法方面的实践表明，这样形式化的方法是实现软件安全性能保障的重要方法。
因为整个算法会牵涉创造性劳动方面，对于形式化方面的开发算法依然是计在算机领域之中极具挑战性的重要问题，这个方针是对形式化的方法PAR开发以及算法的重要特征，这就很好反应关于问题的分划和推递关系以及构造方面的规律，这就需要从问题的形式化相关功能规约作为出发点，对于问题的分划和规约的变换可以比较机械地完成，从而自然地揭示出求解问题方面的算法和思想，对于自然地揭示出相关求解问题的算法以及思想，也就能自动地出现高效的求解问题相关算法程序。
下面我们首先会需要介绍的是PAR方法，我们需要重点介绍和分析这里面出现的，形式化方面的功能规约机制以及拓展算法程序的重要方法。之后依据对于问题方面的分析，详细的陈述我们提出的问题，进而划分和规约变换策略。
2PAR方法
所谓PAR方法，是一种全新形式的设计方法，具有统一性特征。这种方法涉及到各种各样的算法及设计技巧，包括穷举法、贪心法等，这些都可以运用到程序开发的整个过程中。另外，应用算法程序，就是利用已经实现的程序或者相对抽象的程序，对语言进行重新描述与设计。这样的方法需要有四个有机部分组成。包括自定义泛型方面的算法设计语言以及泛型抽象相关的程序设计方面的语言，和系统的算法以及程序设计有效方法学和转换工具有效的集成组成。在这里面，PAR从问题的出发点设计出Radl算法的全过程提供了对形式化方面的支持。在Radl算法通过Apla相关的程序，就可以执行语言方面程序的生成，给这些准备了自动化方面的支持。如下图所示：
2.1形式化功能规约
算法程序的起点就是形式化相关功能方面的规约。Radl语言的重要功能就是对问题的规约进行描述，对于规约变换方面的规则和描述算法进行描述。它是由算法规约语言以及算法描述语言这两个部分有机成的。Radl能够提供丰富抽象的机制，可以对问题的功能进行足够集中的刻划。不能被设计以及现实相关的问题干扰。一般会采取如下的Radl算法相关的规约以及刻划形式：
这里面的标示符中的说明部分重要的作用是用来说明前和后置断言之中，会出现的变量以及函数的属性和类别，属性大致有三种。第一种是输入变量，需要用关键的字in进行标识。第二种是输出变量，需要用关键字out来进行标识。第三种是辅助变量，需要借助关键字aux进行标识。类型可以在Radl语言之中的相关标准数据以及类型和关于自定义方面的简单类型以及预定义重要的ADT类型和自定义ADT方面的类型。
上面提及的以AQ和AR开头相关的谓词表示意义分别是算法前置言以及后置断言，选择标识算法属于参数需要满足的条件加上算法的输出需要满足的条件都是一阶谓词逻辑方面的公式。使用的一致格式是a：r(i)：(i))表示“在范围r(i)上，对函数，(i)施行q运算所得的量”。其中Q是对q运算的一般化表示，能表述为V(也就是全称量词)，j(也就是存在量词)，MIN(也就是求最小值量词)，MAX(表示的是求最大值量词)，Σ(代表求和量词)，II(表示求积量词)等。这些每一个对应的q运算都是V，rain，max，+，*等。运用量词相关性质就可以抵御规约做以及等价方面的有效变换，运用用揭露问题求解的思想，在这里用到的性质主要有：
2.2开发算法程序的方法
基于递推相关的概念，运用PAR开发进行算法以及循环不变式和程序的全过程。可以分为5步。第一步是构造求解方面的问题。也就是Radl功能规划，第二步是把要求求解的问题分割为若干的原问题以前结构一样，但是规模需要更加细小的子问题。第三步是依照分割的形式对于功能规约做好变换，用来构造问题实现求解的序列来构建递推关系。第四步是在递推关系基础上，总结Radl算法，并依据我们涉及的循环不变式相关的新定义，以及新开发策略构造循环不变式。第五步是基于上面得到的Radl算法和循环不变式相关的开发Apla抽象程序，据此，进一步转换出一些可以执行的语言相关的程序。
3构造递推关系
我们一般都是通过对于规约相关的等价交换，来实现构造递推关系。为了减少在变换约束集中盲目地进行搜索和尝试，一个能够有效指导变换规则和适当选取以及应用的策略就变得很有必要。依据对与递推关系相关的构造整个过程已有的研究，易于得到一些启发，得到规约变换相关的策略。它所列举的规约变换时相关规则的应用方面的顺序，让变换的整个过程变得有序，除此之外，也让整个变换相关过程朝着分划指定设定的方向前行。
上面提及的工作都没能系统的进行刻划算法相关设计的规律。虽然Clark和Darling极早就指出，运用推导已知算法的方式，来实现积累以及有关推导路径方面的经验，运用更改和推导路径来发现新的算法。目前相关的研究还只能导致现在已知算法的出现。
4结束语
形式化方法，是整个软件开发之中重要的可信软件相关技术方面的一部分，但是算法对于可信性的得知和保证拥有着不能替代的作用。但是它还处在不断的实验之中，使用的用户大多是专家型用户，怎样减少形式化开发算法方面的难度，这是一件有长远利益的事。算法相关的形式开发是计算这个机领域里面极具挑战性的问题，我们需要通过实践不断积累经验，实现不断改进，来促进PAR方法对于可信软件在开发之中的运用，不断提高其在软件工程之中的实际效能。
参考文献：
[1]杨晨,薛锦云,苏昭.三个经典数学问题的形式化开发[J].计算机与现代化,2010(8).
[2]杨晨,薛锦云.关系代数派生算子语义表达式问等价性证明[J].计算机科学与探索,2008(1).
[3]万松松,薛锦云,谢武平.循环不变式开发技术研究[J].计算机工程与科学,2010(9).
[4]胡启敏,薛锦云.若干算法程序的形式化推导与生成技术研究[J].计算机研究与发展,2008(21).
[5]王昌晶,薛锦云.一类0-1背包问题算法程序的形式化推导[J].武汉大学学报(理学版),2009(6).