基于PAR的高可信装备保障算法推演

算法被誉为计算的“灵魂”（spirit of computing），算法程序的可靠性和正确性对软件系统的可信度起着至关重要的作用。动态规划、贪心、分支限界等传统的算法设计策略缺乏有效的选择标准，一些算法形式化开发方法和工具的应用水平和范围也很有限，因此算法的可靠性已成为高可信软件系统的一个主要瓶颈。 作为军事运筹学的一个重要分支，装备保障计算主要研究军事活动中装备领域的决策优化问题，保障计算软件特别是算法的可靠性在很大程度上决定了装备保障的效率乃至军事行动的成败。利用形式化软件工程的研究成果、特别是引入算法程序的形式化开发方法，对我军通用装备保障领域中的大量算法类问题进行有效求解，有利于优化保障结构、统筹保障资源、整合保障力量、提高保障时效，促进装备整体战斗力水平的提升。 本文以高可信软件开发方法PAR为基础，面向装备保障计算的领域需求，提出了一类离散最优化问题（discrete optimization problem, DOP）的结构模型和算法推演技术，并成功推演了一系列典型的装备保障算法。本论文的主要创新性贡献如下： （1）定义了DOP的结构模型，提出了基于单点结构（Singleton）的问题分划递推策略，进而通过PAR算法推演生成问题的高效求解算法，涵盖了多种传统算法设计策略，显著提高了算法程序设计的机械化水平。 （2）提出了描述DOP分划递推过程的问题简约图（problem reduction graph, PRG）模型，并针对典型DOP结构推演得到了一组PRG构造算法模式，其中每个算法模式都涵盖了满足特定代数结构性质的一大类具体问题。 （3）阐述了PAR算法推演的范畴模型，为算法设计和重用提供了抽象而有效的方法指导。 （4）对我军通用装备保障领域具有代表性的48个问题进行了形式化的算法推演，构建了领域算法库。 （5）在PAR平台的基础上设计了装备保障算法开发平台的原型COPALM，支持DOP算法推演和重用，进而提高了相关应用软件的开发效率。

基于PAR的算法形式化开发

形式化方法是构建可信软件的重要途径.基于对算法问题的分析,针对形式化方法PAR开发算法的特征,刻划了问题分划、递推关系构造方面的规律.从一类问题的形式化功能规约出发,可机械地完成问题的分划及规约的变换,自然地揭示出求解问题的算法思想,在相关工具的支持下自动生成算法程序.研究结果将算法设计中尽可能多的创造性劳动转化为非创造性劳动,降低了形式化求解算法问题的难度,提高了算法程序的可靠性和形式化开发效率.

PAR方法和循环不变式的范畴语义

范畴论对理解程序规约及程序设计和正确性证明十分有用.PAR方法则是建立在严格的数学基础之上的一种统一的算法程序设计方法.循环不变式在循环算法程序的设计中至关重要.使用格理论和范畴论作为工具对PAR方法建立一个理论框架,并对其用范畴论的概念加以解释,从而使得PAR有更强的理论基础.在此基础上引入不动点原理深入刻划循环不变式的含义,循环不变式可以表示为谓词泛函的最小不动点,并从范畴论的角度解释该过程.