927 -- Exemples de preuve d’algorithme : correction, terminaison. : Différence entre versions
De AgregmathKL
Yon (discuter | contributions) (leçon 927) |
Yon (discuter | contributions) m (numérotation) |
||
| Ligne 13 : | Ligne 13 : | ||
algorithmes incorrects sont intéressants (ex : Soloway-Strassen). | algorithmes incorrects sont intéressants (ex : Soloway-Strassen). | ||
| − | # Étude de la terminaison | + | #* Étude de la terminaison |
Problème indécidable. Ensembles bien fondés. Variant de boucle. | Problème indécidable. Ensembles bien fondés. Variant de boucle. | ||
| − | # Exemple complet : Algorithme de Hopcroft [Carton + preuve modifiée] (DEV) | + | #* Exemple complet : Algorithme de Hopcroft [Carton + preuve modifiée] (DEV) |
Écrire l'algo sur le plan. Ne prouver que la correction si trop long. | Écrire l'algo sur le plan. Ne prouver que la correction si trop long. | ||
| Ligne 27 : | Ligne 27 : | ||
Syntaxe, définitions | Syntaxe, définitions | ||
| − | # Sémantique dénotationnelle | + | #* Sémantique dénotationnelle |
Sémantique des commandes surtout, en particulier du while. | Sémantique des commandes surtout, en particulier du while. | ||
| Ligne 33 : | Ligne 33 : | ||
Remarque : a priori on pourrait faire la sémantique opérationnelle aussi. | Remarque : a priori on pourrait faire la sémantique opérationnelle aussi. | ||
| − | # Règles de Hoare | + | #* Règles de Hoare |
Langage d'assertions, triplet de Hoare. Exemple pour le calcul de la | Langage d'assertions, triplet de Hoare. Exemple pour le calcul de la | ||
| Ligne 40 : | Ligne 40 : | ||
Correction des règles (DEV). | Correction des règles (DEV). | ||
| − | # Plus faibles préconditions | + | #* Plus faibles préconditions |
== Développements == | == Développements == | ||
Version du 1 décembre 2013 à 11:19
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
