927 -- Exemples de preuve d’algorithme : correction, terminaison. : Différence entre versions
De AgregmathKL
Yon (discuter | contributions) m (en-têtes) |
Yon (discuter | contributions) m (Mise en page enfin correcte) |
||
| Ligne 4 : | Ligne 4 : | ||
Petite intro (mentionner le problème de preuve de correction et terminaison | Petite intro (mentionner le problème de preuve de correction et terminaison | ||
| − | des boucles) | + | des boucles). |
=== Preuves informelles [Cormen] === | === Preuves informelles [Cormen] === | ||
| Ligne 10 : | Ligne 10 : | ||
==== Étude de la correction ==== | ==== Étude de la correction ==== | ||
| − | Invariant de boucle, exemple du tri insertion. Remarque que certains | + | # Invariant de boucle, exemple du tri insertion. Remarque que certains algorithmes incorrects sont intéressants (ex : Soloway-Strassen). |
| − | 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. | |
| − | # | + | |
| − | + | ||
| − | Problème indécidable. Ensembles bien fondés. Variant de boucle. | + | |
| − | + | ||
| − | # | + | |
| − | + | ||
| − | Écrire l'algo sur le plan. Ne prouver que la correction si trop long. | + | |
=== Preuves formelles [Winskel] === | === Preuves formelles [Winskel] === | ||
| − | # Langage IMP | + | # Langage IMP : Syntaxe, définitions. |
| − | + | #* Sémantique dénotationnelle : sémantique des commandes surtout, en particulier du while. | |
| − | Syntaxe, définitions | + | #* 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). | |
| − | #* Sémantique dénotationnelle | + | #* Correction des règles (DEV). |
| − | + | ||
| − | + | ||
| − | + | ||
| − | Remarque : a priori on pourrait faire la sémantique opérationnelle aussi. | + | |
| − | + | ||
| − | # | + | |
| − | + | ||
| − | + | ||
| − | factorielle (autre DEV possible a priori). | + | |
| − | + | ||
| − | Correction des règles (DEV). | + | |
| − | + | ||
#* Plus faibles préconditions | #* Plus faibles préconditions | ||
== Développements == | == Développements == | ||
| − | + | === Proposés === | |
* [[Correction de l'algo de Hopcroft]] | * [[Correction de l'algo de Hopcroft]] | ||
* [[Correction des règles de Hoare]] | * [[Correction des règles de Hoare]] | ||
| − | + | === Autres possibles === | |
* Correction du calcul de la factorielle avec les règles de Hoare | * Correction du calcul de la factorielle avec les règles de Hoare | ||
| Ligne 57 : | Ligne 38 : | ||
* Cormen et al. | * Cormen et al. | ||
* Carton | * Carton | ||
| + | * Winskel | ||
Version du 1 décembre 2013 à 11:25
Sommaire
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
