Invariant

Exercice 1

On considère le programme suivant:

def max_binaire(a,b):
    """
    a et b sont deux variables de valeurs comparables.
    La fonction renvoie  la plus grande des deux.
    """
    if a > b:
        return a
    else:
        return b

def max_tableau(tab):
    """
    tab est une liste d'éléments comparables.
    La fonction renvoie l'élément le plus grand.
    """
    m = tab[0]
    for i in range(1, len(tab)):
        m = max_binaire(m, tab[i])
        #
    return m

A la ligne marquée d'un #, on peut affirmer:

A. m = max( tab[0], tab[1], ..., tab[i] )
B. m = max( tab[0], tab[1], ..., tab[i-1] )
C. m = max( tab[0], tab[1], ..., tab[i+1] )

Une résolution

• La réponse B est fausse. Faisons un appel de la fonction avec tab = [3,4,5]. En ligne 16 (m = tab[0]), m reçoit la valeur 3. On entre alors dans la boucle. i reçoit la valeur 1. Puis, avec la ligne m = max_binaire(m, tab[i]), m reçoit la valeur max_binaire(3, tab[1]), c'est à dire m ← max_binaire(3, 4), donc m = 4 au niveau de la ligne #. Or max(tab[0], tab[1], ..., tab[i-1]) = max(tab[0]) = 3 $\neq$ 4.

• La réponse C est fausse. Si on reprend l'exemple précédent, pour i = 1, on a m = 4 au niveau de la ligne #. Or max(tab[0], tab[1], ..., tab[i+1]) = max(tab[0], tab[1], tab[2]) = max(3,4,5) = 5 $\neq$ 4.

• La réponse A est correcte: m = max(tab[0], tab[1], ..., tab[i]).

  1. Pour vérifier cela, on vérifie que c'est vrai pour la première valeur de i, c'est à dire pour i = 1. Lorsqu'on entre dans la boucle (valeur de i = 1), on exécute la ligne m = max_binaire(m, tab[i]), c'est à dire m = max_binaire(tab[0], tab[1]), on a donc m = max(tab[0], tab[1], ..., tab[i]).
  2. Puis on vérifie que lorsque c'est vrai pour une valeur de i = k-1 (avec k < len(tab)) alors c'est également vrai pour i = k. On suppose donc que l'on a m = max(tab[0], tab[1], ..., tab[i]) = max(tab[0], tab[1], ..., tab[k-1]) à la fin de la boucle correspondant à i = k-1. Au tour de boucle suivant, on aura i = k. On exécute la ligne 18 m = max_binaire(m, tab[i]), c'est à dire m = max_binaire(max(tab[0], tab[1], ..., tab[k-1]), tab[k]), ou encore m = max(tab[0], tab[1], ..., tab[k-1], tab[k]).
  3. On peut conclure:
     • c'est vrai pour i = 1 (point a) et vrai pour i+1 = 2 (en utilisant le point b).
     • c'est vrai pour i = 2 (point précédent) et vrai pour i+1 = 3 (en utilisant le point b).
     • c'est vrai pour i = 3 (point précédent) et vrai pour i+1 = 4 (en utilisant le point b).
     • ...

Note

Ceux qui arrêtent la spécialité NSI en fin de première auront une épreuve de QCM. Ces QCM proposeront 4 réponses au choix, dont une seule est correcte. Il sera donc possible d'adopter la stratégie: j'élimine des réponses (comme nous l'avons fait pour B et C dans la solution ci-dessus) sans chercher à démontrer la bonne réponse (comme nous l'avons fait pour la réponse A). La stratégie "élimination" est souvent efficace dans un QCM, pensez-y!

Remarque

Pour "vérifier" (sur des exemples et non de façon générique par raisonnement) que l'on a bien m = max( tab[0], tab[1], ..., tab[i] ) à la ligne marquée d'un #, on peut utiliser assert et la fonction max prédéfinie du langage python.

Vérifier que le code suivant (assertion en ligne 19) ne mène pas à une AssertionError.

def max_binaire(a,b):
    """
    a et b sont deux variables de valeurs comparables.
    La fonction renvoie  la plus grande des deux.
    """
    if a > b:
        return a
    else:
        return b

def max_tableau(tab):
    """
    tab est une liste d'éléments comparables.
    La fonction renvoie l'élément le plus grand.
    """
    m = tab[0]
    for i in range(1, len(tab)):
        m = max_binaire(m, tab[i])
        assert( m == max(tab[0:i+1]) )
    return m



if __name__ == '__main__':
    from random import randint

    L = [ randint(1,20) for _ in range(randint(1,12))]
    print(L)
    print(max_tableau(L) == max(L) )

Note

Le code L = tab[i:j] est un code qui affecte à L la liste [ tab[i], tab[i+1], ..., tab[j-1] ]. Attention, donc: le dernier indice est $j-1$.

En particulier tab[0:i+1] est la liste [ tab[0], tab[1], ..., tab[i] ].

Voir cette page de la documentation python pour en savoir plus sur la technique des tranches en python.

Exercice 2

Expliquer comment utiliser la propriété d'invariant établie dans l'exercice précédent, pour établir que la fonction max_tableau renvoie bien le maximum de la liste tab qui lui est passée en paramètre.

Une résolution

Après la dernière boucle, on a i = len(tab)-1 et m = max(tab[0], tab[1], ..., tab[i]). On a donc m = max(tab[0], tab[1], ..., tab[len(tab)-1]). m est donc la valeur maximale contenue dans le tableau.

Exercice 3

On considère le programme suivant:

def max_binaire(a,b):
    """
    a et b sont deux variables de valeurs comparables.
    La fonction renvoie  la plus grande des deux.
    """
    if a > b:
        return a
    else:
        return b

def max_tableau2(tab):
    """
    tab est une liste d'éléments comparables.
    La fonction renvoie l'élément le plus grand.
    """
    m = tab[0]
    for i in range(1, len(tab)-1):
        m = max_binaire(m, tab[i])
        #
    return m

Question 1

A la ligne marquée d'un #, peut-on encore affirmer que l'on a m = max(tab[0], tab[1], ..., tab[i]) ?

Une réponse

Oui, et la démarche de démonstration est exactement la même que dans l'exercice 1.

Question 2

Peut-on en déduire que la fonction max_tableau2 renvoie le maximum de la liste? Si non, donner une liste pour laquelle la fonction ne renvoie pas le maximum et expliquer ce qui est en défaut dans le raisonnement présenté à l'exercice 2.

Une réponse

Après la dernière boucle, on a i = len(tab)-2 et m = max(tab[0], tab[1], ..., tab[i]) donc m = max(tab[0], tab[1], ..., tab[len(tab)-2]). Le raisonnement de l'exercice 2 est valable mais la valeur extrême pour i n'est pas la même: la conclusion n'est donc pas tout à fait la même. m est le maximum du tableau privé de son dernier élément.

m étant le maximum du tableau privé de son dernier élément, pour que la fonction ne renvoie pas le maximum d'une liste L, il faut et il suffit que le maximum de cette liste L soit placé en dernière position dans la liste.