Développement #217

Titre : Preuve de la factorielle en logique de Hoare

Contenu : 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.

Créé le : 23/07/2026 12:42

Mis à jour : 23/07/2026 12:42