模型驱动的Dafny程序形式化生成与自动验证  

The Model-Driven Dafny Program Generation and Automatic Verification

作　　者：王昌晶[1] 贺江飞 罗海梅[2,3] 左正康[1] 许帆 WANG Changjing;HE Jiangfei;LUO Haimei;ZUO Zhengkang;XU Fan(College of Computer Information Engineering,Jiangxi Normal University,Nanchang Jiangxi 330022,China;College of Physics and Communication Electronics,Jiangxi Normal University,Nanchang Jiangxi 330022,China;Key Laboratory of Photoelectronics and Telecommunication of Jiangxi Province,Jiangxi Normal University,Nanchang Jiangxi 330022,China)

机构地区：[1]江西师范大学计算机信息工程学院,江西南昌330022 [2]江西师范大学物理与通信电子学院,江西南昌330022 [3]江西师范大学江西省光电子与通信重点实验室,江西南昌330022

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

基　　金：国家自然科学基金(61762049,11804133,61862033);江西省科技厅课题(2020BABL202025,2020BABL202026,2018BAB206034)资助项目.

摘　　要：Dafny是一种内置规范结构的编程语言和静态程序证明器,它能验证程序的功能正确性以及将证明过程自动化,这既提高了软件开发的效率,又极大增强了软件开发的可靠性.该文探索了一种模型驱动的Dafny程序形式化生成的方法.首先,从问题的Radl规约出发,根据规约变换技术得到其Radl算法;然后,根据PAR方法中循环不变式开发新策略得到问题的循环不变式;最后,在Radl算法和循环不变式基础上利用模型等价转换规则生成Dafny程序,并由Dafny证明器自动验证其功能正确性.用该方法解决了2个典型问题的算法程序开发与验证,证实了该方法能够有效地提高Dafny程序的生成效率和可靠性.Dafny is a programming language with built-in specification structure and a static program prover.It can verify the program′s functional correctness and automate the certification process.This not only improves the efficiency of software development,but also greatly enhances the reliability of software development.A model-driven method for the formal generation of Dafny programs is explored in the paper.Firstly,the Radl algorithm is derived from the Radl specification of the problem according to the protocol transformation technology.Then,a new strategy is developed based on the loop invariant of the PAR method to obtain the loop invariance of the problem.Finally,based on Radl algorithm and loop invariant,Dafny program is generated using model equivalent transformation rules,and its functional correctness is automatically verified by Dafny prover.The method proposed in this paper solves two typical problems of algorithm program development and verification,and it is proved that this method can effectively improve the generation efficiency and reliability of Dafny programs.

关 键 词：模型驱动 Dafny程序 循环不变式 形式化生成 自动验证 

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