Na prova de correção, uma designação indicando que de um programa declarações de saída sigam logicamente de suas declarações de entrada e etapas de processamento, e que, além disso, o programa termina em todas as entrada condições especificadas.