基于PAR的算法形式化开发  

PAR-Based Formal Development of Algorithms

作　　者：石海鹤[1,2,3] 薛锦云[1,2] 

机构地区：[1]中国科学院软件研究所计算机科学国家重点实验室,北京100190 [2]江西师范大学省高性能计算技术重点实验室,南昌330022 [3]中国科学院研究生院,北京100049

出　　处：《计算机学报》2009年第5期982-991,共10页Chinese Journal of Computers

基　　金：国家自然科学基金(60573080,60773054);科学技术部国际科技合作计划项目(2008DFA11940);江西省自然科学基金(2008GQS0056)资助~~

摘　　要：形式化方法是构建可信软件的重要途径.基于对算法问题的分析,针对形式化方法PAR开发算法的特征,刻划了问题分划、递推关系构造方面的规律.从一类问题的形式化功能规约出发,可机械地完成问题的分划及规约的变换,自然地揭示出求解问题的算法思想,在相关工具的支持下自动生成算法程序.研究结果将算法设计中尽可能多的创造性劳动转化为非创造性劳动,降低了形式化求解算法问题的难度,提高了算法程序的可靠性和形式化开发效率.Formal method is an important approach for construction of the trustworthy software. Based on the analysis of algorithmic problems and the features of formal method PAR, the laws of problem partition and recurrence relation construction are described. From a class of problem formal functional specification, the problem partition and the specification transformation can be done mechanically, the ideas behind algorithmic solutions can be discovered naturally, and further the resultant algorithmic programs can be produced automatically by means of tools. The research result makes as much creative work as possible converted into routine work, and the difficulty of formal algorithmic problem solving is reduced substantially, thus enables the improvement of reliability and productivity of algorithmic programs.

关 键 词：算法 形式化方法 PAR 规约 可信软件 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]