Mostre que a sentença
é um invariante do laço no segmento em pseudocódigo a seguir.
Condições prévias:
\(i \leftarrow 1\)
\(m \leftarrow x_{1}\)
enquanto \(i<n\) fazer
    \(\ulcorner i \leftarrow i+1\)
        se \(x_{i}>m\) então
    ᄂ \(\quad m \leftarrow x_{i}\)

Passo 1

O enunciado nos dá o seguinte trecho de código, que percorre o vetor x1,x2,dots,xn procurando o maior elemento:
i 1
m x1
enquanto i < n fazer
i i + 1
se xi > m então
m xi
fim se
fim enquanto
Queremos mostrar que a sentença
m >= x para todo xinx1,x2,dots,xi
é um invariante de laço. Para isso usamos a definição de invariante:
1. provar que a propriedade vale antes de entrar no laço (inicialização),
2. provar que, se vale antes de uma iteração, então vale também ao final da iteração (preservação).

Passo 2

(Inicialização)
Antes de executar o laço temos
i = 1 e m = x1
O conjunto x1,dots,xi nessa situação é x1. Como m = x1, certamente
m >= x1,
portanto
m >= x para todo xinx1
Logo a propriedade vale antes da primeira iteração.

Passo 3

(Preservação)
Suponha que, ao entrar em uma iteração qualquer do laço com valor atual de i, valha
m >= xk para todo k=1,2,dots,i
Como i<n, executamos primeiro
i i + 1,
e chamemos de i' o novo valor de i (ou seja, i'=i+1). Em seguida testamos
se xi'>m então m xi' ã
Queremos mostrar que, após esses comandos, ainda vale
m >= xk para todo k=1,2,dots,i'
Existem dois casos:
Caso 1: xi'>mantigo.
Nesse caso a nova variável m é atualizada para xi'. Para todo k < i', pela hipótese de indução mantigo>= xk, e como xi'>mantigo segue
mnovo = xi' ;>=; xk
Além disso mnovo=xi'>= xi'. Logo vale para todo k<= i'.
Caso 2: xi'<= mantigo.
Aqui m não se altera, fica mnovo=mantigo. Para k<i' vale mantigo>= xk pela hipótese de indução; e para k=i' vale mantigo>= xi' porque xi'<= mantigo. Logo novamente
mnovo>= xk para todo k=1,dots,i'
Em ambos os casos preservamos a propriedade
m >= x para todo xinx1,dots,xi'

Passo 4

Concluímos que a sentença
m >= x para todo xinx1,x2,dots,xi
é de fato um invariante de laço, pois vale antes da primeira iteração e é preservada em cada passo do laço.

Resposta

A sentença
m >= x para todo xinx1,x2,dots,xi
é invariante do laço.

Exercícios de Livros Relacionados