01. Algoritmo de busca binária:

============================================================
Algoritmo: busca_bin.
Entrada: um vetor ORDENADO A[1..n] de números, um número x.
Saída: um número de 0 a n.
------------------------------------------------------------
01. i := 1
02. j := n
    // INVARIANTE: se existe k tal que A[k] = x, então i <= k <= j.
03. ENQUANTO i <= j
04. | m := (i+j) div 2
05. | SE x = A[m]
06. | | RETORNE m
07. | SE x < A[m]
08. | | j := m-1
09. | SENÃO
10. | | i := m+1
11. RETORNE 0
============================================================

02. EXERCÍCIO: prove que a afirmação acima da linha 3 é de fato um invariante do laço do algoritmo acima.

03. EXERCÍCIO: mostre que a função f(i,j) = j-i+1 é um(a) variante do laço acima.

04. LEMA: o laço do algoritmo acima executa no máximo 1 + lg(n) iterações.
    (Observação: lg(n) = log_2(n).)

===================================================
---------------------- PROVA ----------------------
Nós mostraremos o lema demonstrando o seguinte resultado:
  para qualquer iteração do laço do algoritmo,
  se, no início da iteração, vale "j-i+1 = h",
  então o laço executará no máximo mais 1 + lg(h) iterações,
  incluindo a iteração em questão.
Por indução em h:

* Base (h = 1):
  Como h=1, então i=j. Temos que mostrar então que no máximo 1 + lg(0) = 1 será ainda executada,
  ou seja, que nenhuma iteração será executada depois da iteração atual.
  De fato, um dos seguintes casos ocorre na iteração em questão:

  Caso 1: A[m] = x. Logo, o algoritmo retornará pela execução da linha 6 e nenhuma iteração do laço ocorrerá além da atual, cqd.
  Caso 2: A[m] != x. Logo, ou x < A[m] ou x > A[m], e, em ambos os casos, teremos j<i ao final da iteração em questão, e portanto o laço terminará sem que nenhuma iteração seja executada em adição à iteração em questão, cqd.

* HIPÓTESE DE INDUÇÃO: para todo h' < h, se j-i+1 = h' no início de uma iteração,
  então o laço executará no máximo mais 1 + lg(h') iterações.

* Passo (h > 1):
  Temos que mostrar que no máximo mais 1 + lg(h) serão executadas.
  Como antes, um dos seguintes casos ocorre na iteração atual:

  Caso 1: A[m] = x. Nesse caso, o algoritmo retornará pela execução da linha 6 e nenhuma iteração do laço será executada depois da iteração atual. Logo, como 1 < 1 + lg(h), o resultado está provado.

  Caso 2: A[m] != x. Nesse caso, ou j ou i receberá novo valor e o intervalo da iteração seguinte terá tamanho no máximo h/2.
  Logo, aplicando-se a hipótese de indução, temos que o laço executará, após a iteração atual,
  no máximo outras 1 + lg(h/2) iterações. Assim, incluindo a iteração atual,
  o algoritmo executa no máximo mais 1 + 1 + lg(h/2) = 1 + lg(h) iterações, cqd.
---------------------- PROVA ----------------------
===================================================