Écrire le prototype, la précondition et la postcondition d'une…

Prototype. indice_du_maximum(t), où t est un tableau de nombres ; le résultat est un entier.

Précondition. len(t) > 0. Un tableau vide n'a pas de maximum, donc pas d'indice de maximum : la fonction ne peut rien promettre.

Postcondition. C'est ici que se joue l'exercice. Écrire « le résultat est l'indice du plus grand élément » suppose qu'il n'y en ait qu'un. La formulation correcte évite l'article défini :

$$0\le i<\text{len(t)}\text{et}t[i]\ge t[j]\text{ pour tout }j.$$

Elle reste vraie en cas d'ex æquo : elle affirme qu'aucun élément ne dépasse t[i], sans prétendre que t[i] est seul de son espèce.

def indice_du_maximum(t):
    """Indice d'un plus grand element de t.

    Precondition  : t est un tableau non vide.
    Postcondition : 0 <= i < len(t) et t[i] >= t[j] pour tout j.
                    En cas d'ex aequo, l'indice rendu est le plus petit.
    """
    assert len(t) > 0, "tableau vide"
    i = 0
    for j in range(len(t)):
        if t[j] > t[i]:
            i = j
    assert 0 <= i < len(t) and all(t[i] >= x for x in t)
    return i

Vérification. indice_du_maximum([3, 1, 4, 1, 5]) rend $4$ ; [7, 7, 7] rend $0$ ; [-3, -1, -7] rend $1$ ; [5] rend $0$. Puis, sur $2000$ tableaux aléatoires de longueurs $1$ à $12$ et de valeurs dans $[-50,50]$ :

for _ in range(2000):
    t = [random.randint(-50, 50) for _ in range(random.randint(1, 12))]
    assert t[indice_du_maximum(t)] == max(t)

Le détail qui décide : la comparaison est > et non >=. Avec >=, la fonction rendrait le dernier indice maximal — ce qui est tout aussi correct vis-à-vis de la postcondition ci-dessus, mais contredirait la précision ajoutée dans la docstring. On ne documente que ce que le code garantit.