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\)
(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
e, ao final, deve deixar em
o valor de
.
Condições prévias: .
Condições posteriores esperadas: .
O conteúdo é prova de correção de programa por invariante de laço. Vamos escolher e verificar um invariante adequado.
Condições prévias:
Condições posteriores esperadas:
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
Isto significa que, em todo ponto de entrada do corpo do laço,
guarda o fatorial de
, e
nunca ultrapassa
.
Passo 3
(Inicialização) Antes de entrar no laço temos
Então
e
, de modo que
e claramente
. Logo
vale antes da primeira verificação de
.
Passo 4
(Preservação) Suponha que
seja verdadeiro no início de uma iteração, ou seja,
e
. O corpo do laço faz
Após
, o novo valor de
é
. Então, ao executar
, temos
Além disso, como
, segue
. Então a propriedade
continua válida.
Passo 5
(Terminação) O laço é “enquanto
”. Quando ele termina, a condição de continuação falha, ou seja,
. Mas pelo invariante sabemos também que
. Logo na saída do laço temos
. Pelo invariante,
. Assim a condição posterior
se cumpre.
Resposta
Provamos que, partindo de
, o algoritmo termina com
, logo está correto.