摘要
可信软件的不断发展进一步推动了形式化方法的深入研究.结合实际应用中的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.
作者
齐蕾蕾
杨庆红
游颖
QI Leilei;YANG Qinghong;YOU Ying(College of Computer Information Engineering,Jiangxi Normal University,Nanchang Jiangxi 330022,China)
出处
《江西师范大学学报（自然科学版）》
CAS
北大核心
2018年第4期379-383,共5页
Journal of Jiangxi Normal University(Natural Science Edition)
基金
国家自然科学基金(61363013)资助项目
