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