“软件危机”的出现，对于软件的可靠性和生产效率提出了更高的要求，形式化开发软件是一个很好的解决办法。而形式化开发软件就是要保证能对算法程序进行正确的推导和证明。而循环不变式是算法程序进行推导和证明的基石。任何一个循环程序都存在一个循环不变式，它在循环执行前和每次迭代后都能成立，当达到循环退出条件时，它产生了循环的最后结果。然而循环不变式无论是手工开发，还是自动构造一直都是一个巨大的挑战。本团队承担了国家自然科学基金重大国际合作项目：若干软件新技术及其在PAR平台中的实验研究。其中研究方向之一就是循环不变式的构造和自动探测。本文首先分析了国内外对循环不变式的定义及其开发方法的研究现状。然后介绍了本团队基于问题求解序列递推关系的循环不变式开发方法。接着介绍单元赋值语句型循环不变式的开发方法：按照PAR方法中的循环不变式开发策略，首先开发出抽象的单元赋值语句型循环程序的循环不变式，即抽象的单元赋值语句型循环不变式，并用Dijkstra最弱前置谓词方法进行了形式化的证明，然后对于具体的单元赋值语句型循环程序，将其对应的抽象的单元赋值语句型循环不变式进行参数实例化即可得到所需的单元赋值语句型循环不变式。最后在本研究团队已有循环不变式自动生成系统中实现了单元赋值语句型循环不变式的自动生成。本文的创新点有如下3个方面：1.对单元赋值语句和单元赋值语句型循环程序进行了抽象，使得该方法具有一定的普遍性和典型性。2.运用Dijkstra最弱前置谓词方法对开发出的抽象的单元赋值语句型循环不变式进行了形式化证明。3.在本研究团队已有的循环不变式自动生成系统上扩充实现了单元赋值语句型循环不变式的自动生成。