程序求精新策略及自动验证方法研究

传统的程序求精策略无法求精至可执行程序,且存在验证的可信度低和自动化程度不高的问题.针对上述问题,提出一种较完整的程序求精策略并给出自动验证方法.使用递归定义函数技术刻画问题规约,基于Morgan精化规则程序求精至IMP程序,并使用验证条件生成器(verification condition generator,VCG)自动生成验证条件,通过Isabelle定理证明器验证IMP程序的正确性,最后利用开发平台自动生成C++可执行程序.以最长标志基因序列问题为实例进行程序求精和自动验证,检验了所提策略的有效性.该策略提高了算法程序开发的正确性,减轻了传统验证烦琐的工作量.