随着计算机应用的日益普及,计算机软件的正确性和可靠性在各个领域中都受到高度重视,尤其在一些关键领域如市场经济、交通安全、航空航天等领域中更是至关重要。算法是软件的核心,它在软件开发中占有不容忽视的地位。形式化方法是保证算法正确性和可靠性的有效途径之一。而循环不变式在算法形式化方法中具有至关重要的作用,它是理解、开发和证明一个算法程序的关键。循环不变式的开发一直是形式化领域中最具挑战性、最富创造性的问题之一,寻找循环不变式开发策略一直存在较多难点。组合数学是计算机出现以后迅速发展起来的一个数学分支,它在理论方面的推进也促进了计算机科学的迅速发展,在计算机科学领域中许多问题的算法求解以组合数学为基础,因而组合数学问题的算法研究已成为计算机科学中重要的研究领域。在组合数学问题中,数列问题和排列组合问题是最经典和最具有代表性的两类问题,因此本文重点研究了数列问题和排列问题算法程序的循环不变式开发技术。本文首先进一步探究了循环不变式在算法形式化方法中的作用,并对现有的循环不变式开发技术和策略进行了分析和比较。其次,通过对组合数学问题中卡特兰数列和斐波那契数列问题进行深入研究,根据这两类数列问题的数学性质和求解特征,提出了一种数列问题的循环不变式开发策略;同时,根据对组合数学中排列问题求解过程的深入分析,基于对所求解问题的分解,通过刻画已处理完成部分和未处理部分的性质以及它们之间所存在的关系,提炼出问题求解过程中所存在的不变性质,提出了排列问题循环不变式的两个具体开发策略,从而为两类组合数学问题循环不变式的开发提供了有效途径。论文将所提出的循环不变式开发策略应用于若干数列问题和排列问题循环不变式的开发,并基于所开发的循环不变式完成了这些问题算法程序的形式化推导过程,从而在获得这些问题求解算法程序的同时,也有效保证了这些算法程序的正确性。