Invariant du maximum

Démonstration : Définissons la propriété ${\mathcal{I}}_i$ : "au début de l'itération d'indice $i$, la variable $m$ est égale au maximum de la sous-liste $t[\mathrm{0..}i-1]$".

• Initialisation ($i=1$) : Avant le premier passage dans la boucle, $m=t[0]$, qui est bien l'unique valeur et donc le maximum de la liste réduite $t[\mathrm{0..0}]$. La propriété ${\mathcal{I}}_1$ est vraie.
• Conservation : Supposons que ${\mathcal{I}}_i$ est vraie au début de l'étape $i$. Durant cette étape, on examine $t[i]$ :
• Si $t[i]>m$, la variable $m$ prend la valeur $t[i]$. $m$ devient supérieur à tous les éléments de $t[\mathrm{0..}i-1]$ et est égal à $t[i]$. C'est donc bien le maximum de $t[\mathrm{0..}i]$.
• Si $t[i]\le m$, la valeur de $m$ reste inchangée. Comme $m$ majorait déjà $t[\mathrm{0..}i-1]$, et qu'il majore également $t[i]$, il reste le maximum de $t[\mathrm{0..}i]$. Dans tous les cas, la propriété ${\mathcal{I}}_{i+1}$ est vraie à la fin de l'itération.
• Conclusion : À la sortie de la boucle, $i=\text{len}(t)=n$. Par récurrence, ${\mathcal{I}}_n$ est vraie : la variable $m$ est égale au maximum de $t[\mathrm{0..}n-1]$, c'est-à-dire de la liste complète t. La postcondition est démontrée.