循环不变式是在循环体的每次执行前后均为真的谓词。循环不变式体现了循环程序中循环变量的变化规律。

在早期程序理论里最重要的不变式是循环不变式。在有关程序正确性证明的早期工作中，Floyd引入了循环不变式的思想。其后，Dijkstra和 Gries做了更深入的研究，从算法逻辑上给出严格的定义，将循环不变式定义为：在循环体的每次执行前后均为真的谓词。循环不变式体现了循环程序中循环变量的变化规律。

布口袋中有黑，白两色小球，现将手放入袋中每次摸出两个，如果两球同色就都不放回袋中，如果两球异色就将白球放回，由于每次至少减少一个，所以袋中的球必然越来越少。现问:如果袋中最后剩下一个球，此球的颜色与开始时袋中黑、白球的个数有什么关系?按照一般的思路，此题非常复杂，难以解决。多次重复摸球及放回的动作构成了一个循环过程。如果我们有意识地寻找循环过程中不变的性质，就会发现,在循环过程中,白球个数的奇偶性保持不变,因为,每次取出的白球的个数或是零或是2.因此,如果开始时白球的个数为奇数,那么剩下的一球为白球。如果开始时白球的个数为偶数，那么剩下的一球为黑球。

这种不依较前面所执行的重复次数的性质称之为循环不变式。

循环是重复多次实现的，要证明循环的结果是正确的，就要仿照数学归纳法的方法，即如这次满足某一性质那么下次也满足，则循环完毕性质也成立，显然,循环不变式是很重要的。

如图1，变量在循环中被引用时，若其值在环内不变，则称它为循环的相对常数，井满足下列条件。

现在研究在程序循环中一个重要的不变性( Invariance)。该不变性在正确性证明和逻辑注解中给人们带来极其深奥的洞察力。一个循环不变式( Loop invariant)具有一个逻辑条件的单一断定，当该断定被计值时，它永远为true。