Le drapeau tricolore, preuve totale intégrale

L'invariant $\mathcal{I}$ structure le tableau en quatre zones : $$t[\mathrm{0..}g-1]\in \{0\},t[g..i-1]\in \{1\},t[i..d]\text{ inconnu},t[d+\mathrm{1..}n-1]\in \{2\}$$ Examinons la conservation selon la valeur de $t[i]$ :

• Si $t[i]==0$ : On échange $t[i]$ avec $t[g]$ (qui contient un 1 ou est égal à $i$). Le 0 est ainsi correctement placé à la fin de la zone des 0. En incrémentant g et i, l'invariant est préservé.
• Si $t[i]==1$ : On se contente d'avancer i. Le 1 intègre naturellement la fin de la zone des 1. L'invariant est préservé.
• Si $t[i]==2$ : On l'échange avec $t[d]$ et on décrémente d. Le 2 est correctement placé au début de la zone des 2. Cependant, la valeur ramenée en position $i$ (qui provient de $t[d]$) est inconnue. On ne doit pas incrémenter i afin d'analyser cette valeur au tour suivant. L'invariant est préservé.