Partir da pós-condição, inverter instruções por leitura textual, aceitar preservação empírica em casos de teste e encerrar o laço quando a guarda permanecer verdadeira.

Escolher um invariante que vale antes do laço, mostrar preservação a cada iteração, definir uma função variante decrescente em ℕ e concluir a pós-condição a partir de invariante verdadeiro e guarda falsa.

Derivar o invariante de exemplos executados, assumir que decrementos eventuais bastam para terminar e concluir a prova substituindo a guarda pela pós-condição ao final.

Fixar o invariante igual à pós-condição, provar que ele se torna verdadeiro no meio do laço e finalizar quando o invariante coincidir com a guarda ainda verdadeira.