927 -- Exemples de preuve d’algorithme : correction, terminaison. : Différence entre versions
De AgregmathKL
Yon (discuter | contributions) m (en-têtes) |
|||
(8 révisions intermédiaires par 4 utilisateurs non affichées) | |||
Ligne 1 : | Ligne 1 : | ||
− | = | + | = Plans = |
− | == Plan | + | [[Fichier:Pdf.png|alt=Pdf|link=Média:927_2012-2013.pdf|24px]] [[Média:927_2012-2013.pdf|Plan scanné de l'année 2012-2013]] |
− | + | [[Fichier:Pdf.png|alt=Pdf|link=Média:927_2013-2014.pdf|24px]] [[Média:927_2013-2014.pdf|Plan scanné de l'année 2013-2014]] | |
− | + | ||
− | == | + | [[Fichier:Pdf.png|alt=Pdf|link=Média:927_2014-2015.pdf|24px]] [[Média:927_2014-2015.pdf|Plan scanné de l'année 2014-2015]] |
− | == | + | [[Fichier:Pdf.png|alt=Pdf|link=Média:927_2015-2016.pdf|24px]] [[Média:927_2015-2016.pdf|Plan scanné de l'année 2015-2016]] |
− | + | [[Fichier:Pdf.png|alt=Pdf|link=Média:927_2018-2019.pdf|24px]] [[Média:927_2018-2019.pdf|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 | + | === 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 | #* Plus faibles préconditions | ||
− | |||
− | |||
− | |||
+ | = Développements = | ||
+ | <DynamicPageList> | ||
+ | category = Développement de la leçon 927 | ||
+ | </DynamicPageList> | ||
+ | == Autres possibles == | ||
* [[Correction de l'algo de Hopcroft]] | * [[Correction de l'algo de Hopcroft]] | ||
* [[Correction des règles de Hoare]] | * [[Correction des règles de Hoare]] | ||
+ | * Correction du calcul de la factorielle avec les règles de Hoare | ||
− | |||
− | + | = Références = | |
− | + | ||
− | + | ||
* Cormen et al. | * Cormen et al. | ||
* Carton | * Carton | ||
+ | * Winskel | ||
+ | |||
+ | |||
+ | [[Category:Leçon d'informatique]] | ||
+ | [[Category:Anciennes leçons]] |
Version actuelle en date du 22 avril 2022 à 10:26
Sommaire
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
- 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
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