循环不变式问题

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

举例：

布口袋中有黑，白两色小球，现将手放入袋中每次摸出两个，如果两球同色就都不放回袋中，如果两球异色就将白球放回，由于每次至少减少一个，所以袋中的球必然越来越少。

现问:如果袋中最后剩下一个球，此球的颜色与开始时袋中黑、白球的个数有什么关系?

按照一般的思路，此题非常复杂，难以解决。多次重复摸球及放回的动作构成了一个循环过程。

如果我们有意识地寻找循环过程中不变的性质，就会发现,在循环过程中,白球个数的奇偶性保持不变,因为,每次取出的白球的个数或是零或是2.

因此,如果开始时白球的个数为奇数,那么剩下的一球为白球。如果开始时白球的个数为偶数，那么剩下的一球为黑球。

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