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

摘要：

形式化推导是在程序正确性证明理论下所进行的程序开发,最终得到完全正确的算法程序.针对序列折半划分问题,现有的形式化推导方法将推导与证明交替进行,推导过程繁琐且大多无法直接获得可执行程序.为解决上述问题,提出了一种新的序列折半划分问题的形式化推导方法.该方法基于分划递推的核心思想,应用规约变换技术对问题规约进行变换并严格保证一致性,使得在推导过程中无需交替证明,进而导出递推关系式并得到高可靠性抽象算法程序Apla,最终通过转换工具自动生成可执行程序.实现了从程序规约到具体可执行程序的完整程序求精过程.以2个序列算法为例,验证了该方法的有效性和可行性,对相关问题的形式化推导具有指导意义.

关键词：折半划分、形式化推导、分划递推、程序求精

所属期刊栏目：44

分类号：TP311.5(计算技术、计算机技术)

资助基金：国家自然科学基金;国家自然科学基金;江西省自然科学基金;江西省自然科学基金;江西省自然科学基金;江西省教育厅科学技术重点研究项目

在线出版日期：2022-06-29（万方平台首次上网日期，不代表论文的发表时间）

页数：共9页

页码：1063-1071