O Corretei de Algoritmos

COR R E T U D E D E

A LGOR I T M OS

Indica que ele termina sua execução, retornando saídas corretas para todas

as instancias do problema. Um dos métodos mais utilizados é a invariante de

laço.

INVARIANTE DE LAÇO

É um método de corretude de algoritmos iterativos, que consiste em provar a

corretude de um algoritmo através de invariantes: Mostrar que que o invariante é

valido antes do laço, durante o laço e após o laço. Isso pode ser feito checando as

iterações uma a uma, porém caso haja um grande quantidade de iterações torna-se

inviável fazer desta forma, por isso a melhor estratégia é usar o método da indução.

INDUÇÃO

Prova-se que o enunciado é verdadeiro para um valor inicial e depois

prova-se que o processo para ir de um valor para o outro também é

valido, e se ambos são provados, então qualquer valor pose ser obtido

através da repetição do processo.

EXEMPLO

INSERTION-SORT(A)

for j ← 2 to length[A]

do key ← A[j]

// Insert A[j] into the sorted sequence A[1..j-1].

i ← j - 1

while i > 0 and A[i] > key

do A[i + 1] ← A[i]

i ← i - 1

A[i + 1] ← key

Invariante do laço neste caso: Subarranjo[1 to j-1] sempre está

ordenado.

Agora iremos checar e provar que o algoritmo está correto.

Inicialização: Antes da primeira iteração j=2. Então subarranjo [1:1] é o

array a ser testado. Por ter apenas um elemento está ordenado. Então a

invariante está satisfeita.

Manutenção: Mostrar que o invariante j continuará valendo para j+1.

Se o invariante vale na iteração j, A[1..j-1] ppossui os elementos originais

de A[1..j-1] ordenados. O codigo do for A[j-1], A[j-2]... até encontrar a

posição adequada. Incrementando j após processo o que nos devolve

A[1..j-1] ordenado.

Término: O subarranjo consiste nos seus elementos originais, porém

ordenados.

...