摘要
形式化验证对保证软件的正确性和可靠性具有十分重要的意义。定理机械证明是形式化验证的一个重要研究领域,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.
出处
《计算机工程与科学》
CSCD
北大核心
2009年第10期85-89,共5页
Computer Engineering & Science
基金
国家自然科学基金资助项目(60573080,60773054)
科技部国际科技合作资助项目(2008DFA11940)