Jump to content
edub13

Loop Invariant ?

Recommended Posts

edub13

Boas já estive a ler uma data de coisas, mas ainda não consegui perceber o que um Loop Invariant, à alguma maneira simples de me explicarem com código?

Cumps


Learning:

C++

Share this post


Link to post
Share on other sites
thoga31

Nota prévia: eu já estudei este conceito há uma temporada, pelo que se cometer alguma imprecisão na minha explicação, não hesitem em me corrigir ;)

Os exemplos serão dados em C.

Loop invariant é um conceito interessante que ajuda formalmente a perceber se um loop está correctamente construído ou não. Essencialmente diz-nos que uma determinada coisa é verdadeira quer antes quer após um loop. Uma coisa pode ser uma variável, uma condição ou o nosso objectivo. Genericamente, dizemos que é uma propriedade do loop que se cumpre antes e após este. Vamos esclarecer isto com um pedaço de código clássico que todos gostam de apresentar:

// Seja "n" um número inteiro positivo não nulo
int a[n] = { /* colocar valores aqui */ };

/* Vamos procurar o maior valor, "max".
  "max" será um valor que está entre a[0] e a[n-1]
  Este é o nosso objectivo, e terá de ser verdadeiro antes e depois do loop.
  Para isso, também temos de garantir que "i" seja menor ou igual a "n-1" e nunca superior. */

int i = 0;
int max = a[ i ];
// "max" é o maior entre a[0] e a[ i ]? Sim. É verdade ANTES do loop.

while (++i <= n-1) {
  if (a[ i ] > max)
     max = a[ i ];
     // "max" só muda se o actual valor de "a" for maior que o actual de "max"
}

// "max" é o maior valor entre a[0] e a[ i ]? Sim, é verdade DEPOIS do loop.
// "i" é menor ou igual do que "n-1"? Sim, neste momento i == n-1. Mantém-se verdadeiro.

Este é o exemplo da praxe, e acredito que não seja o mais fácil de entender.

Portanto, vamos a um exemplo possivelmente mais simples:

int i=0, n=10;

// "i" é menor ou igual que "n"? Sim.
while (++i <= n)
  printf("%d ", i);

// "i" é menor ou igual que "n"? Sim.

Neste caso, estamos perante um loop invariant. Se fizeres o teste, vais obter o outpit 1 2 3 4 5 6 7 8 9 10. Mas agora ou vou mudar uma coisa:

int i=0, n=10;

// "i" é menor ou igual que "n"? Sim.
while (i++ <= n)    // <--- !!! ALTERAÇÃO !!!
  printf("%d ", i);

// "i" é menor ou igual que "n"? !!! NÃO !!!

Agora este não é um loop invariant: a condição não se cumpre depois do loop! Repara no output: 1 2 3 4 5 6 7 8 9 10 11.

A questão que se coloca é: então e durante o loop? Já vi debates interessantes acerca do assunto, e a meu ver a resposta é não. Estamos perante invariância e não constantes. Claro que não é saudável brincar com o fogo dentro de loops e há que ter cuidado com o que fazemos lá dentro, mas este exemplo mostra outro loop invariant:

int number = 1 + rand() % 20;  // número aleatório entre 1 e 20
int temp = number; // guardámos em "temp" o valor pseudoaleatório

// "number" é igual a "temp"? Sim.
do {
  scanf("%d", &number);
} while (number != temp);
// "number" é igual a "temp"? Sim.

Este último exemplo não seria assim implementado na prática, claro, mas serve para mostrar o que é um loop invariant.

Todavia, há linguagens que permitem definir a invariância de um loop (linguagem Eiffel) ou simular essa invariância (linguagem Java). Em C podemos simular isto de forma rudimentar ao não mexer no iterador dentro do ciclo:

for (int i = 0; i <= 10; ++i) {
  // NÃO mexer no valor de "i"!
};

Em alguns dialectos do Pascal, nomeadamente o Free Pascal, o ciclo for é obrigatoriamente invariante! O seguinte código dá erro na compilação:

program prog;
var i : integer;
begin
  for i:=1 to 10 do begin
     write(i:2);
     inc(i);  // incrementa em 1 o valor de "i".
  end;
end.

O erro é o seguinte: prog.pas(6,6) Error: Illegal assignment to for-loop variable "i".

Isto acontece porque, em Pascal, é obrigatório no ciclo for o intervalo do iterador tem de começar em inicio e acabar em fim, no matter what:

for iterador := inicio to/downto fim do

A prova em como é invariante:

program ideone;
var i : integer;
begin
  for i:=1 to 10 do
     write(i:3);
  write('| i=':5, i);
end.

E o output: 1 2 3 4 5 6 7 8 9 10 | i=10

Portanto, o ciclo for cumpre que antes do início do ciclo iterador está entre inicio e fim, e que no final também, e dentro do ciclo também! Quando sais do ciclo, iterador tem obrigatoriamente o valor de final, nem mais nem menos. Se colocarmos um break pelo meio, também vai estar entre inicio e fim.

Em Eiffel, segundo a pesquisa que fiz agora (não me lembrava de nenhuma linguagem que definisse explicitamente a invariância), podes definir esta invariância explicitamente:

from
   i := 0
invariant
   i <= 10
until
   i >= 10
loop
   i := i + 1
end

Uma extensão deste conceito são as classes invariantes, em que as propriedades, por exemplo, terão sempre um valor bem definido dentro de certos limites. Por exemplo, em D, podes definir numa classe que a propriedade XPTO tem de estar compreendida entre -10 e 90.

Espero que o conceito esteja esclarecido.

Cumprimentos.


Knowledge is free!

Share this post


Link to post
Share on other sites
thoga31

Nota: faltou-me, no meio disto, diferenciar dois conceitos:

  • Invariância - refere-se a uma propriedade.
  • Imutabilidade - refere-se a um valor.

É por isso que num loop invariant pode haver, e costuma haver, mutabilidade do iterador ou variável de controlo. O que torna um loop num loop invariant é uma propriedade que se confirma antes e após o loop.


Knowledge is free!

Share this post


Link to post
Share on other sites
Rui Carlos

O invariante é muitas vezes usado para mostrar que um ciclo tem o comportamento desejado.

Por exemplo, no caso indicado pelo thoga31,

int i = 0;
int max = a[ i ];

int i=1;
while (i != n) {
  if (a[ i ] > max)
     max = a[ i ];
  i++;
}

Se provarmos que o invariante max = maximo({a0, ..., ai}) é efectivamente válido (provamos que é válido antes do ciclo, e depois provamos que válido depois de uma iteração, assumindo que é válido no início), como temos por condição de paragem i != n, no final do ciclo temos i == n && max = maximo({a0, ..., ai}), donde facilmente se conclui que max = maximo({a0, ..., an}).

(Estas provas costumam envolver ainda mais um passo, que é provar que o ciclo termina.)

Share this post


Link to post
Share on other sites

Create an account or sign in to comment

You need to be a member in order to leave a comment

Create an account

Sign up for a new account in our community. It's easy!

Register a new account

Sign in

Already have an account? Sign in here.

Sign In Now

×
×
  • Create New...

Important Information

By using this site you accept our Terms of Use and Privacy Policy. We have placed cookies on your device to help make this website better. You can adjust your cookie settings, otherwise we'll assume you're okay to continue.