Invariante de tabela dinâmica sob inserção
[Enunciado do exercício.]
Queremos mostrar que
no início de cada iteração (linha 25)
a poupança tem pelo menos 2m − t moedas.
Eis a prova.-
A propriedade vale no início da primeira iteração
pois nessa ocasião m = t = 1.
Suponha agora que a propriedade vale
no início de uma iteração qualquer.
Há dois casos a considerar:
-
Se m < t,
a iteração custará 1 moeda.
No fim da iteração,
m terá aumentado em 1 unidade e
t terá permanecido constante,
donde o valor da expressão 2m−t
terá aumentado em 2 unidades.
Por outro lado, a poupança de moedas terá aumentado em 3−1 = 2 unidades.
Logo, no início da próxima iteração,
continuaremos tendo pelo menos 2m−t moedas na poupança.
-
Se m = t,
a iteração começará com pelo menos 2m−t = m moedas
na poupança e custará m+1 moedas.
Como a poupança ganha 3 novas moedas,
teremos pelo menos 2 moedas na poupança no fim da iteração.
Por outro lado, no fim da iteração,
t estará valendo o dobro do valor original de m
e m terá aumentado em 1 unidade.
Logo, o novo valor da expressão 2m−t
será exatamente 2.
Assim, no início da próxima iteração,
a tabela continuará tendo pelo menos 2 = 2m−t
moedas na poupança.
Provamos assim que a poupança tem pelo menos 2m − t
moedas no início de cada iteração.