Correct mais sans variant simple — et l'inverse

Soit la fonction :

import random
def indice_max_hasard(t: list) -> int:
    while True:
        i = random.randrange(len(t))
        if all(t[i] >= x for x in t):
            return i

• Correction partielle : Le seul point de sortie est l'instruction return i qui est conditionnée par le fait que t[i] soit supérieur ou égal à toutes les valeurs du tableau. Si la boucle s'arrête, la postcondition est donc nécessairement vraie.
• Terminaison : Rien ne garantit l'arrêt. Il existe une probabilité non nulle (bien qu'infinitésimale) que le tirage aléatoire ne sélectionne jamais l'indice du maximum (ex: tirages répétés du même indice non optimal). Aucun variant entier strictement décroissant ne peut être défini.