- 论坛徽章:
- 5
|
本帖最后由 starwing83 于 2012-08-08 10:16 编辑
回复 74# OwnWaterloo
好吧，我以为对着聪明人，有些话不必说全，既然你坚持，我就说全好了= =
所谓循环不变式，是的，就是个interface，它用于两个方面：1. 说明满足这些条件的算法是正确的（必要性）2. 说明按照这些条件可以很容易设计算法（充分性）。
下面详细解释，为了简单，我们以upper-bound为例，lower-bound反之亦然。
upper-bound的定义是：在[left, right)中找到一个合适的值v，并且这个v是所有v的最右边的一个。
为了找到满足这个定义的算法，我们可以给出一系列的限制条件。
1. v一定在[left, right)范围内（由定义可得）。
2. 二分查找一定会结束（由“算法”这个概念的定义可得）。
2.1. 推论：查找中，每次递归必须收缩范围（因为查找每次递归行为相同，可以一次不收缩，就意味着会永远不搜索，从而导致条件2被违背——反证法）。
2.2. 推论：查找必须要有一个终结条件（由条件2直接得出）。
3. 我们规定，在最后剩下一个元素的时候（即left == right时），退出查找（由2.2和定义可得）。
通过推论，我们得到了上面的三条invariant。现在我们要保证这三条invariant在每次循环中必须遵守（此为循环不变式）。
接下来分析upper-bound本身的性质：根据二分查找原理和upper-bound定义，当遇到相同的元素时，我们应该选择右半（包含该元素）的部分。
证明：因为遇到了相同元素，我们可知，相同元素一定出现在唯一一个相同元素区间（因为二叉树本身是有序的）。
那么，我们所求的upper-bound，一定在这个元素的右边，或者就是这个元素（由upper-bound定义可得）。
结论：我们应该选择该元素的右半部分，并包含该元素。
你看，几乎所有推论都是由定义得的。如果这还不叫简单，我不知道还有什么叫简单。现在我们用得到的四条规律实现一个算法（算法实现），当实现以后，我们说明实现的算法是满足这四条规律的（！！），那么这四条规律的证明过程（如你所见，非常简单）就是对算法正确性的证明。
首先给出最简单的，有序数组查找方法（原因是，这种方式很容易在二分的时候，包含相等元素自身，方便设计，容易看出那四条规律）：
- int array_upper_bound(int *begin, int *end, int v) {
- while (begin + 1 < end) { /* 当begin + 1 == end时，区间只有一个元素，满足算法结束条件 */
- int *middile = &begin[(end - begin)>>1];
- if (v >= *middle) /* 由第四条规律直接可得。 */
- begin = middle; /* 注意包含了middle本身，选择后半部分 */
- else
- end = middle + 1; /* 注意包含middle本身，选择前半部分 */
- }
- return *begin; /* 退出循环意味着begin,end区间只有一个元素，此即所求元素 */
- }
我们很详细的说明了四条指导方针是如何设计算法的。几乎算法的每一条都是由四条方针直接可得。有一条无法表现在算法中，即范围一定缩小。这一条应该标记在int *middle那行，不过位置太小，我写不下，就写在这里好了。
根据结束条件，只有end紧跟begin的时候才会退出，这时会剩余一个元素，在这种情况下，范围不缩小是允许的（直接触发结束条件）。那么，算法范围不缩小也不退出就只会有一个情况，即新计算的end没有紧跟begin，而范围也没有缩小。而这不可能：假设middle等于begin（即if真分支不缩小，begin不变），那end一定等于begin或等于begin+1（由middle计算逆推可得），这时直接触发结束条件；假设middle等于end-1（即if假分支不缩小，end不变），同理可得begin一定等于middle，同样会直接退出。因此算法范围一定缩小，或者直接退出。
现在根据这个数组区间算法，我们直接给出对于二叉树的搜索算法：
- int upper_bound(tree *t, int v) {
- while (1) { /* 不同于数组，我们无法在循环条件中保证一定有一个t，除非设置一个parent，见下 */
- if (v >= t->v) { /* upper-bound之附加条件。见数组版upper-bound */
- if (t->right != NULL) /* 保证至少范围内有一个元素 */
- t = t->right;
- else
- return t; /* 否则，返回t本身 */
- }
- else {
- if (t->left != NULL)
- t = t->left;
- else
- return t;
- }
- }
- }
注意到，如果t为NULL时，t的父亲一定是满足条件的（t一定有父亲，甚至t是NULL也是这样，而t为NULL代表空集，如果t有父亲，一定是那个满足条件的元素），伴随这个认知，我们每次记录t的父亲，可以避免复杂的判断。
- int upper_bound(tree *t, int v) {
- tree *answer = t;
- while (t) {
- answer = t;
- if (v >= t->v)
- t = t->right
- else
- t = t->left;
- }
- return answer;
- }
这样，我们就根据四规律，设计了三个版本的upper-bound算法。我们很轻松地能证明这些算法是正确的。证明正确的过程，就是解释的过程。因此只需要按照上面的逻辑正推一遍，给出设计时的思路，这本身就是对算法的解释。以上，很多证明都是由定义可得，如果忽略，就是我最开始发言的部分。这就是我说简单的含义。哎，非逼着我打这么多字。
顺便说一下，以上所有代码纯粹手写，仅做说明用途，没有经过任何测试，请测试后再使用。
最后提一下，四个规律很容易可以写成assert嵌入到代码里面，这可以更强地保证代码的正确性，这也是循环不变式（上面所有推导过程的核心思路）的实际应用之一——这总用不着我再举例了吧= = |
|
免费注册
楼主: OwnWaterloo
发表于 2012-08-07 21:04
发表于 2012-08-08 06:03