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}\)
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
procurando o maior elemento:
enquanto
se
fim se
fim enquanto
Queremos mostrar que a sentença
é um invariante de laço. Para isso usamos a definição de invariante:
. provar que a propriedade vale antes de entrar no laço (inicialização),
. 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
Antes de executar o laço temos
O conjunto
nessa situação é
. Como
, certamente
portanto
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 , valha
Suponha que, ao entrar em uma iteração qualquer do laço com valor atual de
Como
, executamos primeiro
e chamemos de
o novo valor de
(ou seja,
). Em seguida testamos
Queremos mostrar que, após esses comandos, ainda vale
Existem dois casos:
Caso
:
.
Nesse caso a nova variável é atualizada para
. Para todo
, pela hipótese de indução
, e como
segue
Nesse caso a nova variável
Além disso
. Logo vale para todo
.
Caso
:
.
Aqui não se altera, fica
. Para
vale
pela hipótese de indução; e para
vale
porque
. Logo novamente
Aqui
Em ambos os casos preservamos a propriedade
Passo 4
Concluímos que a sentença
é 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
é invariante do laço.