Hallar el invariante no es difícil macho.
Solo tienes que poner 3 cosas intersecadas por un ^
1) Una "regla general" que construyes tú a partir de una traza que hagas del bucle, que ha de ser parecida a la postcondición del propio bucle.
2) Los elementos de la precondición del bucle que no varían.
3) Una expresión de "lo que hace falta para salir del bucle", expresado de la misma forma que la condición del propio bucle.
Por ejemplo, si es un bucle mientras i
<n, el 3º punto del invariante será i
<n+1. ¿Por qué? El bucle se repite mientras i sea menor o igual a n. Con tal de que sea inmediatamente mayor (por una unidad, por ejemplo), ya sales de él.
Pues así funciona la cosa.