迴圈不變數：s是乙個語句，已知迴圈
while c do
e當此迴圈滿足以下條件,即：在任何迴圈開始前，語句s和c都為真，而且在迴圈結束後，s仍為真，那麼s就是迴圈不變數
迴圈不變數定理：已知乙個迴圈和迴圈條件的guard condition g。命 i(n) 為迴圈不變式。如果下面四個條件為真，那麼此迴圈是正確的
1）basic property: the pre-condition implise i(0)
2）induction property: for all ints k = 0, if guard and i(k) are true before the iteration, then i(k+1) is true after.
3）eventual falsity of the guard: after a finite number of iterations, g becomes false;
4）correctness of postconditons: if n is the first place where g is false, and i(n) is true, then post-condition holds.
其中，guard condition g 是指在迴圈前對迴圈變數的檢查，例如：while( i < n) 中的 i <= n
以求陣列中最大值為例子，
max(a[1],...a[n])
m = a[1]
i = 1
while(i <= n) do
if a[i] > m then
m = a[i]
end if
i = i + 1
end while
return m
迴圈前的先驗條件為陣列的第乙個元素 m = a[1] 而且 i = 1。迴圈的後驗條件是m是陣列a中最大的元素。那麼現在的迴圈不變數就是i(i): m是陣列a中前 i 個元素的最大值。the guard condition condition g is i <=n.
通過在i上的推導來證明這個迴圈的正確性。首先，注意n是個固定的整數，而且 i 的初始值比n小，且每次迴圈n都增加，在某一點的時候 i <=n 為假。這在n-1次迴圈之後總會發生。
現在來證明迴圈不變數。首先，i(1)是真的，因為a[1] = m，所以在陣列中只有乙個元素，所以此時a[1]肯定是最大的。為了進行推導，我們假設m是a[1]......a[i]中的最大值，這個假設為i(i),我們要證明的是在一次迴圈之後，i(i+1)將會成立。考慮兩種情況，1)a[i+1]>m，在這種情況下，a[i+1]比先前a中的元素都大，通過傳遞性，m=a[i+1]也是a[1]......a[i+1]中最大的元素。
2)a[i+1] 不變數理論 9224903?fr aladdin invariant theory 一組幾何元素由 k個引數組成的向量 p1表示 若 t為某一變換，t g g為某一變換群，這組幾何元素經 t變換後，其引數組成的向量由 p1變為 p2 p1,p2 均為 k維向量 如果 i p1 i tp1 i p2 ... 先看引用自由cay horstmann寫的 computing concepts with c essentials 3rd 一書的，用以計算a n的例子 double power double a,int n else return r 粗看一下，用此方法計算a n時比原始方法進行迴圈次數要少很多... 在演算法中，有乙個重要的概念就是迴圈不變式，迴圈不變式主要用來幫助我們理解演算法的正確性。關於迴圈不變式，我們必須證明三條性質 1.初始化 迴圈的第一次迭代之前，它為真。2.保持 如果迴圈的某次迭代之前它為真，那麼下次迭代之前它仍為真。3.終止 在迴圈終止時，不變式為我們提供了乙個有用的性質，該性質...invariant theory 不變數理論
迴圈不變式
迴圈不變式