Recherche par dichotomie

Le problème

Le problème consiste à écrire le code de la fonction index ci-dessous, puis à justifier que ce code est correct.

In [ ]:
def index(L, x):
    """ Retourne le plus petit indice i tel que L[i] >= x.
        Retourne -1 si L[i] < x pour tout i.
        
        Les éléments de L sont supposés être ordonnés par
        ordre croissant.
    """

Lire la spécification externe

Question 1

Indiquer la valeur retournée lors de chacun de ces appels :

index([4, 6, 7, 12, 24], 2)
index([4, 6, 7, 12, 24], 7)
index([4, 6, 7, 12, 24], 10)
index([4, 6, 7, 12, 24], 27)

Concevoir la boucle

Question 2

Exprimer en quelques phrases, l'idée de l'algorithme.

Question 3

Quelles sont les informations que vous devez mémoriser à chaque nouvelle itération pour décrire l'état d'avancement du calcul ?

Question 4

Choisir des variables. Les nommer et écrire ce qu'elles représentent dans l'état d'avancement du calcul.

Question 5

Faire un schéma pour représenter l'état d'avancement au début d'une itération quelconque.

Question 6

Décrire le travail à réaliser pour progresser jusqu'à l'itération suivante.

Question 7

Écrire les instructions python à placer à l'intérieur de la boucle.

Question 8

Quelle est la situation initiale ? Faire un schéma.

Question 9

Écrire les instructions Python qui initialisent les variables de boucle.

Question 10

Quel est l'état d'avancement qui correspond à l'état final ? Faire un schéma.

Question 11

Écrire la condition de boucle.

Question 12

À partir de l'état final, comment obtient-on la valeur de l'indice i à retourner.

Question 13

Écrire le code complet de la fonction index.

In [ ]:
 

Prouver la correction de la boucle

Question 14

Écrire un invariant de boucle , c'est-à-dire une propriété (P) liée aux variables de boucle et qui est satisfaite au début de chaque itération.

Question 15

Justifier que (P) est satisfaite au début de la première itération.

Question 16

Justifier que si $(P)$ est satisfaite au début d'une itération alors elle sera également satisfaite au début de l'itération suivante.

Question 17

Justifier que la boucle se termine au bout d'un nombre fini d'itérations. Exhiber pour cela une quantité entière qui décroit strictement à chaque itération.

Question 18

Écrire les propriétés qui sont satisfaitent en sortie de boucle.

Question 19

En déduire que la fonction retourne une valeur correcte.