Na Seção 5.2, fizemos a afirmação de que o algoritmo
para i in1,2, ldots<n fazer
visitar xi
visita cada elemento no vetor x1, x2, ldots, xn exatamente uma vez. Demonstre formalmente essa afirmação usando um invariante do laço. (Dica: primeiro, reescreva o algoritmo usando um laço-enquanto em vez de um laço-para.)

Passo 1

Resumindo, temos o algoritmo que para i variando de 1 até n chama
visitar(xi)
Queremos provar que cada elemento do vetor x1,x2,dots,xn é visitado exatamente uma vez. Para isso, primeiro reescrevemos o laço-para como um laço-enquanto e depois apresentamos um invariante de laço que demonstre formalmente essa propriedade.

Passo 2

Reescrevendo o laço-para como laço-enquanto, temos
i &>=ts 1; enquanto ,i <= nfaça ;visitar(xi); ;i >=ts i + 1; fim-enquanto ç
Agora definimos o invariante de laço:
Invariante P(i): “No início de cada iteração do laço-enquanto, para todo índice j tal que 1 <= j < i, a chamada visitar(xj) já foi executada exatamente uma vez, e para todo k com i <= k <= n, visitar(xk) ainda não foi executada.”

Passo 3

Verificação da inicialização: antes de entrar no laço, i=1.
Nesse momento, o conjunto de índices j com 1 <= j < i é vazio, logo nenhuma chamada visitar foi feita. E, de fato, para todo k com 1 <= k <= n, visitar(xk) ainda não ocorreu. Portanto, P(1) é verdadeira.

Passo 4

Manutenção do invariante: suponha que P(i) seja verdadeira no início de uma iteração com i <= n. O corpo do laço faz exatamente duas ações:
  1. Executa visitar(xi), de modo que agora xi é visitado exatamente uma vez;
  2. Incrementa i para i+1.
    Após essas ações, para todo j< i (antes do incremento) já tínhamos cada visitar(xj) uma vez, e agora também temos visitar(xi) uma vez. Além disso, para k >= i+1 ainda não foi chamada visitar(xk). Logo, P(i+1) vale. Isso mostra que o invariante se mantém.

Passo 5

Término do laço: o laço para quando i=n+1. Nesse ponto, pelo invariante P(n+1), sabemos que para todo j com 1<= j< n+1, ou seja 1<= j<= n, a chamada visitar(xj) foi feita exatamente uma vez. E não há índices k com k>= n+1 no vetor. Assim, todos e somente os elementos x1,dots,xn foram visitados exatamente uma vez.

Resposta

O invariante de laço
P(i): exatamente os e<=mentos x1,dots,xi-1 já foram visitados uma vez e os demais ainda não áã
é verdadeiro na inicialização, mantido em cada iteração e garante, na terminação, que cada xj ( 1<= j<= n) foi visitado exatamente uma vez. Portanto, a afirmação está demonstrada.

Exercícios de Livros Relacionados