Как мне придумать инвариант цикла для псевдокода, который вычисляет нечетное число?

#loops #numbers #pseudocode #loop-invariant

Вопрос:

Я изо всех сил пытаюсь придумать инвариант цикла для следующего фрагмента кода:

Странный номер(n)

  1. a = 2
  2. для i = от 1 до n сделайте
  3.     a = a * i
     
  4. возврат a 1

Теперь я хочу найти инвариант цикла, который является правильным, прежде чем вводить цикл for в п. 2.Моя идея заключалась в том, что a = произведение от k=1 до i-1, умноженное на 2, однако у меня возникли проблемы с добавлением 1 в конце.

Комментарии:

1. a всегда четно — это инвариант цикла.

2. тогда как бы я продолжал доказывать это с помощью индукции?

3. Легко. Основание a=2 — оно четное. Тогда четное число, умноженное на любое другое (естественное) число, всегда тоже четное.

4. Но значение 1 добавляется в конце цикла, так что a никогда не может быть четным, не так ли? Независимо от того, как часто вы умножаете значение a на i, в конце концов вам всегда придется добавить 1

5. И что? Инвариант все еще существует, a он даже есть. Любое четное число 1 является нечетным. Что ты пытаешься доказать?