TD n°3 — corrigé

Exercice 1

In [1]:
let incr x =
  x := !x + 1
;;
Out[1]:
val incr : int ref -> unit = <fun>
In [2]:
let decr x =
  x := !x - 1
;;
Out[2]:
val decr : int ref -> unit = <fun>

Exercice 2

In [3]:
let vect_length = Array.length  (* En Ocaml `vect` se dit `array `*)
Out[3]:
val vect_length : 'a array -> int = <fun>
In [4]:
let f1 x =
  let y = !x + 1 in
  y
;;
Out[4]:
val f1 : int ref -> int = <fun>
In [5]:
let f2 x y =
  for i = x to 10 do
    y := x :: !y
  done;
  !y
;;
Out[5]:
val f2 : int -> int list ref -> int list = <fun>

Mais vous n'avez pas le droit d'utiliser de références de listes sauf indication contraire.

In [6]:
let e3 = if true then "Hello !\n";;
Out[6]:
File "[6]", line 1, characters 22-33:
Error: This expression has type string but an expression was expected of type
         unit
Characters 22-33:
  let e3 = if true then "Hello !\n";;
                        ^^^^^^^^^^^
In [7]:
(* Équivalent à *)
let e3 = if true then "Hello !\n" else ();;
(* D'où le problème de type, explicite dans le message d'erreur *)
Out[7]:
File "[7]", line 2, characters 39-41:
Error: This expression has type unit but an expression was expected of type
         string
Characters 60-62:
  let e3 = if true then "Hello !\n" else ();;
                                         ^^
In [8]:
let e4 = if true then print_string "Bye...\n";;

Bye...
Out[8]:
val e4 : unit = ()
In [9]:
let e5 =
  let x = ref 10;  (* erreur ici *)
  while !x > 0 do
    print_int !x;
    print_char ' ';
    decr x
  done
;;
Out[9]:
File "[9]", line 8, characters 0-2:
Error: Syntax error
Characters 119-121:
  ;;
  ^^
In [10]:
let e5 =
  let x = ref 10 in
  while !x > 0 do
    print_int !x;
    print_char ' ';
    decr x
  done
;;

10 9 8 7 6 5 4 3 2 1
Out[10]:
val e5 : unit = ()
In [11]:
let e6 = let x = ref 0 in let y = x in x := !x + 1; y;;
Out[11]:
val e6 : int ref = {contents = 1}
In [12]:
let f7 x y =
  if !x > 0 then
    decr x;
    y := !y + !x
  else
    incr x
;;
Out[12]:
File "[12]", line 5, characters 2-6:
Error: Syntax error
Characters 61-65:
    else
    ^^^^
In [13]:
(* Équivalent à *)
let f7 x y =
  if !x > 0 then decr x else ();
  y := !y + !x
  else  (* Erreur de syntaxe, que vient faire ce else ?)
    incr x
;;
Out[13]:
File "[13]", line 5, characters 2-6:
Error: Syntax error
Characters 84-88:
    else  (* Erreur de syntaxe, que vient faire ce else ?)
    ^^^^
In [14]:
(* Il faut parenthéser pour avoir une version correcte *)
let f7 x y =
  if !x > 0 then begin
    decr x;
    y := !y + !x
  end else
    incr x
;;
Out[14]:
val f7 : int ref -> int ref -> unit = <fun>
In [15]:
let foo = ref succ;;
Out[15]:
val foo : (int -> int) ref = {contents = <fun>}
In [16]:
let bar x = !foo x;;
Out[16]:
val bar : int -> int = <fun>
In [17]:
bar 2;;
Out[17]:
- : int = 3
In [18]:
foo := function x -> x + 2;;
Out[18]:
- : unit = ()
In [19]:
bar 2;;
Out[19]:
- : int = 4
In [20]:
let p = ref 0 in let q = ref p in !(!q) + begin p := 2; !(!q) end;;
Out[20]:
- : int = 4

Comportement non spécifié ! Ici le membre de droite du + a été évalué en premier, mais il aurait pû en être autrement (ce n'est pas dans la norme et cela peut dépendre de la machine ou d'une implémentation particulière). Moralité : ne jamais faire cela. Utiliser des let in pour forcer l'ordre.

