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.