927 -- Exemples de preuve d’algorithme : correction, terminaison. : Différence entre versions
De AgregmathKL
Ligne 4 : | Ligne 4 : | ||
*2013-2014 [[Fichier:Pdf.png|alt=Pdf|link=|24px]] [[Média:927_2013-2014.pdf|927 Exemples de preuve d’algorithme : correction, terminaison.]] | *2013-2014 [[Fichier:Pdf.png|alt=Pdf|link=|24px]] [[Média:927_2013-2014.pdf|927 Exemples de preuve d’algorithme : correction, terminaison.]] | ||
*2014-2015 [[Fichier:Pdf.png|alt=Pdf|link=|24px]] [[Média:927_2014-2015.pdf|927 Exemples de preuve d’algorithme : correction, terminaison.]] | *2014-2015 [[Fichier:Pdf.png|alt=Pdf|link=|24px]] [[Média:927_2014-2015.pdf|927 Exemples de preuve d’algorithme : correction, terminaison.]] | ||
+ | *2015-2016 [[Fichier:Pdf.png|alt=Pdf|link=|24px]] [[Média:927_2015-2016.pdf|927 Exemples de preuve d’algorithme : correction, terminaison.]] | ||
Version du 24 août 2016 à 17:08
Sommaire
Plans scannés
- 2012-2013 927 Exemples de preuve d’algorithme : correction, terminaison.
- 2013-2014 927 Exemples de preuve d’algorithme : correction, terminaison.
- 2014-2015 927 Exemples de preuve d’algorithme : correction, terminaison.
- 2015-2016 927 Exemples de preuve d’algorithme : correction, terminaison.
Développements
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
- Invariant de boucle, exemple du tri insertion. Remarque que certains algorithmes incorrects sont intéressants (ex : Soloway-Strassen).
- Étude de la terminaison. Problème indécidable. Ensembles bien fondés. Variant de boucle.
- 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]
- 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.
- 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
Proposés
Autres possibles
- Correction du calcul de la factorielle avec les règles de Hoare
Références
- Cormen et al.
- Carton
- Winskel