927 -- Exemples de preuve d’algorithme : correction, terminaison.

Plans

Plan scanné de l'année 2012-2013

Plan scanné de l'année 2013-2014

Plan scanné de l'année 2014-2015

Plan scanné de l'année 2015-2016

Plan scanné de l'année 2018-2019

Autre plan : Olivier et Yon (2013)

Plan

Petite intro (mentionner le problème de preuve de correction et terminaison des boucles).

Preuves informelles [Cormen]

Étude de la correction

1. Invariant de boucle, exemple du tri insertion. Remarque que certains algorithmes incorrects sont intéressants (ex : Soloway-Strassen).
2. Étude de la terminaison. Problème indécidable. Ensembles bien fondés. Variant de boucle.
3. Exemple complet : Algorithme de Hopcroft [Carton + preuve modifiée] (DEV). Écrire l'algo sur le plan. Ne prouver que la correction si trop long.

Preuves formelles [Winskel]

1. Langage IMP : Syntaxe, définitions.
   • Sémantique dénotationnelle : sémantique des commandes surtout, en particulier du while.
   • Remarque : a priori on pourrait faire la sémantique opérationnelle aussi.
2. Règles de Hoare : langage d'assertions, triplet de Hoare. Exemple pour le calcul de la factorielle (autre DEV possible a priori).
   • Correction des règles (DEV).
   • Plus faibles préconditions

Développements

• Algorithme d'unification

Autres possibles

• Correction de l'algo de Hopcroft
• Correction des règles de Hoare
• Correction du calcul de la factorielle avec les règles de Hoare

Références

• Cormen et al.
• Carton
• Winskel