高可靠性软件是当今软件开发的热点问题.确保算法程序逻辑结构正确最理想途径是算法程序的形式化推导和证明。循环不变式在软件形式化方法中占有十分重要的地位,它是理解、证明和推导算法程序的基础和关键。使用形式化方法来证明或推导算法程序无法回避的一个问题就是给出正确的循环不变式。但是循环不变式的开发一直是算法程序设计领域中最具挑战性、最富有创造性、也是最困难的问题之一。自形式化方法出现以来,众多专家致力于循环不变式的开发,提出了许多循环不变式开发技术,如谓词抽象技术、动态探测技术等。这些技术能探测出较简单问题的循环不变式,但是却无法处理复杂问题。从本质上来说,循环不变式刻画了循环变量的变化规律和循环程序的特征,因此一个循环程序的循环不变式并非轻易就能得到,尤其是对复杂算法的来说,必须在对循环程序的算法本质有充分理解的基础上才能找到。而现有的循环不变式定义不能反映出循环不变式的本质,基于现有循环不变式定义的技术缺乏理论上的指导,在探测循环不变式的过程中具有试探性和盲目性,又因为本身技术上的限制,因而无法得出复杂问题的循环不变式。薛锦云教授及其学术团队分析了大量算法程序的本质特征及其与循环不变式关系[15]~[20],发现现有循环不变式定义的不足,提出了关于循环不变式的新定义和基于新定义之上的循环不变式开发技术,并在此基础上形成了一种实用的算法程序形式化开发方法——PAR方法及其开发环境,在复杂算法程序及软件形式化开发中发挥了重要作用。本文是PAR方法及其开发环境研究的继续,也是薛锦云主持承担的国家自然科学基金项目“基于PAR方法的算法设计形式化和自动化研究”和973前期预研项目“形式化方法制导的软件自动化研究”的重要研究内容。本文主要的工作是对现有循环不变式定义和现有开发技术进行深入研究,并与PAR方法中的循环不变式开发技术进行比较,指出了现有开发技术的不足之处;同时基于薛锦云教授提出的循环不变式新定义和新开发技术,探讨、研究并初步实现了循环不变式自动开发系统。具体研究成果如下:1.深入研究了循环不变式定义;2.对循环不变式标准开发策略和现有较新的几种循环不变式开发技术进行了分析和比较,剖析了其难以适用的原因;3.详细分析了PAR方法循环不变式新定义和新开发策略,以其作为基础提出了循环不变式开发系统的新模型,并初步实现循环不变式自动开发系统;4.使用Dijkstra最弱前置谓词法对开发出的循环不变式进行正确性证明。