状态机：如何构建稳定的婚姻( 二 ) _状态

首先我们建立一个状态机，它的状态表示为(b, l)，其中b代表big jug，l代表 jug，所以0(0, l)将小水桶里的水倒入大水桶中。(1) 如果b + l(b+l, 0). (2)否则，(b, l) -> (9, l - (9-b))将大水桶里的水倒入小水桶中。(1) 如果b + l(0, b+l). (2)否则，(b, l) -> (b - (3-l), 3)
注意到这个状态机和我们之前那个计数器状态机不同，它每一次的状态转换的选择不止一个，像这样的状态机就称为”非确定性的“（），计数器状态机则称为”确定性的“（）。
设P((b, l))为“b，l均为3的整数倍”，下面我们证明它是对状态机所有状态都成立的不变量：
首先证明如果P(q)成立，q -> r，那么P(r)也成立：
“装满操作”，得到(9, l)或者(b, 3)，由于9, 3, l, b都是3的整数倍，命题成立“清空操作”，得到(0, l)或者(b, 0)，由于0, l, b都是3的整数倍，命题成立将小水桶里的水倒入大水桶中。(1) 如果b + l(b+l, 0) 由于b+l, 0都是3的整数倍，命题成立 (2)否则，(b, l) -> (9, l - (9-b)) 由于9, l - (9-b)都是3的整数倍，命题成立。将大水桶里的水倒入小水桶中。(1) 如果b + l(0, b+l) 由于0, b+l都是3的整数倍，命题成立 (2)否则，(b, l) -> (b - (3-l), 3) 由于b - (3-l), 3都是3的整数倍，命题成立。
综上，P是该状态机的一个不变量。又因P(0, 0)也成立，而(0, 0)是该状态机的起始状态，由不变性原理，P对于该状态机所有可到达的状态都成立。因为4不是3的整数，所以我们不可能得到一个装有4加仑水的桶。证毕。
3. 状态机的部分正确性和可终结性
我们可以从两个方面判定程序（状态机）是否可用：部分正确性（）和可终结性（）。部分正确性并不是指程序结果是部分正确的，而是因为程序在计算“部分关系”（）的时候可能不会终止，所以这个正确性是“部分的”，或者这么说，如果程序最终停止，得出的结论一定是正确的。可终结性则是指程序理论上是会最终停止的。
通常情况下，部分正确性可以用不变性原理证明，而可终结性可以用良序原理证明。下面我们用一个常见的快速求幂算法来解释这两个性质，对于求a^b的值，算法如下：

文章插图
首先建立起这个状态机：其的状态为(x, y, z)，所以其起始状态为(a, 1, b)，状态转换为：(1) 如果z != 0 && z为偶数，(x, y, z) -> (x^2, y, z/2) (2) 如果z != 0 && z为奇数，(x, y, z) -> (x^2, xy, z/2) 。
接着证明该状态机的不变量P((x, y, z))：z为自然数且y*(x^z) = a^b 。设P((x, y, z))成立；则在第一种转换下，z为自然数，y*((x^2)^(z/2)) = a^b 。在第二种转换下，z为自然数，y*x*((x^2)^(z/2))（z除2后舍去了余数1）= a^b 。得证，又因为起始状态P((a, 1, b))依然成立，由不变性原理我们便证明了该程序/状态机的部分正确性。
在证明该程序的可终结性之前，先介绍一下“派生变量”（）这个概念：
我们在证明程序是可终止的时候通常会使用程序中的一个非负数值，如果它在程序每一步的运行中都是严格递减的，由良序原理，它不可能无限递减，最终会达到那个最小值，也就是程序终止。如果更普遍的理解，我们将一套设计好的操作f作用于状态p，称之为f(p)，如果f(p)是严格递减的，即(p -> q)f(q) < f(p)，且对于所有可到达状态，f(p)构成一个良序集合，那么就可以得到该程序/状态机是可终止的（f类似于物理学里面的势能函数）。
另外，这种方法也常常用于算法的分析，即对于一个算法生成一个派生变量，在算法运行的过程中观察这个变量的变化。
对于上面例子中的算法，我们可以令派生变量f((x, y, z)) = z，我们已经证明了z是自然数（即良序集合），且当z不为0时z/2