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

Java循环不变

回答

相关问题