Corretude aplicada no Insertion Sort

Ordenados: 1..j-1
Desordenados: j..n

Como decorrer do algoritmo os ordenados ganham (+1), logo fica {1..j} e os desordenados perdem (-1), ficando {j+1..n};
Invariante de Laço ou Loop de Invariante: Utilizamos as invariantes de laço para entender se o algoritmo está correto.
Definição: um invariante de um laço é uma propriedade que relaciona as variaveis do algoritmo a cada execução completa do laço.
Ele deve ser escolhido de modo que, ao termino do laço tenha-se uma propriedade útil para mostrar a corretude do algoritmo.
A prova de corretude de um algoritmo requer que sejam encontrados e provados invariantes dos vários laços que o compõem.
Em geral, é mais difícil descobrir um invariante apropriado do que mostrar sua validade se ele for dado de bandeja.

for j <- 2 to comprimento [A]
 do key <- A[j]
 //Inserir A[j] na sequência ordenada 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