Produit de deux entiers

def multiplication(a, b):
    """
    a -- entier naturel
    b -- entier    

    renvoie le produit a*b
    """

    p = 0
    m = 0

    while m < a:
        m = m + 1
        p = p + b

    return p

• Est-ce que m est un variant de la boucle?

Réponse

Oui...et non.

• Si l'on s'en tient à l'idée essentielle: variable ne pouvant prendre qu'un nombre fini de valeurs distinctes dans les passages de la boucle (ce qui garantit la terminaison), alors la réponse est oui: la variable m ne peut prendre que les valeurs entre 0 et a (a est fixe) et ne prend jamais deux fois la même valeur puisque la valeur de m croît strictement à chaque passage dans la boucle.

• Toutefois, on cherchera à se ramener systématiquement à la définition donnée au départ (afin de simplifier le discours) d'une suite de valeurs entières strictement décroissante. Pour se ramener à cela, la modification est simple: on raisonne avec a-m au lieu de m (c'est l'objet de la question suivante).

• Prouver que la boucle termine en établissant que a-m est un variant de la boucle.

Une résolution

a - m est un variant.

• a - m est un entier positif dans la boucle (puisqu'on ne rentre dans le corps de boucle que si $m < a$).
• m augmente strictement à chaque passage dans la boucle et a est inchangé, donc a -m diminue strictement.

On a explicité un variant donc la boucle termine.