![]() |
![]() |
Perfez |
![]()
Сообщение
#1
|
![]() Бывалый ![]() ![]() ![]() Группа: Модераторы Сообщений: 231 Пол: Женский Репутация: ![]() ![]() ![]() |
Предоставляется такой, довольно-таки простой код с пре- и пост- условиями:
Код #предусловие: 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 - 2.03.2011 12:41 |
![]() ![]() |
![]() |
Текстовая версия | 21.06.2024 19:52 |