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

Dafny是一种内置规范结构的编程语言和静态程序证明器,它能验证程序的功能正确性以及将证明过程自动化,这既提高了软件开发的效率,又极大增强了软件开发的可靠性.该文探索了一种模型驱动的Dafny程序形式化生成的方法.首先,从问题的Radl规约出发,根据规约变换技术得到其Radl算法; 然后,根据PAR方法中循环不变式开发新策略得到问题的循环不变式; 最后,在Radl算法和循环不变式基础上利用模型等价转换规则生成Dafny程序,并由Dafny证明器自动验证其功能正确性.用该方法解决了2个典型问题的算法程序开发与验证,证实了该方法能够有效地提高Dafny程序的生成效率和可靠性.

The Model-Driven Dafny Program Generation and Automatic Verification

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.