Код
#предусловие: 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 = -1range(len(bit))
Сообщение отредактировано: Perfez -