Докажите по индукции, что инвариант цикла выполняется

//Precondition: n > 0
//Postcondition: returns the minimum number of decial digits
//               necessary to write out the number n

 int countDigits(int n){
1.    int d = 0;
2.    int val = n;
3.    while(val != 0){
4.        val = val / 10;     // In C++: 5 / 2 === 2
5.        d++;
6.    }
7.    return d;
}

Инвариант: непосредственно перед оценкой защиты от петель в строке 3, n с удаленными крайними правыми цифрами d идентичен val. (Предположим, что для записи числа 0 требуется 0 цифр, и это единственное число, для записи которого требуется 0 цифр).

Докажите по индукции, что инвариант цикла верен.

Я всегда думал, что доказательство с помощью индукции предполагает, что при замене переменной в уравнении на k будет истинным, тогда я должен доказать, что k + 1 также будет истинным. Но на самом деле в этом вопросе мне дается не уравнение, а просто блок кода. Вот мой базовый вариант:

Непосредственно перед оценкой защиты от петель в строке 3 значение d равно 0, а в строке 2 - val == n, поэтому, если у n удалена крайняя правая цифра 0, это будет val. Следовательно, базовый случай имеет место.

Я не совсем уверен, как написать индуктивный шаг после этого, так как я не уверен, как доказать k + 1 ..


induction proof
person user3567126    schedule 24.04.2014    source источник
comment
Обратите внимание, что вам не обязательно проводить индукцию по одной из переменных; вы рассматривали индукцию по длине n?   -  person Joost    schedule 25.04.2014
comment
извините, что вы имеете в виду под длиной n?   -  person user3567126    schedule 25.04.2014

Ответы (1)


arrow_upward
0
arrow_downward

Логика действительно такая же, как и с уравнением, за исключением того, что вы заменяете значение k в своем уравнении на n итерацию цикла:

  1. базовый случай состоит в том, что инвариант цикла сохраняется перед запуском цикла;
  2. вы должны доказать, что если инвариант сохраняется до итерации N, он все равно будет сохраняться после выполнения итерации N.

Из 1. и 2. по индукции заключаем, что инвариант сохраняется в конце цикла (или, фактически, в конце любой итерации).

ИЗМЕНИТЬ, и это интересно, потому что цикл заканчивается на val == 0. Ваш инвариант (все еще верный в конце цикла) равен n с удаленными крайними правыми цифрами d, идентичен val, поэтому n с удаленными d цифрами идентичен 0 в этой точке, поэтому d правильно количество цифр, необходимое для отображения n.

person jods    schedule 24.04.2014