终止证明方法在形式化建模中的应用

Application of Termination Proof Method in Formal Modeling

随着形式化方法的普及和应用,定理证明器HOL4在形式化建模过程中无法自动完成终止证明的情况越来越多,而手动终止证明又缺少通用的证明思路.针对这种情况,提出规范化的手动终止证明方法.该方法从问题产生的本质入手,首先保证目标具备解决终止问题的必要条件,然后通过等效替换简化证明目标,最后以原有定理库为基础,寻找证明过程中缺失的引理,推进证明.实例表明,该方法逻辑清晰,能够有效地解决HOL4中大部分情况下的手动终止证明问题.

With the popularization and application of formal methods, there are increasingly more cases in which the theorem prover HOL4 cannot automatically complete the termination proof in the process of formal modeling. Manual termination proof still lacks a general idea. In response, a standardized manual termination proof method is proposed.Starting from the nature of the problem, the method guarantees that the target has the necessary conditions for solving the termination problem. Then, the proof target is simplified by equivalent substitution. Finally, on the basis of the original theorem library, the lacking lemma in the proof process is found to advance the proof. The example shows that this method has a clear logic and can solve the manual termination proof problem of the HOL4 in most cases.