Spécification, tests et preuve d'un algorithme

def renverse(t: list) -> list:
    """Renvoie une nouvelle liste contenant les éléments de t inversés.

    Précondition : t est une liste.
    Postcondition : renvoie une liste r de même longueur que t telle que
    r[i] == t[len(t) - 1 - i] pour tout indice i. La liste t n'est pas modifiée.
    """
    r = []
    n = len(t)
    for i in range(n):
        # Invariant : r est égale aux i derniers éléments de t inversés : [t[n-1], ..., t[n-i]]
        r.append(t[n - 1 - i])
    return r

Jeu de tests associés :

assert renverse([1, 2, 3]) == [3, 2, 1]
assert renverse([]) == []
assert renverse([5]) == [5]
assert renverse([1, 2, 2]) == [2, 2, 1]
# Vérification de la non-altération de la liste originale t
t_original = [1, 2, 3]
renverse(t_original)
assert t_original == [1, 2, 3]

Démonstration de la preuve : L'invariant ${\mathcal{I}}_i$ s'énonce : "au début de l'étape d'indice $i$, la liste $r$ contient les $i$ derniers éléments de $t$ inversés".

• Initialisation ($i=0$) : Avant d'entrer dans la boucle, $r$ est vide, ce qui correspond bien aux 0 derniers éléments de $t$. ${\mathcal{I}}_0$ est vraie.
• Conservation : Supposons ${\mathcal{I}}_i$ vraie. Durant l'étape $i$, on ajoute à la fin de $r$ l'élément $t[n-1-i]$. Par conséquent, la nouvelle liste $r$ est constituée des $i+1$ derniers éléments de $t$ inversés. La propriété ${\mathcal{I}}_{i+1}$ est donc vérifiée.
• Conclusion : À la sortie de la boucle ($i=n$), la liste $r$ contient les $n$ derniers éléments de $t$ inversés, ce qui correspond à la liste complète inversée. Le calcul est correct.