Как правильно выбрать и установить инвариант цикла?

Question

Мне дали следующую задачу об инвариантах цикла:

Рассмотрим

x=4; for(i=5;i<k;i++) { a=a+x+i; x=x*2; }

Определите инвариант подходящего цикла, который использует замкнутую формулу для a и x.

Теперь, Как вы знаете, у вас есть правильный инвариант цикла здесь? Я имею в виду, что вы можете установить инвариант цикла следующим образом: «На j-й итерации« x »меньше, чем« a »», что будет правильно, но не будет использовать какие-либо замкнутые формулы, верно?

Как можно использовать оператор (инвариант цикла), чтобы определить значение "a", когда цикл закончен? Все примеры, которые я видел, просто устанавливают инвариант цикла и он не используется в качестве замкнутой формулы.

Есть идеи?

Спасибо за вашу помощь.

Answer 1

Начните с замкнутых формул: ясно для x (j) [для j от 0 до k-5], x при входе в j-ую ветвь цикла, x(j+1) = x(j) * 2, поэтому x(j) равно 4 * 2**j (используя ** для "повышения до власти"), поскольку x(0) равно 4; и a(j+1) = a(j) + x(j) + j + 5 - нам не говорят, что такое a(0), но мы можем выделить это и записать a(j) как a(0) + что-то. Можете ли вы выяснить, что это такое, учитывая приведенное выше решение с закрытой формулой для x(j)? Я не хочу делать твою домашнюю работу от тебя - ты уже начал изучать Конкретную математику или что там у тебя в учебнике ...?

Как только вы запишете формулу замкнутой формы для a(j), чтобы перейти к тривиальной формуле, которую я предоставил для x(j), вы можете увидеть, как они объединяются, чтобы сделать инвариант цикла ...?