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

Plan Olivier et Yon (2013)

Plan

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

Preuves informelles [Cormen]

1. Étude de la correction

Invariant de boucle, exemple du tri insertion. Remarque que certains algorithmes incorrects sont intéressants (ex : Soloway-Strassen).

1. Étude de la terminaison

Problème indécidable. Ensembles bien fondés. Variant de boucle.

1. 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

1. 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.

1. 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).

1. Plus faibles préconditions

Développements

1. Proposés

• Correction de l'algo de Hopcroft
• Correction des règles de Hoare

1. Autres possibles

• Correction du calcul de la factorielle avec les règles de Hoare

Références

• Cormen et al.
• Carton