算法的形式化推导与基于Isabelle的自动化验证  

The Formal Derivation of Algorithm and Automatic Verification Based on Isabelle

作　　者：齐蕾蕾[1] 杨庆红[1] 游颖 QI Leilei;YANG Qinghong;YOU Ying(College of Computer Information Engineering,Jiangxi Normal University,Nanchang Jiangxi 330022,China)

机构地区：[1]江西师范大学计算机信息工程学院,江西南昌330022

出　　处：《江西师范大学学报（自然科学版）》2018年第4期379-383,共5页Journal of Jiangxi Normal University(Natural Science Edition)

基　　金：国家自然科学基金(61363013)资助项目

摘　　要：可信软件的不断发展进一步推动了形式化方法的深入研究.结合实际应用中的2个问题,采用基于递推关系的算法形式化方法,演示了算法的形式化推导过程,并运用Isabelle定理证明器结合Dijkstra最弱前置谓词方法,对得到的算法程序进行了自动化验证,避免了手工验证过程繁琐和易出错等问题.研究表明:基于递推关系的算法形式化方法不仅可以提高开发算法的效率,而且通过数学变换保证推导过程的正确性,从而有效保证了算法和程序的正确性.The continuous development of trusted software has further promoted the in-depth study of formal methods.Two formal problems of practical application are introduced,and the formal deduction process of the algorithm is demonstrated by the formal method based on recursive relation.The Isabelle theorem prover is combined with the weakest predicate method of Dijkstra to validate the algorithm automatically,which avoid the problem that manual verification process is tedious and error prone.The research shows that the formal method based on recursive relation can not only improve the efficiency of the algorithm,but also ensure the correctness of the derivation process by mathematical transformation.So this process effectively guarantees the correctness of the algorithm.

关 键 词：形式化方法 Isabelle定理证明器 自动化验证 形式化推导 

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