Le -1 de C contre le option d'OCaml

(* indice_de t v renvoie Some i, ou i est le PLUS PETIT indice tel que
   t.(i) = v, et None si v ne figure pas dans t.
   Precondition  : aucune (le tableau vide est admis).
   Postcondition : si le resultat est Some i, alors 0 <= i < Array.length t
                   et t.(i) = v et v n'est dans aucun t.(k) pour k < i. *)
let indice_de t v =
  let n = Array.length t in
  let i = ref 0 in
  (* INVARIANT : v ne figure dans aucun des t.(0) .. t.(!i - 1),
     et 0 <= !i <= n.       VARIANT : n - !i. *)
  while !i < n && t.(!i) <> v do incr i done;
  if !i = n then None else Some !i

Le compilateur infère val indice_de : 'a array -> 'a -> int option : la fonction sert pour n'importe quel type d'éléments, sans une ligne de plus.

Terminaison. Variant $V=n-i$ : entier, positif tant que la condition tient, et décroissant strictement de $1$ à chaque tour. La boucle fait au plus $n$ tours.

Correction. Initialisation : $i=0$, la tranche $t.(0)\dots t.(-1)$ est vide, l'invariant est vrai. Conservation : on n'incrémente $i$ que si t.(!i) <> v, donc la tranche s'agrandit d'une case qui ne contient pas $v$. Utilisation : à la sortie, ou bien $i=n$ et l'invariant dit que $v$ est absent de tout le tableau — on rend None —, ou bien $t.(i)=v$ et l'invariant dit qu'aucun indice plus petit ne convient — c'est bien la première occurrence.

Complexité. $\Theta (n)$ comparaisons dans le pire cas (valeur absente), $\Theta (1)$ dans le meilleur, $\Theta (1)$ en espace.

L'ordre du && n'est pas décoratif. La condition s'écrit !i < n && t.(!i) <> v et pas l'inverse. Mesuré sur t = [| 1; 2; 3 |] et i = 3 :

if i < Array.length t && t.(i) = 0 -> "non", aucun acces
if t.(i) = 0 && i < Array.length t -> Invalid_argument "index out of bounds"

C'est exactement l'exercice 1.3 — la garde vient en premier —, à ceci près qu'ici l'accès fautif lève une exception au lieu de lire en silence une mémoire étrangère. Le défaut est le même ; sa punition est immédiate.

Et le type dit le contrat. La version C rendait $-1$, valeur qu'aucune signature ne distingue d'un indice et que rien n'oblige à tester. int option force l'appelant à décomposer par un filtrage, donc à traiter le cas d'absence. Le chapitre chap:discipline en fait une règle de spécification.