当今世界是一个软件定义一切的时代,尤其在安全攸关领域,需要保证计算机程序的可靠运行。这种可靠性可以通过向程序传递所有可能的测试用例的方法来实现,但该方法难以保证一些输入范围无限的复杂程序的正确性。形式验证的目的是构建程序正确性的数学说明,但所需验证工作是繁琐的,而且容易出错,使用自动验证工具使证明过程自动化是目前形式验证的一种趋势。Dafny是微软研究院创建的一种内置规约结构的编程语言和静态程序证明器,其目的是验证程序的功能正确性并可将程序验证过程完全自动化。这大大减少了繁琐的程序验证过程,极大提高了软件的可靠性。必须认识到,现阶段Dafny程序的生成没有特定的方法和工具,很多问题的Dafny程序都是基于开发者的经验,而且Dafny程序中循环不变式都是从天而降的,基于开发者对算法设计的熟练程度。本文结合算法程序设计方法PAR方法和程序证明器Dafny提出了一个模型驱动的Dafny程序生成与验证方法,通过该方法对一些经典问题进行了算法形式化开发与自动验证,大幅提高了所开发算法程序的可靠性。本文的主要工作包括:一、对Dafny自动验证机理进行了深入剖析并给出示例说明。二、探索出一种模型驱动的Dafny程序形式化生成与自动验证方法。其步骤如下:首先,在程序开发的前期采用规约变换技术从问题Radl规约出发得到问题的Radl算法;然后,利用PAR方法中循环不变式开发新策略得到循环不变式;最后,以Radl算法和循环不变式为依据,根据模型等价转换规则得出问题的Dafny程序,并由Dafny证明器自动验证该程序功能正确。三、通过该方法解决了一些典型问题的算法程序开发与验证,如立方和、最小和、查找、排序等问题,证实了该方法能够有效地提高Dafny程序的开发效率、正确性和可靠性。提炼出二重嵌套循环Dafny程序生成模型等价变换规则,据此生成了若干冒泡排序算法程序,并生成一种新的局部冒泡排序算法。