循环不变式 [#]_
########################################

熟练掌握数学归纳法的思路对于程序员来说是相当重要的。例如，要在程序中编写循环处理(loop) 时数学归纳法是非常有用的。

在编写循环时，找到让每次循环都成立的逻辑表达式很重要。这种逻辑表达式称为 ``循环不变式（loop invariant）``。循环不变式相当于用数学归纳法证明的“断言”。

循环不变式用于证明程序的正确性。在编写循环时，思考一下“这个循环的循环不变式是什么”就能减少错误。

光这么说也许不容易理解。我们还是以一个非常简单的例子来讲解循环不变式吧。

代码清单4-2 是用C 语言写的sum 函数，功能是求出数组元素之和。参数array[] 是要求和的对象数组，size 是这个数组的元素数。调用sum 函数，会获得array[0] 至array[size-1] 的size 个元素之和。

**代码清单4-2 sum函数，求出数组的元素之和**

.. code-block:: c

    int sum(int array[], int size){
        int k = 0;
        int s = 0;
        while(k < size){
            s = s + array[k];
            k = k + 1;
        }
        return s;
    }


在sum 函数中使用了简单的 while 循环语句。我们从数学归纳法的角度来看这个循环，得出下述断言M(n)。这个断言就是循环不变式。

- 断言M ( n ) ：数组 array 的前 n 个元素之和，等于变量 s 的值。

我们在程序中成立的断言上标注注释，形成清单4-3 所示代码。

**代码清单4-3 在4-2的代码中成立的断言上标注注释**

.. code-block:: c

    int sum(int array[], int size){
        int k = 0;
        int s = 0;
        // M(0)
        while(k < size){
            // M(k)
            s = s + array[k];
            // M(k+1)
            k = k + 1;
            // M(k)
        }
        // M(size)
        return s;
    }

在代码清单4-3 的第4 行，s 初始化为0。由此，第5 行的M(0) 成立。M(0) 即为“数组array 的前0 个元素之和等于变量s 的值”。这相当于数学归纳法的步骤1。

**图4-8 数学归纳法的步骤1（M(0)成立）**

.. image:: assets/循环不变式M0.png

第7 行中，M(k) 成立。然后进行第8 行的处理， 将数组array[k] 的值加入s, 因此M(k+1) 成立。这相当于数学归纳法的步骤2。

**图4-9 数学归纳法的步骤2（M(k) M(k+1)成立）**

.. image:: assets/循环不变式Mk.png

请一定要理解第8 行，
``s=s+array[k];``

意为“在M(k) 成立的前提下，M(k+1) 成立”。

第10 行中k 递增1，所以第11 行的M(k) 成立。这里是为了下一步处理而设定变量k的值。

最后，第13 行的M(size) 成立。因为while 语句中的k 递增了1，而这时一直满足M(k), 走到第13 行时k 和size 的值相等。M(size) 成立说明sum 函数是没有问题的。因此，第14 行return 返回结果。

**图4-10 M (size )成立**

.. image:: assets/循环不变式Msize.png

综上所述，这个循环在k 从0 增加到size 的过程中一直保持循环不变式M(k) 成立。编写循环时，有两个注意点。一个是“达到目的”，还有一个是“适时结束循环”。循环不变式M(k) 就是为了确保“ 达到目的”。而k 从0 到size 递增确保了“适时结束循环”。

代码清单4-4 中，写明了M(k) 成立的同时k 递增的情形。（∧表示“并且”）

**代码清单4-4 M (k )成立的同时k递增**

.. code-block:: c

    int sum(int array[], int size){
        int k = 0;
        int s = 0;
        // M(0) ∧ k ==0
        while(k < size){
            // M(k) ∧ k < size
            s = s + array[k];
            // M(k+1) ∧ k < size
            k = k + 1;
            // M(k) ∧ k ≤ size
        }
        // M(size) ∧ k == size
        return s;
        }

看了以上循环不变式M(k) 在每次循环时都成立的情形之后，您是否都掌握了呢？

.. note::

   在 《算法导论（第三版）》中，对循环不变式提出了以下三条性质：

   #. 循环的第一次迭代之前，它为真
   #. 若循环的某次迭代之前它为真，那么下次迭代之前它任然为真
   #. 在循环终止时，不变式为我们提供了一个有用的性质，该性质有助于证明算法是正确的

.. [#] \ `程序员的数学：循环不变式 <https://www.ituring.com.cn/book/miniarticle/20305>`_