L'invariant de boucle est

factorielle = i!

La démonstration :

1. L'invariant est vrai au début de la boucle car 0! = 1.

2. Supposons l'invariant de boucle vrai au début de la boucle et démontrons qu'il est encore vrai à la fin de la boucle.

Soit I la valeur de n à la fin de la boucle, soit FACT la valeur de factorielle à la fin de la boucle. On a :

FACT = FACT * (i + 1) = i! * (i + 1) = (i + 1) ! = I!.

Ce qui veut dire que l'invariant de boucle est bien vrai au début et à la fin de chaque boucle.

3. Après la boucle l'invariant est donc vrai et en plus on a i = n (condition de sortie de la boucle). Donc après la boucle on a factorielle = n!.

CQFD