典型文献
程序求精新策略及自动验证方法研究
文献摘要：
传统的程序求精策略无法求精至可执行程序,且存在验证的可信度低和自动化程度不高的问题.针对上述问题,提出一种较完整的程序求精策略并给出自动验证方法.使用递归定义函数技术刻画问题规约,基于Morgan精化规则程序求精至IMP程序,并使用验证条件生成器(verification condition generator,VCG)自动生成验证条件,通过Isabelle定理证明器验证IMP程序的正确性,最后利用开发平台自动生成C++可执行程序.以最长标志基因序列问题为实例进行程序求精和自动验证,检验了所提策略的有效性.该策略提高了算法程序开发的正确性,减轻了传统验证烦琐的工作量.
文献关键词：
程序求精;自动验证;Isabelle定理证明器;Morgan精化规则
中图分类号：
作者姓名：
左正康;黄志鹏;黄箐;王渊;王昌晶
作者机构：
江西师范大学 计算机信息工程学院 江西 南昌 330022;江西师范大学 软件学院 江西 南昌 330022
文献出处：
引用格式：
[1]左正康;黄志鹏;黄箐;王渊;王昌晶-.程序求精新策略及自动验证方法研究)[J].郑州大学学报（理学版）,2022(05):1-7
A类：
程序求精
B类：
自动验证,验证方法,可执行程序,可信度,较完整,递归,规约,Morgan,精化,IMP,生成器,verification,condition,generator,VCG,自动生成,Isabelle,定理证明,明器,开发平台,C++,标志基因,基因序列,程序开发,烦琐
AB值：
0.371755
相似文献
机标中图分类号，由域田数据科技根据网络公开资料自动分析生成，仅供学习研究参考。
