Preuve d'algorithme et Invariant de boucle

Lire le cours, puis faire la fiche d'exercice avant de passer à la suite. Les solutions des exercices de la fiche sont sur la dernière page. Audio du cours

Exercice 1 : invariant de boucle du tri par insertion

Introduction

Nous allons travailler sur le tableau A = [27, 10, 12, 8, 11].

Divisons le tableau A en 2 parties :

• Une première partie qui contient les éléments d'index 1 à i-1. Ce sous-tableau sera noté A1[1..i-1].
• Une seconde partie qui contient le reste du tableau A (index i à n).

1. Dans l'algorithme tri_insertion, à quelle valeur est initialisée la variable i ?
2. Sur l'exemple A donné, écrire ce que vaut le sous-tableau A1, ainsi que le tableau A, au début des 5 premières itérations.
3. Que peut-on conclure sur le sous-tableau A1 au début de chaque itération ?

Invariant de boucle

Dans un cas général (valable pour tous les tableaux à trier A), notre invariant de boucle pourrait être : Le sous-tableau A[1..i-1] est trié.

Pour montrer qu'un invariant de boucle permet d'attester de l'exactitude de l'algorithme, il faut montrer les 3 étapes initialisation / conservation / terminaison.

4. Initialisation : montrer que l'invariant de boucle est vrai avant la première itération.
5. Conservation : on suppose que l'invariant est vrai à l'itération i. Montrer qu'il demeure vrai jusqu'à la fin de la boucle. Attention, il faut prendre en compte l'incrémentation cachée de i.
6. Terminaison : est-ce qu'il y a terminaison de l'algorithme ? Si oui, pourquoi ? Si oui, que devient l'invariant de boucle ?

Correction

Elle est ici.

Cet exercice a trouvé son inspiration ici.

Exercice 2: invariant de boucle du tri par sélection

Reprendre l'exercice précédent mais pour le tri sélection cette fois-ci.

Répondre aux mêmes questions.

Correction

Elle est ici.