三次排序程序的程序正确性

Question

我想要一些帮助来证明我的python三次排序程序的循环不变量。

到目前为止，我已经算出了循环不变量，它有两部分

1. 0<=i+1<=len(L(
2. 对L[0:i+1]进行排序

def cubicSort(L):
i = 0
while i + 1 < len(L):
if L[i] > L[i + 1]:
L[i], L[i + 1] = L[i + 1], L[i] # That is, swap L[i] and L[i + 1].
i = 0
else:
i = i + 1

前提条件是L是一个整数列表帖子：是列表被排列和排序

我不知道如何接近验证

Answer 1

正确性的证明有两个要素：必须证明当算法终止时，结果是正确的；你必须证明算法确实终止了。

---

你的两个循环不变量都是对的，但你需要证明它们是不变量。要显示这一点，必须在循环的第一次迭代之前证明它们是真的，如果在某次迭代之前它们是真，那么在迭代之后它们将是真的。

完成后，很简单，当循环终止时，i + 1 == len(L)，因此L[0:i+1]等于L，因此，当循环结束时，对L进行排序。

---

通常，通过找到循环变量来表明算法终止更简单——循环变量是一个整数，在循环的每次迭代中都会变小，当数量达到0时，它会导致循环终止。但对于该算法，没有明显的变化，因为循环计数器i在循环中重置为0，这意味着该变量不会简单地单调地变大或变小。

这个证明的关键是考虑列表中反转的数量，其中"反转"意味着一对无序的列表元素。在每次迭代中，i变大，或者i重置为0，但反转次数减少1。如果i没有达到while环界，或者反转数没有达到0，i不可能继续变大，反转数也不可能一直变小。一旦列表中没有反转，L[i] > L[i + 1]总是为假，因此i将继续增加到界，然后循环根据需要终止。