循環不變函數

Question

我想知道循環不變量。我開始知道在算法（主要是排序算法）中有一個循環不變量，循環不變表明算法的正確性。

這是如何工作的？有人能幫助我理解這一點嗎？

Answer 1

循環不變本身並不表示算法的正確性。對於循環的每次迭代而言，這是一個謂詞。 （你通常需要證明謂詞對於循環來說的確是不變的。）不變量可以用來證明循環的各種屬性（包括可能的正確性）。 Wikipedia article Loop invariant有一些示例說明了這可以如何工作。有關更多示例和解釋，請參閱this thread。