Блог

Главная - Вопросы по программированию - Инвариант цикла Java

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

#java #logarithm #invariants #loop-invariant

#java #логарифм #инварианты #инвариант цикла

Вопрос:

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

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

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

Ответ №1:

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

Комментарии:

1. Хотя это правильно, это не так строго, как вы можете быть для последующего условия. 5 <= 1024 = 2 ^ 10 могло бы быть примером этого, но 10, очевидно, не было бы правильным журналом. Конечно, метод действительно частично корректен, и можно было бы показать более сильное постусловие

Ответ №2:

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

Ответ №3:

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

Ответ №4:

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

 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))}

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