我在看Hoare Logic，並且在理解找到循環不變的方法時遇到了問題。 有人可以解釋用於計算循環不變的方法嗎？ 什麼循環不變應該包含一個「有用」的？ 我只處理簡單的例子，發現不變量並證明部分和完全校正的例子，如： { i ≥ 0 } while i > 0 do i := i−1 { i = 0 }
int logarithmCeiling(int x) {
int power = 1;
int count = 0;
while (power < x) {
power = 2 *power;
count = count +1;
}
return count;
}
上面的代碼是爲了使用while循環計算並返回給定正