https://minerve.ens-rennes.fr/api.php?action=feedcontributions&feedformat=atom&user=Yon 2026-05-07T02:03:48Z Contributions de l’utilisateur MediaWiki 1.24.0 https://minerve.ens-rennes.fr/index.php?title=Correction_des_r%C3%A8gles_de_Hoare&diff=1302 2013-12-01T09:39:40Z

<p>Yon : ajout fichier .tex</p> <hr /> <div>[[Média: Hoare.pdf | Correction des règles de Hoare ]]<br /> <br /> [[Média: Hoare.tex | Correction des règles de Hoare (fichier .tex) ]]</div>

Yon https://minerve.ens-rennes.fr/index.php?title=Fichier:Hopcroft.tex&diff=1300 2013-12-01T09:38:56Z

<p>Yon : </p> <hr /> <div></div>

Yon https://minerve.ens-rennes.fr/index.php?title=Fichier:Hoare.tex&diff=1299 2013-12-01T09:37:35Z

<p>Yon : </p> <hr /> <div></div>

Yon https://minerve.ens-rennes.fr/index.php?title=Correction_des_r%C3%A8gles_de_Hoare&diff=1298 2013-12-01T09:31:45Z

<p>Yon : Hoare (pdf)</p> <hr /> <div>[[Média: Hoare.pdf | Correction des règles de Hoare ]]</div>

Yon https://minerve.ens-rennes.fr/index.php?title=Fichier:Hoare.pdf&diff=1297 2013-12-01T09:31:33Z

<p>Yon : </p> <hr /> <div></div>

Yon https://minerve.ens-rennes.fr/index.php?title=Fichier:Hopcroft.pdf&diff=1295 2013-12-01T09:29:38Z

<p>Yon : </p> <hr /> <div></div>

Yon https://minerve.ens-rennes.fr/index.php?title=927_--_Exemples_de_preuve_d%E2%80%99algorithme_:_correction,_terminaison.&diff=1294 2013-12-01T09:25:40Z

<p>Yon : Mise en page enfin correcte</p> <hr /> <div>= Plan Olivier et Yon (2013) =<br /> <br /> == Plan ==<br /> <br /> Petite intro (mentionner le problème de preuve de correction et terminaison<br /> des boucles).<br /> <br /> === Preuves informelles [Cormen] ===<br /> <br /> ==== Étude de la correction ====<br /> <br /> # Invariant de boucle, exemple du tri insertion. Remarque que certains algorithmes incorrects sont intéressants (ex : Soloway-Strassen).<br /> # Étude de la terminaison. Problème indécidable. Ensembles bien fondés. Variant de boucle.<br /> # Exemple complet : Algorithme de Hopcroft [Carton + preuve modifiée] (DEV). Écrire l'algo sur le plan. Ne prouver que la correction si trop long.<br /> <br /> === Preuves formelles [Winskel] ===<br /> <br /> # Langage IMP : Syntaxe, définitions.<br /> #* Sémantique dénotationnelle : sémantique des commandes surtout, en particulier du while.<br /> #* Remarque : a priori on pourrait faire la sémantique opérationnelle aussi.<br /> # Règles de Hoare : langage d'assertions, triplet de Hoare. Exemple pour le calcul de la factorielle (autre DEV possible a priori).<br /> #* Correction des règles (DEV).<br /> #* Plus faibles préconditions<br /> <br /> == Développements ==<br /> <br /> === Proposés ===<br /> <br /> * [[Correction de l'algo de Hopcroft]]<br /> * [[Correction des règles de Hoare]]<br /> <br /> === Autres possibles ===<br /> <br /> * Correction du calcul de la factorielle avec les règles de Hoare<br /> <br /> == Références ==<br /> <br /> * Cormen et al.<br /> * Carton<br /> * Winskel</div>

Yon https://minerve.ens-rennes.fr/index.php?title=927_--_Exemples_de_preuve_d%E2%80%99algorithme_:_correction,_terminaison.&diff=1293 2013-12-01T09:20:19Z

<p>Yon : en-têtes</p> <hr /> <div>= Plan Olivier et Yon (2013) =<br /> <br /> == Plan ==<br /> <br /> Petite intro (mentionner le problème de preuve de correction et terminaison<br /> des boucles)<br /> <br /> === Preuves informelles [Cormen] ===<br /> <br /> ==== Étude de la correction ====<br /> <br /> Invariant de boucle, exemple du tri insertion. Remarque que certains<br /> algorithmes incorrects sont intéressants (ex : Soloway-Strassen).<br /> <br /> #* Étude de la terminaison<br /> <br /> Problème indécidable. Ensembles bien fondés. Variant de boucle.<br /> <br /> #* Exemple complet : Algorithme de Hopcroft [Carton + preuve modifiée] (DEV)<br /> <br /> Écrire l'algo sur le plan. Ne prouver que la correction si trop long.<br /> <br /> === Preuves formelles [Winskel] ===<br /> <br /> # Langage IMP<br /> <br /> Syntaxe, définitions<br /> <br /> #* Sémantique dénotationnelle<br /> <br /> Sémantique des commandes surtout, en particulier du while.<br /> <br /> Remarque : a priori on pourrait faire la sémantique opérationnelle aussi.<br /> <br /> #* Règles de Hoare<br /> <br /> Langage d'assertions, triplet de Hoare. Exemple pour le calcul de la<br /> factorielle (autre DEV possible a priori).<br /> <br /> Correction des règles (DEV).<br /> <br /> #* Plus faibles préconditions<br /> <br /> == Développements ==<br /> <br /> # Proposés<br /> <br /> * [[Correction de l'algo de Hopcroft]]<br /> * [[Correction des règles de Hoare]]<br /> <br /> # Autres possibles<br /> <br /> * Correction du calcul de la factorielle avec les règles de Hoare<br /> <br /> == Références ==<br /> <br /> * Cormen et al.<br /> * Carton</div>

