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\)
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 “
é um número natural ímpar” e pós-condição desejada “
":
enquanto
O objetivo é provar a correção do laço usando um invariante de laço, isto é, encontrar uma propriedade
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
e
que expressa a soma dos primeiros
números ímpares. Definimos
Em palavras, após cada iteração
guarda o quadrado do número de termos ímpares somados até então, e
é exatamente o último ímpar somado.
Passo 3
(Inicialização)
Antes de entrar no laço fazemos e
. Então
Antes de entrar no laço fazemos
logo
vale inicialmente. Além disso
é ímpar e
por hipótese em
.
Passo 4
(Manutenção)
Suponha que, no início de uma iteração em que , valha
Suponha que, no início de uma iteração em que
O corpo do laço faz
Então, usando a hipótese
, temos
Transformando em um único quadrado:
Mas
implica
. Logo
e
continua ímpar, preservando
.
Passo 5
(Terminação)
O laço termina quando a condição falha, ou seja, quando
. Como
caminha de
em
até atingir um valor ímpar não superior a
, a única possibilidade é
. Nesse ponto, o invariante dá
O laço termina quando a condição
que é exatamente a pós-condição desejada.
Resposta
O algoritmo está correto, pois o invariante de laço
é válido na inicialização, é mantido a cada iteração e leva à pós-condição
no término do laço.