Loop Invariant

Em ciência da computação, uma condição que é verdadeira antes e depois de cada iteração de um laço (loop). É uma ferramenta importante para provar a correção de algoritmos.