Développement : Preuve de la factorielle en logique de Hoare

Détails/Enoncé :

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.

Recasages pour l'année 2019 :

Versions :