-
循環不變量
鎖定
循環不變量(loop invariant)是一個
不變量,被用來證明
循環的特點,更多地,
算法使用循環 (usually
正確性)。非正式的説,一個循環不變量是指在循環開始和循環中每一次迭代時永遠為真的量,這意味着在循環中和循環結束時循環不變量和循環終止條件必須同時成立。
- 中文名
-
循環不變量
- 外文名
-
loop invariant
- 性 質
-
不變量
- 領 域
-
計算機
循環不變量理化性質
由於循環和遞歸的程序相似的原因,證明帶有不變量的循環的部分正確性和證明通過歸納的遞歸程序的正確性極其相似。事實上,循環不變量通常是一個遞歸程序可以等價為一個給定循環的遞歸的屬性。
[1]
循環不變量霍爾邏輯
在弗洛伊德-霍爾邏輯,While循環的
部分正確性被下列的規則所確定:
意思是:
一個 while 循環不可以使得
為假 - 如果在給定條件
下循環體 body 不會使不變量
從真變成假,則
將在循環之後如在循環之前一樣為真。
只要
為真時
必會循環。若其於循環之後中止,則當為假。
[1]
循環不變量循環不變代碼外提
循環不變代碼外提(英語:loop-invariant code motion,縮寫LICM)在計算機編程中是指將循環不變的語句或表達式移到循環體之外,而不改變程序的語義。循環不變代碼外提在英文中又被稱為hoisting或scalar promotion,是
編譯器中常見的
優化方法。
[1]
循環不變量循環不變量
在計算機科學中,
循環不變性(loop invariant,或“循環不變量”),是一組在循環體內、每次迭代均保持為真的性質,通常被用來證明
程式或
偽碼的正確性(有時但較少情況下用以證明
算法的正確性)。簡單説來,“循環不變性”是指在循環開始和循環中,每一次迭代時為真的性質。這意味着,一個正確的循環體,在循環結束時“循環不變性”和“循環終止條件”必須同時成立。
由於
循環和遞歸的相通,證明帶有不變性的循環的部分正確性和證明通過歸納的遞歸程序的正確性極其相似。
[1]
循環不變量遞歸
遞歸(英語:Recursion),又譯為
遞迴,在
數學與計算機科學中,是指在
函數的定義中使用函數自身的方法。遞歸一詞還較常用於描述以
自相似方法重複事物的過程。例如,當兩面鏡子相互之間近似平行時,鏡中嵌套的圖像是以無限遞歸的形式出現的。也可以理解為自我複製的過程。
- 參考資料
-
-
1.
C. A. R. Hoare. "An axiomatic basis for computer programming". Communications of the ACM, 12(10):576–585, October 1969. doi:10.1145/363235.363259
-
2.
Stokey, Nancy,; Robert Lucas; Edward Prescott. Recursive Methods in Economic Dynamics. Harvard University Press. 1989. ISBN 0674750969.