In [21]:
let clock = ref 0;;
Out[21]:
val clock : int ref = {contents = 0}
In [22]:
let time () = incr clock; !clock;;
Out[22]:
val time : unit -> int = <fun>
In [23]:
time ();;
Out[23]:
- : int = 1
In [24]:
time () + time ();;
Out[24]:
- : int = 5
In [25]:
(* Comportement non spécifié ! *)
time () - time ();;
Out[25]:
- : int = 1

Exercice 3

In [26]:
let puissance x n =
  let res = ref 1 in
  for k = 1 to n do
    res := x * !res
  done;
  !res
;;
Out[26]:
val puissance : int -> int -> int = <fun>

Il n'y a aucun problème de terminaison. La boucle s'effectue $n$ fois sur un $\Theta(1)$, le reste est en $\Theta(1)$ donc la complexité est linéaire en $n$. Un invariant de boucle est l'égalité entre le contenu de res et $x^{k - 1}$. Montrons que ceci est bien un invariant et qu'il permet bien de justifier la correction de la fonction :

  • Initialisation : Il faut se placer juste avant le début de la boucle for, c'est-à-dire juste après l'initialisation de $k$ qui vaut donc $1$ et juste avant le test qui vérifie si $k$ dépasse $n$. À ce moment là res a pour contenu $1$ qui est bien égal à $x ^ {1 - 1} = x^0 = 1$.

  • Transmission : On suppose que l'invariant est vérifié au début de la boucle (pour un certain $k$) et il faut montrer que c'est encore le cas au début de la boucle suivante (donc juste après l'incrémentation de $k$, c'est-à-dire pour $k + 1$). Au début de la boucle, le contenu de res est donc $x^{k - 1}$. La boucle est constituée d'une seule instruction qui multiplie le contenu de res par $x$. À la fin de la boucle suivant res a donc pour valeur $x^{k - 1} \times x = x^k = x^{(k + 1) - 1}$. Au début de la boucle suivante, l'invariant est donc bien vérifié.

  • Terminaison : la boucle s'arrête lorsque $k$ dépasse $n$, c'est-à-dire lorsque $k = n + 1$. En sortie de boucle on a donc le contenu de res qui vaut $x ^ {(n + 1) - 1} = x^n$, ce qui est bien le résultat attendu.

Exercice 4

In [27]:
let somme_elements tableau =
  let n = vect_length tableau in
  let somme = ref 0 in
  for i = 0 to n - 1 do
    somme := !somme + tableau.(i)
  done;
  !somme
;;
Out[27]:
val somme_elements : int array -> int = <fun>
In [28]:
somme_elements [|1; 2; 3; 1; -6|];;
Out[28]:
- : int = 1

Pour produit_elements il suffit de remplacer le + par un *.

Exercice 5

In [29]:
let appartient tableau element =
  let n = vect_length tableau in
  let trouve = ref false in
  let i = ref 0 in
  while (not !trouve) && (!i < n) do
    trouve := !trouve || (tableau.(!i) = element);
    incr i
  done;
  !trouve
;;
Out[29]:
val appartient : 'a array -> 'a -> bool = <fun>
In [30]:
appartient [|2; 1; 4; 2; 3|] 3;;
Out[30]:
- : bool = true

Lors de chaque passage dans la boucle, la valeur de i — qui commence à 0 — est incrémentée de 1 ce qui garanti que la condition d'arrêt est atteinte après au plus $n$ passages. Ceci montre que la fonction termine et que sa complexité au pire est en $\Theta(n)$ où $n$ est la taille du tableau puisque tout est en $\Theta(1)$.

Un invariant permettant de prouver la correction : $trouve = element \in tableau[0..i[$. Pour l'initialisation, il est certain que l'élément ne se trouve pas dans le sous-tableau vide $tableau[0,0[$ et $trouve$ est bien faux. La transmission ne pose pas de problème puisque le corps de la boucle revient exactement à affecter à $trouve$ le booléen $element \in tableau[0..i[$ ou $element = tableau[i]$, c'est-à-dire $element \in tableau[0..i + 1[$, suivi d'une incrémentation de $i$, ce qui conserve donc l'invariant. Pour la terminaison, deux conditions de sorties sont possibles. Soit trouvé est vrai et alors l'élement se situe dans un sous-tableau $tableau[0, i[$ et donc a fortiori dans le tableau (car $i \leq n$), soit trouvé est faux et alors $i = n$, dans ce cas l'invariant justifie que $element \not\in tableau[0..n[$. Ce qui prouve bien ce que l'on souhaite.

Exercice 6

Voir DM n°2.

Exercice 7

Voir DM n°2.