基于Isabelle定理证明器算法程序的形式化验证

Formal Verification of Algorithmic Programs Based on the Isabelle Theorem Prover

形式化验证对保证软件的正确性和可靠性具有十分重要的意义。定理机械证明是形式化验证的一个重要研究领域,Isabelle系统是一个被广泛运用的定理证明辅助工具。本文在分析Dijkstra最弱前置谓词理论的基础上,根据PAR方法开发的算法程序循环不变式,提出了一种使用Isabelle定理证明器对算法程序进行机械验证的方法。该方法既克服了传统手工验证过程的繁琐性和易错性等缺点,又达到"提高验证效率和保证算法程序高可信"的目标,具有很好的实用价值。

Formal verification plays an important role in ensuring software＇s correctness and dependability. Theorem＇s mechanical proof is a significant research domain of formal verification. The Isabelle system is generically considered as a useful tool for theorem proving. In this paper, according to the analysis of Dijkstra＇s weakest pre-condition theory and the algorithmic program＇s loop invariant developed by the PAR method, we offer a method of how to mechanically verify algo- rithmic programs based on Isabelle. The method not only overcomes the shortcomings of traditional manual verification, but also attains the goal of enhancing the dependability and efficiency of the verification process and ensuring the algorithmic programs＇ trustworthiness. Therefore, it is useful and valuable in practicability.