1. Quand on sait que le nombre demandé est entre x et y, on propose la moyenne m = (x+y)/2. En cas d'échec, on continue la recherche dans les intervalles [x…m-1] ou [m+1…y] selon que m est plus grand ou plus petit que le nombre mystère. Dans le cas de l'intervalle de départ [1…10] on propose 5, ce qui nous donne en cas d'échecs répétées un intervalle de taille au pire 5, puis 2, et c'est fini (intervalle de taille 1 et donc réponse exacte assurée, ou détection, au mieux, d'une erreur dans les réponses précédentes).
   
   
2. Soit la propriété φ(i,j) qui exprime que si k se trouve dans le tableau complet t[0...n[, alors k se trouve dans le sous-tableau t[i...j[.

   φ(i,j) =

   (

   k ∈ t[0...n[ ⇒ k ∈ t[i...j[

   )

   static boolean search(int [] t, int k) {     int low = 0 ;     int high = t.length ; // 0 ≤ low ≤ high ≤ n ∧ φ(low, high)     while (high-low > 0) { // 0 ≤ low < high ≤ n ∧ φ(low, high)       int m = (low+high) / 2 ; // 0 ≤ low ≤ m < high ≤ n ∧ φ(low, high)       if (k < t[m]) { // φ(low,m) ∧ 0 ≤ low ≤ m < high ≤ n         high = m ; // φ(low, high) ∧ 0 ≤ low ≤ high < n       } else if (k > t[m]) { // φ(m+1,high) ∧ 0 ≤ low ≤ m < high ≤ n ∧ φ(low, high)         low = m+1 ; // φ(low, high) ∧ 0 < low ≤ high ≤ n       } else { // t[m] = k         return true ; // Rien~!       } // φ(low, high) ∧ 0 ≤ low ≤ high ≤ n     } // 0 ≤ low = high ≤ n ∧ φ(low,high)     return false ;   }

   La correction est prouvée car la dernière assertion entraîne que k n'est pas dans le tableau. Les passages importants sont de φ(low,high) à φ(low, m) et φ(m+1, high), ils utilisent l'hypothèse d'un tableau trié.
   
   
3. Il y a un argument qui tue : entre le début et la fin d'une itération de la boucle, un élément (celui d'indice m) est exclu de l'intervalle de recherche. Cet argument révèle la robustesse du programme, m peut aussi bien être n'importe quel indice valide de l'intervalle [low…high[.
   
   Plus conformément au cours, on peut considérer l'ordinal high-low (c'est bien un entier naturel) qui décroit strictement du début à la fin d'une itération. En effet sous l'hypothèse low < high et en posant m = (low+high)/2 alors il vient low ≤ m < high. Soit encore m-low < high-low et high-m ≤ high-low (et donc high - (m+1) < high-low). On peut être plus précis, si high-low est impair et vaut 2p+1 alors le nouvel intervalle est de taille p, sinon high-low = 2p (p ≥ 1) et le nouvel intervalle est de taille p ou p-1.
   
   
4. Un premier point important est de constater que la terminaison ne dépend pas des éléments du tableau. En revanche la correction en dépend. Dans tous les cas, si search(t, k) répond vrai, alors le résultat est exact, sinon, le résultat peut être exact. Dans le cas où le tableau est trié à l'envers, on aura search(t, k) == true, si et seulement si k est l'élément d'indice médian de t.
   
   
5. Le code est peut être un peu plus régulier :

   static boolean search(int [] t, int k) {     int low = 0 ;     int high = t.length-1 ;     while (low <= high) {       int m = (low+high) / 2 ;       if (k < t[m]) {         high = m-1 ;       } else if (k > t[m]) {         low = m+1 ;       } else {         return true ;       }     }     return false ;   }