927 -- Exemples de preuve d’algorithme : correction, terminaison. : Différence entre versions

De AgregmathKL
Aller à : navigation, rechercher
m (numérotation)
 
(9 révisions intermédiaires par 4 utilisateurs non affichées)
Ligne 1 : Ligne 1 :
−
= Plan Olivier et Yon (2013) =
+
= 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]]
  
−
Petite intro (mentionner le problème de preuve de correction et terminaison
+
[[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]]
−
des boucles)
+
  
−
=== Preuves informelles [Cormen] ===
+
[[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]]
  
−
# Étude de la correction
+
[[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]]
  
−
Invariant de boucle, exemple du tri insertion. Remarque que certains
+
[[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]]
−
algorithmes incorrects sont intéressants (ex : Soloway-Strassen).
+
  
−
#* Étude de la terminaison
 
  
−
Problème indécidable. Ensembles bien fondés. Variant de boucle.
+
= Autre plan : Olivier et Yon (2013) =
  
−
#* Exemple complet : Algorithme de Hopcroft [Carton + preuve modifiée] (DEV)
+
== Plan ==
  
−
Écrire l'algo sur le plan. Ne prouver que la correction si trop long.
+
Petite intro (mentionner le problème de preuve de correction et terminaison
 +
des boucles).
  
−
=== Preuves formelles [Winskel] ===
+
=== Preuves informelles [Cormen] ===
  
−
# Langage IMP
+
==== Étude de la correction ====
  
−
Syntaxe, définitions
+
# 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.
  
−
#* Sémantique dénotationnelle
+
=== Preuves formelles [Winskel] ===
−
 
+
−
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).
+
  
 +
# 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 ==
 
−
 
−
# Proposés
 
  
 +
= 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
  
−
# Autres possibles
 
  
−
* Correction du calcul de la factorielle avec les règles de Hoare
+
= Références =
−
 
+
−
== 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

Plans

Pdf Plan scanné de l'année 2012-2013

Pdf Plan scanné de l'année 2013-2014

Pdf Plan scanné de l'année 2014-2015

Pdf Plan scanné de l'année 2015-2016

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 informelles [Cormen]

Étude de la correction

  1. Invariant de boucle, exemple du tri insertion. Remarque que certains algorithmes incorrects sont intéressants (ex : Soloway-Strassen).
  2. Étude de la terminaison. Problème indécidable. Ensembles bien fondés. Variant de boucle.
  3. 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.
    • 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.
  2. 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


Références

  • Cormen et al.
  • Carton
  • Winskel
Récupérée de « https://minerve.ens-rennes.fr/index.php?title=927_--_Exemples_de_preuve_d’algorithme_:_correction,_terminaison.&oldid=4926 »