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

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

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

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


java logarithm invariants loop-invariant
person Paradox    schedule 23.05.2011    source источник

Ответы (4)


arrow_upward
1
arrow_downward

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

person astay13    schedule 23.05.2011
comment
Хотя это правильно, это не так строго, как вы можете быть для пост-условия. 5 ‹= 1024 = 2^10 Может быть примером этого, но 10 явно не будет правильным журналом. Конечно, метод действительно частично корректен, и можно было бы показать более сильное постусловие. - person b.buchhold; 23.05.2011

arrow_upward
0
arrow_downward

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

person Ted Hopp    schedule 23.05.2011

arrow_upward
0
arrow_downward

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

person Ryan    schedule 23.05.2011

arrow_upward
0
arrow_downward

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

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

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

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

это именно то, что вам нужно для демонстрации частичной правильности всей функции.

person b.buchhold    schedule 23.05.2011