Information

Author(s) Vincent Branders, Pierre Dupont
Deadline 22/04/2026 14:00:00
Submission limit No limitation

Συνδεθείτε

[TP09] La règle d'Horner - Invariant

Le pseudocode suivant propose une implémentation de la règle d'Horner afin de calculer la valeur d'un polynôme en un point. On vous demande de prouver la correction de l'algorithme en :

  1. traduisant dans un premier temps la boucle for en boucle while,
  2. puis en mettant en oeuvre les différentes étapes de preuve par invariant.
https://inginious.info.ucl.ac.be/course/LINFO1103/S09_5_1_horner/algo.png

Question 1: Définir l'invariant

Pour trouver l'invariant :

  1. Commencez par analyser un exemple simple.
  2. Déterminez l'état des variables après l'initialisation.
  3. Déterminez l'état des variables après chaque itération de la boucle while.

Qu'observez-vous à la fin de chaque itération ?

Sélectionnez, parmi les propositions suivantes, celle(s) qui est (sont) respectée(s) à la fin de chaque itération.

Pour rappel, lorsque l'on transforme une boucle for en boucle while, la dernière instruction dans cette boucle est la mise à jour de la variable de boucle (ici i). Nous nous intéressons donc à l'état de l'algorithme juste après cette mise à jour et donc avant de revenir à l'instruction while.

Question 2: Initialisation

L'invariant est-il vérifié après l'initialisation ?

Pour rappel, lorsque l'on transforme une boucle for en boucle while, l'initialisation concerne aussi celle de la variable de boucle (i = ...). Donc, l'initialisation se réfère à toutes les instructions effectuées avant de tester pour la première fois la condition dans l'instruction while.

Sélectionnez, parmi les propositions suivantes, celle qui répond à la question précédente.

Question 3: Itération

L'invariant est-il conservé par l'exécution d'une itération ?

Sélectionnez, parmi les propositions suivantes, celle(s) qui est (sont) correcte(s).

Question 4: Condition de terminaison

Lorsque la condition de terminaison est atteinte, l'invariant définit la post-condition.

Sélectionnez, parmi les propositions suivantes, celle qui correspond à la condition d'arrêt de la boucle.

Question 5: Preuve

Si l'on utilise la condition d'arrêt pour mettre à jour l'invariant, la correction de la fonction est prouvée.

Sélectionnez, parmi les propositions suivantes, celle(s) qui prouve(nt) que la fonction est correcte.