ime_2/Exercícios/03 - Logaritmos/Logaritmos.md

Logaritmos

Exercícios 2

1. Prove os dois invariantes da primeira versão da função lg:

int lg (int N)
{  
   int i, n;
   i = 0;
   n = 1;
   while (n <= N/2) {
      n = 2 * n;
      i += 1;
   }
   return i;    
}

Um invariante é uma propriedade a qual invariavelmente é verdadeira durante toda a execução de um loop, de tal forma que a corretude deste pode ser demonstrada se a invariante se mantêm verdadeira

• antes da iteração inicial (i = 0),

• para cada iteração subsequente (se verdadeira em i = k, também o é para i = k + 1)

• e ao término do loop (i = n, onde n é o valor de parada)

Para o algoritmo acima, seja N \in \N, temos como invariantes que n \le N e i = \log_2n.

Prova

Para n temos:

• Inicialização: Para N = 1, n_0 = 1, então n_0 \le N.

• Manutenção: Para N = k na iteração x, x > 0, assumimos n_x \le k/2. Ai para iteração x + 1 temos que o valor de n_{x + 1} = 2n_x. Como n_x \le k/2, tem-se que n_{x + 1} \le k, ou seja, n_{x + 1} \le N.

• Término: Para se encerrar na iteração x tem-se que n_x > N/2 seja porque n = N = 1 ou, senão, porque n_x > N \div 2 quando n_{x - 1} \le N/2. No primeiro caso nada resta a demonstrar, mas no segundo caso segue que n_x = 2n_{x - 1}, então