Uma invariante de laço é uma propriedade do algoritmo iterativo, em relação às suas variáveis, que deve se manter verdadeira antes, durante e depois da execução do laço. Uma vez que a invariante de laço mantenha-se verdadeira, podemos afirmar que, em relação à propriedade escolhida, o algoritmo está correto.
Sobre a invariante de laço, devemos demonstrar seu estado da em três momentos, para demonstrar a correção do algoritmo:
A prova de correção de algoritmos por invariantes de laço são semelhantes à prova por indução.
Para entender melhor como funcionam as invariantes de laço, três exemplos serão analisados.
A busca linear, ou sequencial, é um algoritmo de busca exaustiva em listas. O algoritmo verifica cada elemento da lista até encontrar uma correspondência, ou até que não existam mais elementos na lista.
O pseudocódigo para a busca linear pode ser definido como:
linear_search(A, v):
for i in 1..A.length:
if A[i] == v:
return i
return nil
Nota: arrays possuem índices começando em 1.
O algoritmo possui um único laço, onde a iteração será executada para cada um dos elementos da lista.
A definição da invariante do laço para a busca linear é:
O valor v não está na lista
A[1..i-1].
i = 1 e A[1..i) é um conjunto vazio, logo, v não pertence ao conjunto, sendo a invariante verdadeira.A[i] == v, o laço termina, logo, a iteração só ocorre se v não pertence a A[i, i+1).A[i] == v, onde o elemento procurado é encontrado, ou se não existem mais elementos em A, sendo que a invariante v não pertence a A[1..i-1] se mantém verdadeira para ambos os casos.Como a invariante se mantém sempre verdadeira, o algoritmo está correto.
Apesar de simples, e de encontrar um elemento independente da organização dos dados, a busca linear é ineficiente, uma vez que pode ser necessário analisar todos os elementos da lista.
Caso os elementos de uma lista estejam organizadas em ordem crescente em relação a uma chave k, a busca por elementos nessa lista pode ser mais eficiente se utilizarmos uma busca binária.
Na busca binária em uma lista ordenada de elementos A[1..n], comparamos uma chave k com um elemento da lista A[i], onde 1 <= i <= n. Se k <= A[i], como a lista está ordenada, sabemos que k está no conjunto A[1..i], caso contrário, sabemos que k está no conjunto A[i+1..n].
O pseudocódigo para a busca binária iterativa pode ser definido da seguinte forma:
binary_search(A, k):
p = 1
q = A.length
while p != q:
m = p + (q - p) / 2
if k <= A[m]:
q = m
else:
p = m + 1
if k != A[q]:
return nil
return p
A invariante do laço pode ser definida como:
Se
kestá emA[1..n], entãokestá na listaA[p..q]que está contida emA[1..n].
p = 1 e q = n, logo, se k esta na lista A[1..n], está na lista A[p..q], sendo a invariante verdadeira.p <= m <= q, como a lista está ordenada, se k <= A[m], k está em A[p..m], logo, sendo q = m, então k está em A[p..q]. Caso contrário se k > A[m], logo, sendo p = m + 1, então k está em A[p..q], sendo verdadeira a invariante.p = q, sendo que se k == A[q] a chave foi encontrada, caso contrario, o elemento não existe na lista.Para que a busca binária possa ser utilizada é necessário que a lista de elementos esteja ordenada de acordo com uma chave. O problema da ordenação pode ser definido em função da sua entrada e saída esperada:
Entrada: lista de N elementos A = {a1, a2, …, an-1, an}
Saída: lista de N elementos A’, tal que A’ = {a’1 <= a’2 <= … <= a’n-1 <= a’n} e a’j pertence a A, para todo j pertencente a [1..n].
Podemos definir o pseudocódigo para o algoritmo Insertion Sort como:
insertion_sort(A):
for j in 2 to A.length:
k = A[j]
i = j - 1
while i > 0 and A[i] > k:
A[i + 1] = A[i]
i = i - 1
A[i + 1] = k
Nota: arrays possuem índices começando em 1.
O algoritmo é formado por dois laços. O laço externo irá iterar sobre todos os elementos da lista, a partir do segundo elemento, e o laço interno ira iterar sobre todos os elementos anteriores ao i-ésimo elemento.
Para verificar a correção do algoritmo insertion sort, definimos a invariante de laço como:
A cada iteração de laço
for, a subsequência A[1..j-1] consiste dos elementos originais em A[1..j-1], porém, ordenados.
E verificamos se a invariante é verdadeira:
for move elementos A[j-1], A[j-2], A[j-3] e assim por diante, uma posição à direita, até que encontre a posição adequada para o elemento A[j]. Nesse ponto, os elementos da subsequência A[1..j] consistem dos elementos originais A[1..j] ordenados. Incrementando o valor de j para a próxima iteração garante que a invariante de laço mantém-se verdadeira.for termine é que j seja maior que o número de elementos em A (n). Como incrementamos j de 1 em 1, o loop terminará com j = n + 1. Substituindo j na invariante do laço, temos que a subsequência A[1..n+1-1], ou seja A[1..n], consiste dos elementos originais de A e está ordenada. Como a sequência A[1..n] é a sequência completa concluímos que todos os elementos foram ordenados.Para uma prova de todo o algoritmo, devemos demostrar que o laço interno, o while, está correto:
Invariante do laço: os elementos A[i..j] são maiores ou iguais a k.
Podemos utilizar invariantes de laço para demonstrar se um algoritmo iterativo está correto ou não. Para isso definimos a invariante de laço e demonstramos que é verdadeira na inicialização, manutenção e finalização do laço. Se a propriedade avaliada pela invariante de laço for verdadeira nas três situações, dizemos que o programa está correto segundo a propriedade escolhida.