Правильность алгоритма, используя математическую индукцию? Опции

[Perfez]

Предоставляется такой, довольно-таки простой код с пре- и пост- условиями:

Код

#предусловие: bit - есть непустая последовательность из нулей и/или единиц
r = 0
t = 1
for i in range(len(bit)):
    r += t * bit[i]
    t *= -1
# постусловие: r делится на 3 если только число с бинарным представлением:
# bit[0] bit[1] bit[2] ... bit[len(bit)-1]
# делится на 3.

А мне собственно интересно, как доказать (математически) то, что алгоритм правилен в принципе

p.s.
Пробовал делать такое через инвариант цикла, но в итоге ничего - выяснилось лишь то, что инвариант в этом случае будет равен
t = -1^{range(len(bit))}

Сообщение отредактировано: Perfez - 2.03.2011 12:41

[TarasBer]

Надо доказать, что число в 2ичной системе счисления делится на 3, согда знакопеременная сумма его цифр делится на 3.

В более общем виде - число имеет тот же остаток от деления на n+1, что и знакопеременная сумма его цифр в n-ичной системе счисления.

Итак, есть число

a0 + a1*n + a2*n*n + a3*n*n*n + a4*n*n*n*n + ...

вычитаем из него (a0-a1+a2-a3+a4-...)
получаем

(a0*(1-1)) +
(a1*(n+1)) +
(a2*(n*n-1)) +
(a3*(n*n*n+1)) +
(a4*(n*n*n*n-1)) + ...

известно, что n^(2k)-1 делится на n+1 : n^(2k)-1 = (n^2-1)(1+n^2+...+n^(2k-2)) = (n+1)(n-1)(1+n^2+...+n^(2k-2))

и что n^(2k+1)+1 делится на n-1: n^(2k+1)+1 = (n+1)(1-n+n^2-...+n^(2k))
значит и вся сумма делится на n+1
а если разность двух чисел делится на n+1, значит у них одинаковый остаток от деления на него.

[Perfez]

просто, и со вкусом (с)

TarasBer, благодарю