Инвариант цикла Java

Question

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

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

Приведенный выше код предназначен для использования в Java как метод вычисления и возврата нижнего логарифма заданного положительного целого числа с использованием цикла while.Как бы я предоставил инвариант для цикла выше?т. е. это имеет место до его начала, каждый раз, когда заканчивается тело цикла, и отрицание условия цикла.

Answer 1

мощность всегда равна 2 ^ отсчет в начале и в конце цикла.Для отрицания, когда цикл закончен, x <= power = 2 ^ count. </p>

Answer 2

Полагаю, вы ищете инвариант, который подходит для доказательства частичной правильности метода?В противном случае «истина» или «ложь» всегда являются инвариантами.Я бы пошел с чем-то вроде этого:

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

RHS может подразумеваться из ваших инициализаций и помогает обеспечить нижнюю границу для x.Вместе с условием отрицательной петли вы можете позже подразумевать.

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

, что именно то, что вы хотите, чтобы показать частичную корректность всей функции.

Answer 3

Ищите переменные или условия, которые всегда верны. Каждый счетчик итераций всегда увеличивается на 1, а мощность всегда умножается на 2. Поскольку целью функции является поиск нижнего логарифма заданного аргумента, можно сказать, что инвариант цикла состоит в том, что счетчик всегда равен логарифму х, округлено вниз. Другим из них будет то, что число всегда равно логарифму мощности.

Answer 4

Существует простая связь между значением power и значением count: power = 2 ^count . Это верно в начале и в конце цикла, но не в определенных местах в теле цикла.