Use um invariante do laço para provar que o algoritmo a seguir está correto.
(a) Condições prévias: .
(b) Condições posteriores: !.
\(x \leftarrow 1\)
\(i \leftarrow 1\)
enquanto \(i<n\) fazer
    \(\ulcorner i \leftarrow i+1\)
    \(\ulcorner x \leftarrow x \cdot i\)

Passo 1

O enunciado nos dá o seguinte algoritmo que recebe um número natural n e, ao final, deve deixar em x o valor de n!.
Condições prévias: ninN.
Condições posteriores esperadas: x = n!.
O conteúdo é prova de correção de programa por invariante de laço. Vamos escolher e verificar um invariante adequado.

Passo 2

Escolhemos como invariante de laço a propriedade
I: x = i!e 1 <= i <= n
Isto significa que, em todo ponto de entrada do corpo do laço, x guarda o fatorial de i, e i nunca ultrapassa n.

Passo 3

(Inicialização) Antes de entrar no laço temos
i 1, x 1
Então x=1 e i=1, de modo que
x = 1 = 1! = i!,
e claramente 1 <= i <= n. Logo I vale antes da primeira verificação de i<n.

Passo 4

(Preservação) Suponha que I seja verdadeiro no início de uma iteração, ou seja, x = i! e 1<= i<n. O corpo do laço faz
i i+1, x x cdot i
Após i i+1, o novo valor de i é inovo = iantigo+1. Então, ao executar x xcdot i, temos
xnovo = xantigocdot inovo = iantigo! ,cdot (iantigo+1) = (inovo)!
Além disso, como iantigo<n, segue inovo<= n. Então a propriedade I continua válida.

Passo 5

(Terminação) O laço é “enquanto i<n”. Quando ele termina, a condição de continuação falha, ou seja, i>= n. Mas pelo invariante sabemos também que i<= n. Logo na saída do laço temos i = n. Pelo invariante, x = i! = n!. Assim a condição posterior x=n! se cumpre.

Resposta

Provamos que, partindo de ninN, o algoritmo termina com x=n!, logo está correto.

Exercícios de Livros Relacionados