Na Seção 5.2, fizemos a afirmação de que o algoritmo
para
fazer
visitar
visita cada elemento no vetor
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.)
para
visitar
visita cada elemento no vetor
Passo 1
Resumindo, temos o algoritmo que para
variando de
até
chama
Queremos provar que cada elemento do vetor
é 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
Agora definimos o invariante de laço:
Invariante : “No início de cada iteração do laço-enquanto, para todo índice
tal que
, a chamada
já foi executada exatamente uma vez, e para todo
com
,
ainda não foi executada.”
Invariante
Passo 3
Verificação da inicialização: antes de entrar no laço,
.
Nesse momento, o conjunto de índices com
é vazio, logo nenhuma chamada
foi feita. E, de fato, para todo
com
,
ainda não ocorreu. Portanto,
é verdadeira.
Nesse momento, o conjunto de índices
Passo 4
Manutenção do invariante: suponha que
seja verdadeira no início de uma iteração com
. O corpo do laço faz exatamente duas ações:
- Executa
, de modo que agora é visitado exatamente uma vez; - Incrementa
para .
Após essas ações, para todo(antes do incremento) já tínhamos cada uma vez, e agora também temos uma vez. Além disso, para ainda não foi chamada . Logo, vale. Isso mostra que o invariante se mantém.
Passo 5
Término do laço: o laço para quando
. Nesse ponto, pelo invariante
, sabemos que para todo
com
, ou seja
, a chamada
foi feita exatamente uma vez. E não há índices
com
no vetor. Assim, todos e somente os elementos
foram visitados exatamente uma vez.
Resposta
O invariante de laço
é verdadeiro na inicialização, mantido em cada iteração e garante, na terminação, que cada
(
) foi visitado exatamente uma vez. Portanto, a afirmação está demonstrada.