Hola chicos como va? Queria saber como poder encontrar una invariante para este bucle . Lo encontre pero no se si esta bien:
FXY ( x integer)
j=4
i=1
while (i<>x) do
j=j+2*i+3
i= i+1
return (j*x)
Encontre que la invariante es Q: j*x= x(x+1)^2 aunque no se si es la correcta !
