liste = [3, 1, 4, 1, 5, 9, 2, 6, 5, 3, 5, 8]


def maximum(liste):
    max = liste[0]
    for i in range(0, len(liste)):
        if liste[i] > max:
            max = liste[i]
        #Invariant de boucle
        assert max == sorted(liste[:i+1])[-1]
    assert max == sorted(liste[:])[-1]
    return max

print(maximum(liste))
print(maximum(liste[:4]))

# Il faut prouver :
#1. L'invariant de boucle est vrai au départ
#2. L'invariant de boucle est préservé lors d'une itération
#3. Quand on sort de la boucle, la post-condition de la boucle est vérifiée

#1. Invariant vrai au départ :
#max = liste[0] => max == sorted(liste[0])[-1]
#2. Invariant préservé
#max == sorted(liste[:i+1])[-1] & liste[i+1] > max => [max := liste[i+1]](max == sorted(liste[:i+2][-1]))
#2.1 le nouvel élément est plus petit que le max mémorisé :
#max == sorted(liste[:i+1])[-1] & liste[i+1] <= max => max == sorted(liste[:i+2][-1])
#Principe : sorted(liste[:i+2])[-1] = max(liste[:i+2])
#                                  = max(max(liste[:i+1]),liste[i+1])]
#                                  = max(liste[:i+1])
#                                  = sorted(liste[:i+1])[-1]
#                                  = max
#2.2 le nouvel élément est plus petit que le max mémorisé :
#max == sorted(liste[:i+1])[-1] & liste[i+1] > max => [max := liste[i+1]](max == sorted(liste[:i+2][-1]))
#Soit :
#max == sorted(liste[:i+1])[-1] & liste[i+1] > max => liste[i+1]] == sorted(liste[:i+2][-1])
#Principe : sorted[liste[:i+2][-1] = max(liste[:i+2])
#                                  = max(max(liste[:i+1]),liste[i+1])]
#                                  = liste[i+1]
#                                  = max
#3. Sortie de boucle
#max == sorted(liste[:i+1])[-1] & i = len(liste) => max == sorted(liste[:])[-1]
#max == sorted(liste[:i+1])[-1] = sorted(liste[:len(liste)])[-1] = sorted(liste[:])[-1]