1. Il y a une seule comparaison au lieu de deux dans le corps de la boucle. On peut espérer un gain non négligeable. La « preuve » d'un tel bout de code devient un impératif.
   
   
2. C'est évident en cas de réponse positive, (à cause du test d'égalité). C'est un peu moins direct en cas de réponse négative. Supposons -1 ≤ low < high ≤ n (voir la suite, mais il est assez évident que low croît et high décroit, tous deux au sens large) et distinguons trois sous-cas,
   • Si low = -1 alors high est zéro et k est strictement plus petit que tous les éléments du tableau qui est trié.
   • Si high = n, alors low est n-1 et k est strictement plus grand que tous les éléments du tableau.
   • Sinon, on a trouvé x = low indice valide, tel que x+1 est aussi un indice valide, avec t[x] < k < t[x+1], et donc k ne peut pas se trouver dans le tableau t.
   Il est notable que c'est la seule intervention de l'hypothèse de tri.
   
   
3. Sous l'hypothèse high-low > 1, on a cette fois low < m < high. La quantite high-low décroit strictement, d'un tour de boucle au suivant. Plus précisément, la quantité high-low passe de 2p+1 (avec 1 ≤ p) à p ou p+1, ou bien de 2p (avec 1 ≤ p) à p. Il y a donc bien décroissance stricte.
   
   
4. Enrichissons l'invariant de quelques inégalités et ajoutons les assertions.

   static boolean searchBis(int [] t, int k) {     int low = -1 ;     int high = t.length ; // -1 ≤ low < high ≤ n ∧ t[low] < k ≤ t[high]     while (high-low > 1) { // -1 ≤ low < low+1 < high ≤ n ∧ t[low] < k ≤ t[high]       int m = (low+high)/2 ; // -1 ≤ low < m < high ≤ n ∧ t[low] < k ≤ t[high]       if (t[m] < k) { // -1 ≤ low < m < high ≤ n ∧ t[m] < k ≤ t[high]         low = m ; // -1 ≤ low < high ≤ n ∧ t[low] < k ≤ t[high]       } else // -1 ≤ low < m < high ≤ n ∧ t[low] < k ≤ t[m]         high = m ; // -1 ≤ low < high ≤ n ∧ t[low] < k ≤ t[high]     } // -1 ≤ low < high ≤ n ∧ high = low+1 ∧ t[low] k ≤ t[high]     return high < t.length && t[high] == k ;   }

   Une fois trouvé l'invariant la pose des insertions est assez mécanique.