Preuve de la factorielle en logique de Hoare

On illustre l'utilisation des règles de Hoare en prouvant l'algorithme calculant la factorielle. Ce développement peut être aussi l'occasion également de parler des difficultés principales pour l'automatisation des preuves utilisant ce système.