Invariant du maximum

Exercice · informatique (tronc commun des prépas scientifiques), chapitre 1 — La discipline de programmation

Énoncé

Prouver par invariant la correction de la fonction suivante calculant le maximum d'une liste non vide :

def maximum(t: list) -> float:
    m = t[0]
    for i in range(1, len(t)):
        if t[i] > m:
            m = t[i]
    return m

Corrigé

Démonstration : Définissons la propriété $I_{i}$ : "au début de l'itération d'indice $i$ , la variable $m$ est égale au maximum de la sous-liste $t [0.. i - 1]$ ".

Initialisation ( $i = 1$ ) : Avant le premier passage dans la boucle, $m = t [0]$ , qui est bien l'unique valeur et donc le maximum de la liste réduite $t [0..0]$ . La propriété $I_{1}$ est vraie.
Conservation : Supposons que $I_{i}$ est vraie au début de l'étape $i$ . Durant cette étape, on examine $t [i]$ :
Si $t [i] > m$ , la variable $m$ prend la valeur $t [i]$ . $m$ devient supérieur à tous les éléments de $t [0.. i - 1]$ et est égal à $t [i]$ . C'est donc bien le maximum de $t [0.. i]$ .
Si $t [i] \leq m$ , la valeur de $m$ reste inchangée. Comme $m$ majorait déjà $t [0.. i - 1]$ , et qu'il majore également $t [i]$ , il reste le maximum de $t [0.. i]$ . Dans tous les cas, la propriété $I_{i + 1}$ est vraie à la fin de l'itération.
Conclusion : À la sortie de la boucle, $i = len (t) = n$ . Par récurrence, $I_{n}$ est vraie : la variable $m$ est égale au maximum de $t [0.. n - 1]$ , c'est-à-dire de la liste complète t. La postcondition est démontrée.

Les autres exercices de ce chapitre Le cours du chapitre

Un blocage sur cet exercice ? Le tuteur d'Adloun guide par questions, sans donner la réponse.