Un invariant trop faible

Bien que l'invariant ${\mathcal{I}}^{\prime }$ soit initialisé et conservé à chaque tour, à la fin de la boucle (lorsque $i=n$), la propriété obtenue est " $m$ est un élément de $t$ ". Cette propriété n'implique pas la postcondition voulue ($m\ge x$ pour tout $x\in t$), car n'importe quel élément du tableau la valide. L'invariant doit être renforcé en formulant la domination : $\mathcal{I}:$ " $m$ est le maximum du sous-tableau $t[\mathrm{0..}i-1]$ ".