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


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

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

#preuve de terminaison
#    variant = len(liste) - i
#    (N, <) : structure bien fondée
#    init -> variant in N
#    variant in N & i <= len(liste) => [i = i+1](variant in N)
#    variant = v => [i = i +1]variant < v
#correction totale
#    variant = borneInf => max = maximum