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 2024 :

  • Pas de recasages pour cette année.

Versions :

Références utilisées dans les versions de ce développement :

The formal semantics of programming langages , Winskel (utilisée dans 3 versions au total)