927 - Exemples de preuve d’algorithme : correction, terminaison.2021

Rapport du jury 2019

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 peut 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 doivent être proposés. Un exemple de raisonnement type pour prouver la correction des algorithmes gloutons peut éventuellement faire l’objet d’un développement.