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

Formal Verification of Algorithmic Programs Based on the Isabelle Theorem Prover

作　　者：游珍[1] 薛锦云[1,2] 

机构地区：[1]江西师范大学省高性能计算技术重点实验室,江西南昌330022 [2]中国科学院软件研究所。北京100190

出　　处：《计算机工程与科学》2009年第10期85-89,共5页Computer Engineering & Science

基　　金：国家自然科学基金资助项目(60573080,60773054);科技部国际科技合作资助项目(2008DFA11940)

摘　　要：形式化验证对保证软件的正确性和可靠性具有十分重要的意义。定理机械证明是形式化验证的一个重要研究领域,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.

关 键 词：形式化验证 定理机械证明 Dijkstra最弱前置谓词理论 PAR方法 算法程序 定理证明器 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]