循环不变式（Loop Invariant）是程序语言和软件工程中的一个概念，主要用于循环结构（如for循环、while循环等）的证明中。它是一个在循环的每次迭代开始之前和结束之后都为真的性质或条件。
具体来说，循环不变式通常满足以下三个条件：
1. 初始条件：在循环开始之前（即循环的第一次迭代之前），循环不变式必须为真。
2. 保持条件：在循环的每次迭代中，如果循环不变式在迭代开始之前为真，那么在迭代结束之后它仍然为真。
3. 终止条件：当循环结束时，循环不变式必须为真，这通常意味着循环的终止条件得到了满足。
循环不变式在程序验证和软件工程中非常重要，因为它可以帮助证明程序的正确性。通过证明循环不变式，可以间接证明循环体内的代码在每次迭代后都满足某个特定的性质，从而帮助确保整个循环的正确性。
例如，考虑一个简单的求和循环：
```c
int sum = 0;
for (int i = 0; i < n; i++) {
sum += array[i];
