algorithm - 算法中不变的东西

Question

k :=0
for i ←1 to n
     c←a[i]
           k←k+1

这是知道元素数量的算法

Answer 1

从技术上讲，是的，k <= i是一个不变量，但不是一个非常有用的变量。我们使用不变量的原因是我们可以使用它们来证明循环后的状态。使用您的不变量，您可以证明k <= n在循环之后成立。尽管非常正确，但这并不能真正帮助您尝试证明循环的真正作用。

那么什么样的不变量会有用呢？我们想证明k等于 和 中的元素a数b。由于我们正在遍历 in 中的元素a，因此一个不错的选择是：k等于在 中的元素a[i]数量b。

---

我们现在需要证明这个不变量成立。我会稍微粗略地说一下，所以这仍然取决于你来正式化。

最初，我们需要证明k = 0之前的元素数量a[1]也在b. 没有这样的元素，所以k = 0是正确的。

现在，鉴于是中的元素数，我们需要证明不变量适用于。有两种选择：要么在，要么不在。kia[i]bi+1a[i+1]b

• 如果a[i+1]在 中b，则在 中的元素数比在 中的元素a[i + 1]数大一。使用我们的不变量，我们因此需要证明.ba[i]bki+1 = ki + 1
• 如果a[i+1]不在 中b，则在 中的元素数等于在 中的a[i + 1]元素数。使用我们的不变量，我们因此需要证明.ba[i]bki+1 = ki

我会留给你来证明这些。