如何正确的理解循环不变式?

还是拿斐波那契数列举例子，我们通常这么写：

//c++11
#include <cstdio>
#include <functional>
int fib1(int n) {
	int a = 0, b = 1, tmp;
	for(int i = 0; i < n; ++i) {
		tmp = a;
		a = b;
		b = b + tmp;
	return a;
int main(){
	printf("%d\n", fib1(10));
	return 0;

可以注意到，在fib1中，我们必须小心处理a，b，tmp三者的赋值顺序，以确保下一个状态的准确。 除此以外，i也是迭代过程中需要处理的状态，这里只是通过for循环来做了。

那么如果这时候我要用《算法导论》上提到的分析“循环不变式”的方法，来分析一下我写的fib1正不正确，该怎么做呢？

我们来理清一下，在a，b，tmp，i，n这5个变量中，tmp仅仅是用来解决赋值时的顺序问题的，n是常量，真正跟迭代的状态有关的变量是a，b，i这三个。

所以我们得到循环不变式：a == fib(i) && b == fib(i + 1) ，只要我们能证明这个特质 在从当前状态到下一个状态的过程中能得以保持 （以及对初始状态成立），我们就相当于证明了式子在迭代的每个阶段都成立（有没有发现其实就是数学归纳法？），我们就能确信我们的代码没有错，即当i == n的时候，我们一定能得到a == fib(n)。

为了让这件事情做得更机械一点，我们把代码改写成下面的fib2这样，把迭代变量a，b，i都暴露出来，并且都通过next_*这些临时变量来计算下一个状态，这样我们就只需要考虑下一个状态和上一个状态的关系，而不用关心赋值的顺序了（可以注意到对next_*赋值的三条语句的顺序是不重要的，对后面三条语句也一样）。

int fib2(int n) {
	int a = 0, b = 1, i = 0, next_a, next_b, next_i; //(a, b, i) 构成一个状态
	while(true) {
		if(i >= n) {
			break;
		else {
			next_a = b; //根据当前状态计算下一个状态
			next_b = a + b;
			next_i = i + 1;
			a = next_a; //更新当前状态
			b = next_b;
			i = next_i;
	return a;

通过上面的改造，我们发现，在新的fib2中，迭代变量a，b，i已经被明确地暴露出来了，并且对下一个状态的计算过程很明确，不再是捣鼓一些不明所以的tmp变量了，而且对计算顺序也不再敏感。

不过，它显然没有fib1简洁好看。那么怎么做到内外兼修呢？ 可以把迭代变量作为一组参数定义一个函数专门用来迭代，然后这组参数表达的就是当前状态，在函数体内要做的主要事情，就是1. 判断是否到达终止状态， 2. 计算出下一个状态。 这样一来我们就得到了下面的fib3 。 可以看到，我们之前通过next_*变量做的事情，现在被传参过程中的参数拷贝替代了。

int fib3(int n) {
	std::function<int(int, int, int)> iter;
	iter = [n, &iter](int a, int b, int i) {
		if(i >= n) {
			return a;
		else {
			return iter(b, b + a, i + 1);