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

来源：计算机工程与科学杂志2022年第6期北京时间：

作者：左正康, 梁赞杨, 苏崴, 黄箐, 王渊, 王昌晶

单位：1.江西师范大学计算机信息工程学院,江西 南昌330022;2.江西师范大学软件学院,江西 南昌330022

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

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

基金资助：国家自然科学基金(61862033,61902162);江西省自然科学基金(20202BABL202026,20202BABL202025,20202BAB202015);江西省教育厅科学技术重点研究项目（GJJ210307）