乐趣区

关于算法:循环不变量loop-invariant的理解

在计算机科学中,循环不变量(loop invariant),是一组在循环体内、每次迭代均放弃为真的某种性质,通常被用来证实程序或算法的正确性。

了解循环不变量这个概念对咱们了解算法过程,和解决算法问题有很大的帮忙。上面参考《算法导论》,对循环不变量的概念进行具体的解释。

咱们应用循环不变量帮忙咱们了解一个算法为什么是对的。对于一个给定的循环不变量,咱们必须遵循以下三个属性:

  • 初始化: 在循环的第一次迭代之前,循环不变量为真。
  • 放弃: 如果在循环的一次迭代之前循环不变量为真,那么在下一次迭代之前循环不变量同样为真。
  • 终止: 当循环完结时,不变量可能提供咱们有用的属性,用于帮忙咱们证实算法是正确的。

当保障前两个属性时,循环不变量在循环的任意迭代之前都满足。留神它与 数学归纳法 的相似性,当你想证实一个属性存在时,你须要证实一个基准和一个演绎步。相应的,咱们第一次迭代之前保障不变量成立对应于一个基准,咱们在每次迭代之间保障不变量成立对应于一个演绎步。

因为咱们用循环不变量证实算法正确性,所以第三个属性或者是最重要的。通常,咱们必须保障在循环完结时“循环不变量”和“循环终止条件”同时成立。 这与数学归纳法有所不同。数学归纳法常采纳有限的演绎步,而循环不变量的演绎往往随着循环的终止而完结。

接下来,咱们通过 插入排序 算法来更好的了解循环不变量。
先贴代码(Go 语言)

func insertionSort(nums []int) {j, n := 0, len(nums)
   for j < n {
      i := j - 1
      key := nums[j]
      for i >= 0 && nums[i] > key {nums[i+1] = nums[i]
         i--
      }
      nums[i+1] = key
      j++
   }
}

循环不变量: j之前(不蕴含nums[j])的元素曾经排好序(升序)。

  • 初始化: j0,示意目前排好序的子数组没有元素,不变式成立。
  • 放弃: 如果前一轮迭代 j 满足条件,则 [0,j) 范畴内子数组的元素均为升序。以后迭代中 nums[j+1] 与子数组的元素从大到小进行比照。如果找到第一个比 nums[j+1] 小的元素,则在其后插入一个值为 nums[j+1] 的元素。因而在此次迭代完结后,[0,j+1)范畴内子数组的元素均为升序,不变式成立。
  • 终止: j一直递增,当 j == n 时,所有数组的元素均被遍历解决,此时 [0,n) 为升序,不变式成立。

通过以上三个属性的证实,能够最终得出整个输出数组 nums 为升序的论断,满足算法的目标,同时也验证了算法的正确性。

退出移动版