典型文献
序列折半划分问题的形式化推导
文献摘要：
形式化推导是在程序正确性证明理论下所进行的程序开发,最终得到完全正确的算法程序.针对序列折半划分问题,现有的形式化推导方法将推导与证明交替进行,推导过程繁琐且大多无法直接获得可执行程序.为解决上述问题,提出了一种新的序列折半划分问题的形式化推导方法.该方法基于分划递推的核心思想,应用规约变换技术对问题规约进行变换并严格保证一致性,使得在推导过程中无需交替证明,进而导出递推关系式并得到高可靠性抽象算法程序Apla,最终通过转换工具自动生成可执行程序.实现了从程序规约到具体可执行程序的完整程序求精过程.以2个序列算法为例,验证了该方法的有效性和可行性,对相关问题的形式化推导具有指导意义.
文献关键词：
折半划分;形式化推导;分划递推;程序求精
中图分类号：
作者姓名：
左正康;梁赞杨;苏崴;黄箐;王渊;王昌晶
作者机构：
江西师范大学计算机信息工程学院,江西 南昌 330022;江西师范大学软件学院,江西 南昌 330022
文献出处：
引用格式：
[1]左正康;梁赞杨;苏崴;黄箐;王渊;王昌晶-.序列折半划分问题的形式化推导)[J].计算机工程与科学,2022(06):1063-1071
A类：
折半划分,形式化推导,分划递推,程序求精
B类：
程序正确性,明理,程序开发,完全正确,推导方法,接获,可执行程序,核心思想,规约,递推关系式,高可靠性,Apla,换工,自动生成
AB值：
0.183593
相似文献
机标中图分类号，由域田数据科技根据网络公开资料自动分析生成，仅供学习研究参考。
