Parcourir, trier, prouver

Cours · NSI (première), chapitre 7 · première, spécialité numérique et sciences informatiques · le début du chapitre, la suite sur Adloun

Un tri : des valeurs en désordre rangées en barres croissantes, élément par élément.

Jusqu'ici, on a écrit des programmes et on les a testés. Le chapitre 3 disait déjà pourquoi cela ne suffit pas : « le succès d'un jeu de tests ne garantit pas la correction d'un programme ». Un test porte sur une entrée ; un programme doit être juste sur toutes.

Ce chapitre franchit le pas. On y écrit les algorithmes classiques du programme — parcours, recherche, tris — et surtout on apprend à démontrer qu'ils sont corrects et qu'ils s'arrêtent, à l'aide de deux outils : l'invariant et le variant. C'est le moment où l'informatique cesse d'être une affaire d'essais pour devenir une science.

7.1 Le parcours séquentiel

Capacité attendue

« Écrire un algorithme de recherche d'une occurrence sur des valeurs de type quelconque. Écrire un algorithme de recherche d'un extrémum, de calcul d'une moyenne. »

7.1.1 Rechercher une occurrence


def recherche(t, v):
    """Indice de la PREMIÈRE occurrence de v dans t, ou -1 si v n'y figure pas.

    Précondition  : les éléments de t sont comparables à v par ==.
    Postcondition : si le résultat r vaut -1, aucun élément de t n'est égal
                    à v ; sinon 0 <= r < len(t) et t[r] == v.
    """
    for i in range(len(t)):
        if t[i] == v:
            return i
    return -1

iRemarque

Le programme précise « sur des valeurs de type quelconque » : rien dans cette fonction ne suppose des nombres. Elle cherche aussi bien une chaîne, un p-uplet ou un booléen — seule l'égalité est requise. C'est ce qui la rend réutilisable, et c'est un trait à rechercher dans tout algorithme.

Complexité : Coût de la recherche séquentielle

Dans le pire cas — la valeur absente, ou placée en dernier — la boucle effectue $n$ comparaisons sur un tableau de $n$ éléments. Le coût est linéaire : doubler la taille du tableau double le travail. Le programme le formule ainsi : « on montre que le coût est linéaire ».

7.1.2 Extrémum et moyenne


def indice_maximum(t):
    """Indice d'un plus grand élément de t.

    Précondition  : t est non vide.
    Postcondition : t[r] >= t[k] pour tout k. En cas d'ex aequo, l'indice
                    du PREMIER maximum rencontré.
    """
    assert len(t) > 0, "tableau vide"
    m = 0
    for i in range(1, len(t)):
        if t[i] > t[m]:
            m = i
    return m


def moyenne(t):
    """Moyenne arithmétique de t. Précondition : t est un tableau non vide
    de nombres. La postcondition est celle du chapitre 3, avec sa tolérance."""
    assert len(t) > 0, "tableau vide"
    total = 0
    for x in t:
        total = total + x
    return total / len(t)

AttentionNe jamais initialiser un extrémum par une constante

Attention à la notation : dans le code ci-dessus, m = 0 est correct, car m y désigne un indice — celui du premier élément. L'erreur du chapitre 3 était tout autre : y initialiser la valeur du maximum à $0$ , ce qui donne le maximum entre $0$ et le tableau, et renvoie $0$ si tous les éléments sont négatifs.

La règle est la même dans les deux cas : on part du premier élément, jamais d'une constante choisie d'avance. D'où la précondition « t est non vide », sans laquelle ni t[0] ni l'indice $0$ n'auraient de sens. Elle n'est pas là pour faire joli : elle rend l'initialisation légitime.

7.2 Prouver qu'une boucle est correcte : l'invariant

Définition 7.1Invariant de boucle

Un invariant de boucle est une propriété qui est vraie avant d'entrer dans la boucle et qui reste vraie après chaque tour. Si l'on montre de plus que, à la sortie, l'invariant entraîne le résultat voulu, on a prouvé la correction de la boucle — sur toutes les entrées à la fois.

La démonstration se fait toujours en trois temps, et il faut les trois :

Initialisation : l'invariant est vrai avant le premier tour.
Conservation : s'il est vrai avant un tour, il l'est encore après.
Terminaison : quand la boucle s'arrête, l'invariant plus la condition d'arrêt donnent le résultat cherché.

Exemple 7.2Invariant de indice_maximum

Invariant : avant le tour d'indice $i$ , la variable m contient l'indice d'un plus grand élément parmi t[0..i-1].

Initialisation. Avant le premier tour, $i = 1$ et m vaut $0$ : c'est bien l'indice du maximum de t[0..0], qui n'a qu'un élément.

Conservation. Supposons l'invariant vrai avant le tour $i$ . Le tour compare t[i] à t[m]. Si t[i] est plus grand, m devient $i$ ; sinon m ne change pas. Dans les deux cas, m désigne un plus grand élément de t[0..i] — donc l'invariant est vrai avant le tour $i + 1$ .

Terminaison. La boucle s'arrête pour $i = n$ . L'invariant dit alors que m est l'indice d'un plus grand élément de t[0..n-1], c'est-à-dire du tableau entier. C'est exactement la postcondition.

L'invariant se voit bien si l'on dessine la frontière qu'il déplace :

Figure : L'invariant de indice_maximum au moment où

i = 4

. La propriété porte sur la partie déjà parcourue ; on ne prétend rien sur le reste.

Exercices du chapitre

La suite du cours · Tous les exercices du chapitre