Leçon 927 : Exemples de preuve d’algorithme : correction, terminaisons.

(2018) 927

Dernier rapport du Jury :

(2017 : 927 - Exemples de preuve d'algorithme : correction, terminaison.) Le jury attend du candidat qu’il traite des exemples d’algorithmes récursifs et des exemples d’algorithmes itératifs. En particulier, le candidat doit présenter des exemples mettant en évidence l’intérêt de la notion d’invariant pour la correction partielle et celle de variant pour la terminaison des segments itératifs. Une formalisation comme la logique de Hoare pourra utilement être introduite dans cette leçon, à condition toutefois que le candidat en maîtrise le langage. Des exemples non triviaux de correction d’algorithmes seront proposés. Un exemple de raisonnement type pour prouver la correction des algorithmes gloutons pourra éventuellement faire l’objet d’un développement.

(2015 : 927 - Exemples de preuve d'algorithme : correction, terminaison.) Le jury attend du candidat qu'il traite des exemples d'algorithmes récursifs et des exemples d'algorithmes itératifs. En particulier, le candidat doit présenter des exemples mettant en évidence l'intérêt de la notion d'invariant pour la correction partielle et celle de variant pour la terminaison des segments itératifs. Une formalisation comme la logique de Hoare pourra utilement être introduite dans cette leçon, à condition toutefois que le candidat en maîtrise le langage.

Plans/remarques :

2018 : Leçon 927 - Exemples de preuve d’algorithme : correction, terminaison.


2016 : Leçon 927 - Exemples de preuve d'algorithme : correction, terminaison.


2015 : Leçon 927 - Exemples de preuve d'algorithme : correction, terminaison.


Retours d'oraux :

2016 : Leçon 927 - Exemples de preuve d'algorithme : correction, terminaison.

  • Leçon choisie :

    927 : Exemples de preuve d'algorithme : correction, terminaison.

  • Autre leçon :

    924 : Théories et modèles en logique du premier ordre. Exemples.

  • Développement choisi : (par le jury)

    Preuve de la factorielle en logique de Hoare

  • Autre(s) développement(s) proposé(s) :

    Pas de réponse fournie.

  • Liste des références utilisées pour le plan :

    Pas de réponse fournie.

  • Résumé de l'échange avec le jury (questions/réponses/remarques) :

    Quelques questions sur le développement :
    - Une règle de conséquence que j'avais oublié d'appliquer, vite rectifié
    - La logique de Hoare est-elle adaptée pour l'automatisation (j'avais un peu parlé de ça en conclusion du développement). Je dis que le problème est surtout de deviner certaines assertions, pour ça on a les weakest prediconditions (wp).
    - Des exemples de wp ? Je parle de l'assignation, on m'a suggéré de regarder la séquence, et c'est aussi facile.
    - Est-ce que la logique de Hoare prouve la correction ? Non, seulement la correction partielle.

    Sur le plan :
    - Vous parlez d'ensemble bien fondé mais uniquement dans le cas des fonctions récursives... Non en fait pour les algos itératifs c'est pareil, juste un peu de maladresse dans mon plan. Exemple d'ensemble bien fondé ? (j'avais mis $\mathbb{N}^2$ muni de l'ordre lexicographique dans mon plan...) Un exemple de terminaison de programme itératif qui l'utilise ? Je dis qu'on peut réécrire un programme récursif que j'avais donné (Binôme de Newton) en mode itératif, j'ai un peu galéré alors que c'était assez con...
    - La terminaison de programme est un problème difficile (je donnais l'exemple de la conjecture de Syracuse). Est-ce que vous connaissez des problèmes dont la correction est arbitrairement difficile ? J'avoue que le "arbitrairement" m'a pas mal dérouté, j'avais aucune idée d'où il voulait m'emmener, du coup on est passé à autre chose.
    - Vous connaissez Dijkstra ? (sérieusement ?) Preuve de la correction ? J'explique qu'à l'étape $i$ on a la longueur du plus court chemin passant par au plus $i$ sommets, ça n'avait pas l'air d'avoir convaincu... Ils voulaient un invariant, c'est assez délicat et eux même n'étaient pas d'accord... On y réfléchit un peu ensemble.

    Exercices :
    - On définit une fonction $f$ de la façon suivante :
    $$f(x) =
    \begin{cases}
    x - 10 & \text{ si } x > 42 \\
    f(f(x+11)) & \text{ sinon}
    \end{cases}
    $$
    Montrer que $f$ termine. On me demande rapidement de calculer $f(42)$, $f(41)$, j'ai montré que si $x \leq 42$, $f(x) = 33$ en raisonnant par "tranches". A la fin, un des membres du jury m'a aussi suggéré une récurrence forte, qui aurait été plus simple c'est vraie...

    - On prend une matrice $n \times n$ triée par ligne et par colonne. Algorithme de recherche d'un élément $x$ en temps linéaire ? Comment le prouver ? Là j'ai expliqué quelle info on pouvait avoir en comparant $x$ à un élément de la matrice, mais il ne me restait plus beaucoup de temps.

  • Quelle a été l'attitude du jury (muet/aide/cassant) ?

    Jury très sympathique, bienveillant et sollicitant. Il y avait Laurent Cheno (Inspecteur Général), Judicaël Courant, et une femme (celle qui m'a acceuillie) dont j'ai oublié le nom.

  • L'oral s'est-il passé comme vous l'imaginiez ou avez-vous été surpris par certains points ? Cette question concerne aussi la préparation.

    Je pense qu'ils ont apprécié que je parle de logique de Hoare (c'est assez suggéré dans le rapport) et surtout que je sois capable de discuter dessus après (j'avais pas mal potassé aussi pendant la préparation).

  • Note obtenue :

    20