Java循環不變

int logarithmCeiling(int x) { 
    int power = 1; 
    int count = 0; 

    while (power < x) { 
     power = 2 *power; 
     count = count +1; 
    } 
    return count; 
}

上面的代碼是爲了使用while循環計算並返回給定正整數的較低對數的Java方法。我將如何爲上面的循環提供一個不變量？即在其開始之前保持，每當循環體結束時，以及循環條件的否定。Java循環不變

來源

2011-05-23 Paradox

在循環的開始和結束時，電源總是等於2^count。對於否定，當循環結束時，x < = power = 2^count。

來源

2011-05-23 14:55:27 astay13

雖然正確，但這並不像您對後期條件那樣嚴格。 5 <= 1024 = 2^10可能是這樣的一個實例，但是10個明顯不會是正確的日誌。當然，這個方法確實是部分正確的，並且可以顯示更強的後置條件 – 2011-05-23 16:14:28

power的值與count的值之間存在一個簡單的關係：power = 2 ^count。這在循環的開始和結束處保持不變，但不在循環體中的某些地方。

來源

2011-05-23 14:48:35

查找始終爲真的變量或條件。每次迭代計數總是加1，並且功率總是乘以2.因爲函數的目的是找到給定參數的較低對數，所以可以說循環不變是計數總是等於x，向下舍入。另一個將是計數總是等於權力的對數。

來源

2011-05-23 14:49:24 Ryan

我想你正在尋找一個適合證明方法的部分正確性的不變量嗎？否則，「真」或「假」永遠是不變的。我會去這樣的事情：

I: {(power <= x) AND (power == 2^count) AND (x > 2^count -1) AND (power >= 1)}

該r.h.s.可以從您的初始化中隱含，並有助於確保x的下限。連同你可以稍後暗示的否定循環條件。

{(x <= 2^count) AND (x > 2^(count -1))}

這正是你想要顯示整個功能的部分正確性。

來源

2011-05-23 15:00:19

回答

相關問題