循环不变量以计算 n、low 和 high 的值

Question

所以，我应该使用循环上方提供的信息来计算 n、low 和 high 的值将是什么，而无需知道内部实际发生了什么循环。有人可以解释我如何使用循环不变量来解决这个例子。问题是找到这些值 n=81 和low =8 和'''high=9```。这些是问题的正确答案。

Answer 1

我们有三个公理：

• 允许low 和high 在循环内更改，但n 不允许。
• low + 1 <= high 和 low * low < n <= high * high 在循环的每次迭代中都必须为真。
• high - low 必须在循环的每次迭代中减少

我不确定你的教科书所说的导出输出的正确方法 - 参考它 - 但从我的角度来看，解决问题的方法是：

1. 将解与初始值进行比较
   • n 不会改变（这很好，@updates 暗示它不应该改变）
   • low 从 3 增加到 8
     • 注意 8^2 = 64
   • high 从 41 减少到 9
     • 注意 9^2 = 81
   • 在循环上方的注释中给出的公理保留在这里
     • (8 + 1)
     • 8^2
2. 既然公理说@decreases high - low，这一定是循环内变化的驱动力。 high 必须减少，或者low 必须增加。
   • 看到high 减少了，low 增加了。这一定是他们各自应该改变的方向。请注意，做这些事情中的任何一个都将满足@decreases 的需求，因为数学。
3. @maintains 公理定义了此更改的限制。 low 不能超过 high（并且 low * low 不能超过 n），并且 high * high 不能小于 n。
   • 即何时停止更改low 或high。如果更改会违反其中一项，请不要进行更改。

我们可以得出结论，这个循环的目的是设置 low 和 high 使得

• 它们正好相差 1
• n 介于low^2 和high^2 之间（包括high^2）

或者，换句话说，将low 和high 分别设置为n 所在的完美平方的两个根。

---

由此，我们可以编写如下代码：

while (low < high - 1) {  // will terminate when low == high - 1
    // check the @maintains for `low`. The first @maintains was just checked by the
    // loop, so we just have to check the next @maintains. If increasing `low`
    // would not make the @maintains false, then we can increase `low`.
    if ((low + 1) * (low + 1) < n) {  
        low++;    // this will always decrease the value of (high - low), per @decreases
    }
    // check the @maintains for `high`. Same as above, but since `low` might
    // have changed since the last time we checked, we need to double-check
    // that we can still decrease high without problems.
    if ((high - 1) * (high - 1) >= n && (high - 1) > low) {
        high--;   // this will always decrease the value of (high - low), per @decreases
    }
}