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

[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