Division par deux, correcte
Cette feuille en Postscript
Soit S une instruction, l'écriture {P} S {Q}, où P est la pré-condition et Q la post-condition, peut se comprendre comme, si P est vraie avant l'éxecution de S alors Q est vraie après l'exécution de S. Dans les programmes on écrit les propositions entre les instructions.

Sans être complètement formel, il semble clair :

1  La recherche dichotomique

Le principe de la recherche dichotomique dans un tableau trié est bien connu.
  1. Expliquer comment ce principe permet de deviner un nombre choisi au hasard entre 1 et 10 en au plus 4 étapes. Le joueur qui cherche propose un nombre et l'autre répond trop grand, trop petit ou exact.
  2. Voici une méthode de recherche d'un nombre k dans un tableau t[0...n[.
      static boolean search(int [] t, int k) {
            int low = 0 ;
            int high = t.length ;
            while (low < high) {
              int m = (low+high) / 2 ;
              if (k < t[m]) {
            high = m ;
          }     else if (k > t[m]) {
            low = m+1 ;
          }     else {
                return true ;
          }
        }
            return false ;
      }
    Équiper le code ci-dessus avec des assertions qui en prouvent la correction. On utilisera 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[ )
    On commencera par trouver l'invariant en n'oubliant pas une condition de validité des indices.

  3. Prouver la terminaison du programme.

  4. Que va t-il se passer si le tableau t n'est pas trié ? Et dans le cas particulier d'un tableau trié à l'envers ?

  5. Modifier le programme pour utiliser des tableaux fermés t[0...n-1].
Solution.

2  Diviser par deux, en plus risqué

Voici une version finement optimisée de la recherche dichotomique, munie d'un début d'invariant de boucle et d'une assertion importante. Notez que l'on se donne deux éléments hypothétiques t[-1] et t[n], avec t[-1] < k ≤ t[n]).
  static boolean searchBis(int [] t, int k) {
    int low = -1 ;
    int high = t.length ;
// t[low] < k ≤ t[high]
    while (high-low > 1) {
      int m = (low+high)/2 ;
      if (t[m] < k) {
        low = m ;
      } else
        high = m ;
    }
// high = low+1 ∧ t[low] < k ≤ t[high]
    return high < t.length && t[high] == k ;
  }
  1. Où est l'optimisation ?
  2. Comment l'assertion finale garantit-elle la correction de la réponse.
  3. Revisiter l'argument de terminaison.
  4. Prouver franchement la correction en donnant les assertions.
Solution.

3  La fonction 91

La technique des assertions peut également s'employer pour les fonctions récursives. Les preuves de corrections fonctionnent en deux temps. Dans cet exercice on considère la fonction suivante.
  static int f(int x) {
    int r ;
    if (x > 100)
      r = x-10 ;
    else
      r = f(f(x+11)) ;
    return r ;
  }
Et on se propose de démontrer :
f(x) = if  x > 100  then  x-10  else 91
Que l'on note P(x,f(x)).
  1. Montrer la correction partielle, c'est-à-dire fermer le chemin entre les deux assertions suivantes.
      static int f(int x) {
            int r ;
    // ∀ x. P(x,f(x))
            if (x > 100) {
          r = x-10 ;
        }     else {
          r = f(f(x+11)) ;
        }
    // P(x,r)
            return r ;
      }
  2. Montrer la terminaison. Pour y arriver on utlisera l'ordre bizarre suivant, -∞ ≻ … ≻ 98 ≻ 99 ≻ 100 et tous les entiers strictement supérieurs à 100 sont incomparables entre eux mais ≺ aux entiers inférieurs ou égaux à 100. Sans en rajouter dans le formalisme, on peut considérer que la correction partielle est l'étape inductive d'une preuve. Il suffit maintenant de montrer que les appels (récursifs) s'exercent sur des arguments décroisssants selon ≺.
Solution.

Ce document a été traduit de LATEX par HEVEA et HACHA.