Изо всех сил пытается найти правильный инвариант цикла - PullRequest
Новая
       6

Изо всех сил пытается найти правильный инвариант цикла

0 голосов
/ 30 октября 2018

У меня есть следующий код: 

public static void main(String[] args) {
    int a = 3;
    int b = 7;

    int x = b; // x=b
    int res = a; // res = a
    int y = 1;

    int invariant = 0;

    System.out.println("a|b|x|y|res|invariant");
    while (x > 0) { 
        if (x % 2 == 0) {
            y = 2 * y;
            x = x / 2;  
        } else {
            res = res + y;
            y = 2 * y;
            x = (x - 1) / 2;
        }
        invariant = y + 2;
        String output = String.format("%d|%d|%d|%d|%d|%d", a,b,x,y,res,invariant);
        System.out.println(output);
    }
    // < res = a + b >
}

Что дает следующий вывод: 

a|b|x|y|res|invariant
3|7|3|2|4|4
3|7|1|4|6|6
3|7|0|8|10|10

Однако, если я изменю числа, инвариант больше не будет равен резолюции. Поэтому мой инвариант цикла для этой задачи не верен.

Я изо всех сил пытаюсь найти правильный инвариант цикла и был бы рад, если есть какие-то подсказки, которые кто-то может дать мне.

Мое первое впечатление после изучения кода и моих результатов заключается в том, что инвариант цикла изменяется в зависимости от a и b. Допустим, и a, и b являются нечетными числами, как они есть в моем примере, тогда мой инвариант Loop является правильным (по крайней мере, так кажется)

Правильно ли предположить вариант цикла, подобный следующему? 

< res = y - 2 && a % 2 != 0 && b % 2 != 0 >

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

Я был бы очень признателен, если бы кто-нибудь дал мне подсказку или общее представление о том, как это решить.

Спасибо

1 Ответ

0 голосов
/ 30 октября 2018

Этот цикл вычисляет сумму a+b. res инициализируется до a. Затем в каждой итерации цикла следующий бит двоичного представления b (начиная с младшего бита) добавляется к res до тех пор, пока цикл не закончится и res не будет содержать a+b.

Как это работает:

x инициализируется до b. В каждой итерации вы исключаете наименее значимый бит. Если этот бит равен 0, вы просто делите x на 2. Если это 1, вы вычитаете 1 и делите на 2 (на самом деле этого будет достаточно для деления на 2, поскольку (x-1)/2==x/2, когда х нечетный int). Только когда вы встретите бит 1, вы должны добавить его (умноженное на правильную мощность 2) к результату. y Содержит правильную силу 2.

В вашем примере a = 3, b = 7 двоичное представление b равно 111

  • На первой итерации значение res равно + 1 (двоичный) == a + 1 = 4
  • Во второй итерации значение res равно + 11 (двоичное) == a + 3 = 6
  • На последней итерации значение res равно + 111 (двоичное) == a + 7 == 10

Вы можете написать инвариант как: 

invariant = a + (b & (y - 1));

Здесь используется тот факт, что в конце i -ой итерации (i начиная с 1) y содержит 2^i, поэтому y - 1 == 2^i - 1 - это число, двоичное представление которого составляет i 1 бит (т. е. 11...11 с i бит). Когда вы & наберете это число с помощью b, вы получите i младшие значащие биты b.

...