Yon https://minerve.ens-rennes.fr/index.php?title=927_--_Exemples_de_preuve_d%E2%80%99algorithme_:_correction,_terminaison.&diff=1292 2013-12-01T09:19:09Z

<p>Yon : numérotation</p> <hr /> <div>= Plan Olivier et Yon (2013) =<br /> <br /> == Plan ==<br /> <br /> Petite intro (mentionner le problème de preuve de correction et terminaison<br /> des boucles)<br /> <br /> === Preuves informelles [Cormen] ===<br /> <br /> # Étude de la correction<br /> <br /> Invariant de boucle, exemple du tri insertion. Remarque que certains<br /> algorithmes incorrects sont intéressants (ex : Soloway-Strassen).<br /> <br /> #* Étude de la terminaison<br /> <br /> Problème indécidable. Ensembles bien fondés. Variant de boucle.<br /> <br /> #* Exemple complet : Algorithme de Hopcroft [Carton + preuve modifiée] (DEV)<br /> <br /> Écrire l'algo sur le plan. Ne prouver que la correction si trop long.<br /> <br /> === Preuves formelles [Winskel] ===<br /> <br /> # Langage IMP<br /> <br /> Syntaxe, définitions<br /> <br /> #* Sémantique dénotationnelle<br /> <br /> Sémantique des commandes surtout, en particulier du while.<br /> <br /> Remarque : a priori on pourrait faire la sémantique opérationnelle aussi.<br /> <br /> #* Règles de Hoare<br /> <br /> Langage d'assertions, triplet de Hoare. Exemple pour le calcul de la<br /> factorielle (autre DEV possible a priori).<br /> <br /> Correction des règles (DEV).<br /> <br /> #* Plus faibles préconditions<br /> <br /> == Développements ==<br /> <br /> # Proposés<br /> <br /> * [[Correction de l'algo de Hopcroft]]<br /> * [[Correction des règles de Hoare]]<br /> <br /> # Autres possibles<br /> <br /> * Correction du calcul de la factorielle avec les règles de Hoare<br /> <br /> == Références ==<br /> <br /> * Cormen et al.<br /> * Carton</div>

Yon https://minerve.ens-rennes.fr/index.php?title=927_--_Exemples_de_preuve_d%E2%80%99algorithme_:_correction,_terminaison.&diff=1291 2013-12-01T09:17:35Z

<p>Yon : leçon 927</p> <hr /> <div>= Plan Olivier et Yon (2013) =<br /> <br /> == Plan ==<br /> <br /> Petite intro (mentionner le problème de preuve de correction et terminaison<br /> des boucles)<br /> <br /> === Preuves informelles [Cormen] ===<br /> <br /> # Étude de la correction<br /> <br /> Invariant de boucle, exemple du tri insertion. Remarque que certains<br /> algorithmes incorrects sont intéressants (ex : Soloway-Strassen).<br /> <br /> # Étude de la terminaison<br /> <br /> Problème indécidable. Ensembles bien fondés. Variant de boucle.<br /> <br /> # Exemple complet : Algorithme de Hopcroft [Carton + preuve modifiée] (DEV)<br /> <br /> Écrire l'algo sur le plan. Ne prouver que la correction si trop long.<br /> <br /> === Preuves formelles [Winskel] ===<br /> <br /> # Langage IMP<br /> <br /> Syntaxe, définitions<br /> <br /> # Sémantique dénotationnelle<br /> <br /> Sémantique des commandes surtout, en particulier du while.<br /> <br /> Remarque : a priori on pourrait faire la sémantique opérationnelle aussi.<br /> <br /> # Règles de Hoare<br /> <br /> Langage d'assertions, triplet de Hoare. Exemple pour le calcul de la<br /> factorielle (autre DEV possible a priori).<br /> <br /> Correction des règles (DEV).<br /> <br /> # Plus faibles préconditions<br /> <br /> == Développements ==<br /> <br /> # Proposés<br /> <br /> * [[Correction de l'algo de Hopcroft]]<br /> * [[Correction des règles de Hoare]]<br /> <br /> # Autres possibles<br /> <br /> * Correction du calcul de la factorielle avec les règles de Hoare<br /> <br /> == Références ==<br /> <br /> * Cormen et al.<br /> * Carton</div>

Yon