00. O algoritmo de busca linear da aula anterior:

============================================
Algoritmo: busca_linear
Entrada: um vetor A[1..n] e um elemento x
Saída: um número de 0 a n
--------------------------------
1. i := 1
   // invariante: para todo k de 1 a i-1, A[k] != x
2. ENQUANTO i <= n
3. | SE A[i] = x
4. | | RETORNE i
5. | i := i + 1
6. RETORNE 0.
============================================

01. DEFINIÇÃO: dado um laço de um programa qualquer, um VARIANTE DO LAÇO em questão é uma função definida sobre o estado do programa em questão, que assume valores num conjunto que possua uma relação de ordem bem-fundada, e que possua ainda a propriedade de que o seu valor sempre diminui após a execução de uma iteração qualquer do laço.
    A importância de se encontrar variantes para laços é que todo laço que possui um(a) variante termina.
    OBSERVAÇÃO: uma relação de ordem bem-fundada é uma relação < tal que não existe uma sequência infinita de elementos a_0, a_1, a_2, etc, tal que a_0 > a_1 > a_2 > ... .

02. Exemplo de variante de laço: a função
  
    f : ESTADOS -> Z : (i,n) |-> n-i+1

    é um variante do laço do algoritmo busca_linear. A prova se encontra abaixo.

03. LEMA (EXERCÍCIO): "1 <= i <= n+1" é um invariante do laço de busca_linear.

04. LEMA: provando o exemplo 2.

=================================
------------- PROVA -------------
Temos que mostrar o seguinte:

a) Que f apenas assume valores naturais: pelo lema 3, temos que "i <= n+1" é válido no início de qualquer iteração do laço. Logo, no início de qualquer iteração do laço, temos n-i+1 >= 0, CQD.

b) Que o valor de f decresce após cada iteração do laço: suponha que, no início de uma iteração qualquer do laço, a variável i assume o valor "j". Logo, o valor de f no início da iteração em questão é n-j+1. Agora, se a execução da iteração em questão chega ao fim, então a linha 4 não é executada, e portanto a linha 5 é executada. Logo, ao final da iteração, a variável i vale "j+1", e portanto f vale n-(j+1)+1 = n-j < n-j+1, CQD.
------------- PROVA -------------
=================================

5. TEOREMA: o algoritmo busca_linear é correto -- isto é, ele termina e retorna uma resposta correta, a saber, 0, se "x" não ocorre em "A", ou, em caso contrário, um índice i de 1 a n tal que A[i] = x.

=================================
------------- PROVA -------------
Pelo lema 4, o laço do algoritmo busca_linear sempre termina, e portanto o mesmo vale para o algoritmo como um todo. Assim, resta apenas mostrar que o valor retornado pelo algoritmo é correto. Observe então que os casos possíveis são os seguintes:

------------
Caso 1: o algoritmo termina pela execução da linha 4. Nesse caso, o algoritmo retorna um índice i tal que A[i] = x, e portanto a resposta retornada é correta. (Observação: o índice i retornado está sempre no intervalo de [1,n], pois, pelo lema 3, vale 1 <= i, e, além disso, se a linha 4 é executada, então, para o valor em questão de i, a condição do laço é verdadeira, ou seja, i <= n.)

Caso 2: o algoritmo não termina pela execução da linha 4. Nesse caso, o algoritmo certamente termina pela execução da linha 6. Agora, pelo lema da aula anterior, "para todo k de 1 a i-1, A[k] != x" é um invariante do laço do algoritmo. Consideremos agora o estado do algoritmo ao fim da execução do laço. O valor de i é certamente n+1, pois "1 <= i <= n+1" é um invariante do laço e, além disso, a condição do laço é falsa, ou seja, i > n. Aplicando o valor de "i" no invariante provado na aula anterior, obtemos "para todo k de 1 a n, A[k] != x", ou seja, o elemento x não ocorre no vetor, e portanto o valor retornado (zero) é correto.
------------

A análise de casos acima mostra que o valor retornado pelo algoritmo é sempre correto, CQD.
------------- PROVA -------------
=================================

6. DEFINIÇÃO: uma demonstração de CORREÇÃO PARCIAL de um algoritmo consiste na argumentação de que, se o algoritmo termina, então ele retorna uma resposta correta. A CORREÇÃO TOTAL de um algoritmo é a demonstração da correção parcial e da terminação, isto é, de que o algoritmo sempre termina E retorna uma resposta correta.
   Assim, por exemplo, o teorema 5 acima mostra a correção total do algoritmo busca_linear.