Доказательство правильности алгоритма по индукции

Question

Недавно я начал читать книгу о структурах данных, и она начинается с введения в алгоритмы. В одном упражнении он просит доказать алгоритм по индукции и инвариант цикла. Алгоритм в псевдокоде:

Algorithm DEC2BIN(int n, int[] b)
Input: int n, array b
Output: b[i] contains the i-th bit of n's binary representation.

1: int x=n, k=0;
2:while(x>0){
3:   b[k]=x%2;
4:   x/=2;
5:   k++;
6:}
en of DEC2BIN

Я сказал:

Пусть P(n) будет утверждением "b содержит двоичное представление n".

Для n=1: очевидно, что b=[1], поэтому P(1).

Пусть P(N). Как я могу показать P(n+1)?

Answer 1

Начните с предоставления правильного цикла-инварианта. Например

"После запуска k цикла б будет содержать первый k цифры двоичного представления n".

Метод Хорнера и Позиционные Системы должны сделать все возможное, чтобы доказать утверждение, начиная с указанного выше инварианта цикла.