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

Research on New Strategy of Program Refinement and Automatic Verification Method

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

Traditional program refinement strategy could not be refined to executable program,which suffered from the low reliability of verification and insufficient automation.To solve the above problems,a more complete program refinement strategy and an automatic verification method were proposed.The recursive definition function technology was used to describe the problem specification.The program was refined to the IMP program based on Morgan refinement method,and the verification condition generator(VCG)was used to automatically generate the verification conditions.The correctness of the IMP program was verified by the Isabelle theorem prover.Finally,the development platform automatically generated the C++executable program.Taking the longest marker gene sequence problem as an example,the program refinement and automatic verification were carried out to test the effectiveness of the proposed strategy.This strategy could improve the correctness of algorithm program development and reduced the tedious workload of traditional verification.