Donner l'invariant de la boucle de recherche , et mener les trois…

L'invariant. Avant le tour d'indice $i$, aucun des éléments t[0..i-1] n'est égal à v.

Remarquez la forme : l'invariant porte sur ce qui est derrière la frontière, et il énonce une absence. C'est normal — tant qu'on n'a rien trouvé, tout ce qu'on sait est ce qu'on n'a pas vu.

Initialisation. Avant le premier tour, $i=0$ : la tranche t[0..-1] est vide, et « aucun élément d'une tranche vide n'est égal à v » est vrai — vrai par vacuité, comme toute propriété universelle sur l'ensemble vide.

Conservation. Supposons l'invariant vrai avant le tour $i$. Le tour teste t[i] == v. Si le test est vrai, la fonction sort par return i : il n'y a pas de tour suivant, il n'y a rien à conserver. S'il est faux, alors t[i] n'est pas égal à v non plus, donc aucun élément de t[0..i] ne l'est : l'invariant vaut avant le tour $i+1$.

Terminaison. Deux sorties possibles, et il faut traiter les deux.

• Par return i : on a testé t[i] == v et il est vrai, donc t[i] == v — la seconde moitié de la postcondition. Et l'invariant garantit qu'aucun indice plus petit ne convenait : c'est bien la première occurrence.
• Par épuisement de la boucle : $i$ a atteint $n$, l'invariant dit qu'aucun élément de t[0..n-1] — c'est-à-dire du tableau entier — n'est égal à v. Renvoyer $-1$ est donc juste.

La vérification machine. La postcondition entière, y compris la primauté de l'occurrence, a été testée sur $3000$ tableaux tirés au hasard :

r = recherche(t, v)
if r == -1:
    assert all(x != v for x in t)
else:
    assert 0 <= r < len(t) and t[r] == v
    assert all(t[k] != v for k in range(r))     # c'est bien la PREMIERE

$3000$ cas passent. Mais la preuve, elle, vaut pour tous les tableaux — y compris ceux que le tirage n'a pas produits. C'est toute la différence.