循环不变量是在循环执行前后为真的断言。

在线性搜索(根据书中给出的练习)中，我们需要在给定的数组中找到值V。

它很简单，从0 <= k < length开始扫描数组并比较每个元素。如果找到V，或者扫描到数组的长度，就终止循环。

根据我对上述问题的理解-

循环不变量(初始化): 在k - 1迭代中找不到V。第一次迭代，这是-1因此我们可以说V不在-1位置

保养: 在下一次迭代中，V不在k-1中成立

Terminatation: 如果V位于k个位置，或者k达到数组的长度，则终止循环。

循环不变量属性是一个条件，适用于循环执行的每一步。For循环，while循环，等等)

这对于循环不变证明是必不可少的，如果在执行的每一步都保持循环不变属性，则可以证明算法正确执行。

对于一个正确的算法，循环不变量必须保持在:

初始化(开始)

维护(之后的每一步)

终止(当它完成时)

这被用来计算很多东西，但最好的例子是加权图遍历的贪婪算法。对于贪心算法产生最优解(穿过图的路径)，它必须达到连接所有节点在最小权值路径可能。

因此，循环不变的性质是所选择的路径具有最小的权值。在开始时，我们没有添加任何边，所以这个属性为真(在这种情况下，它不是假的)。在每一步中，我们都遵循最小权值边(贪婪步)，所以我们再次采用最小权值路径。最后，我们找到了最小加权路径，所以我们的性质也是成立的。

如果一个算法不这样做，我们可以证明它不是最优的。

在这种情况下，不变量意味着在每次循环迭代的某一点上必须为真条件。

在契约编程中，不变量是在调用任何公共方法之前和之后必须为真(通过契约)的条件。

简单地说，它是一个循环条件，在每次循环迭代中都为真:

for(int i=0; i<10; i++)
{ }

在这里，我们可以说i的状态是i<10并且i>=0

简单地说，循环不变量是对循环的每次迭代都成立的某个谓词(条件)。例如，让我们看一个简单的For循环，它是这样的:

int j = 9;
for(int i=0; i<10; i++)  
  j--;

在这个例子中，i + j == 9(对于每个迭代)是正确的。一个较弱的不变式也是成立的 I >= 0 && I <= 10。