Use um invariante de laço para provar que o algoritmo a seguir está correto.
Condições prévias: é um número natural ímpar.
Condições posteriores: .
\(s \leftarrow 1\)
\(i \leftarrow 1\)
enquanto \(i<n\) fazer
    \(\ulcorner i \leftarrow i+2\)
    \(\ulcorner s \leftarrow s+i\)

Passo 1

O enunciado nos dá o algoritmo abaixo, com pré-condição “ n é um número natural ímpar” e pós-condição desejada “ s = l(n+12r)^2":
s 1
i 1
enquanto i < n fazer
i i + 2
s s + i
O objetivo é provar a correção do laço usando um invariante de laço, isto é, encontrar uma propriedade I(i,s) que seja verdadeira ao iniciar, permaneça verdadeira a cada iteração e, ao sair do laço, leve à pós-condição.

Passo 2

Escolhemos como invariante a relação entre s e i que expressa a soma dos primeiros i+12 números ímpares. Definimos
I: s = l(tfraci+12r)^2 e i é ímpar, 1 <= i <= n éí
Em palavras, após cada iteração s guarda o quadrado do número de termos ímpares somados até então, e i é exatamente o último ímpar somado.

Passo 3

(Inicialização)
Antes de entrar no laço fazemos s1 e i1. Então
tfraci+12 = tfrac1+12 = 1 Longrightarrow l(tfraci+12r)^2 = 1 = s,
logo I vale inicialmente. Além disso i=1 é ímpar e 1<= i<= n por hipótese em n.

Passo 4

(Manutenção)
Suponha que, no início de uma iteração em que i<n, valha
s = l(tfraci+12r)^2 e i ímpar í
O corpo do laço faz
i' = i + 2, s' = s + i'
Então, usando a hipótese s = l(i+12r)^2, temos
s' = l(tfraci+12r)^2 + (i+2)
Transformando em um único quadrado:
s' = (i+1)^24 + 4(i+2)4 = i^2 +2i +1 +4i +84 = i^2+6i+94 = l(tfraci+32r)^2
Mas i' = i+2 implica tfraci'+12 = tfraci+32. Logo
s' = l(tfraci'+12r)^2
e i' = i+2 continua ímpar, preservando I.

Passo 5

(Terminação)
O laço termina quando a condição i<n falha, ou seja, quando i>= n. Como i caminha de 1 em 1 + 2 + 2 + cdots até atingir um valor ímpar não superior a n, a única possibilidade é i=n. Nesse ponto, o invariante dá
s = l(tfraci+12r)^2 = l(tfracn+12r)^2,
que é exatamente a pós-condição desejada.

Resposta

O algoritmo está correto, pois o invariante de laço
s = l(tfraci+12r)^2
é válido na inicialização, é mantido a cada iteração e leva à pós-condição s = l(tfracn+12r)^2 no término do laço.

Exercícios de Livros Relacionados