Langages fortement typés

Pour le besoin de notre discussion OCaml fera très bien l'affaire comme représentant des langages fortement typés.

Après avoir lancé la commande en ligne ocaml on entre ce code dans la console :

type interval = Interval of int * int;;

On peut alors créer des intervalles d'entiers comme l'intervalle [1,2] ou l'intervalle [0,9] :

# Interval(1,2);;
- : interval = Interval (1, 2)
# Interval(0,9);;
- : interval = Interval (0, 9)

Cependant on peut tout aussi bien créer des intervalles invalides comme [2,1] :

# Interval(2,1);;
- : interval = Interval (2, 1)

Et ocaml les accepte comme des intervalles valides !

Alors que faire ?

Programmation par contrat

Il existe une solution que l'on appelle la programmation par contrat et qui consiste à cacher l'implémentation du type interval et à lui associer un constructeur make qui vérifie la validité des paramètres fournis.

module Interval :
sig (* interface *)
  type interval
  val  make : int -> int -> interval
end 
  =
struct (* implémentation *)
  type interval =
    Interval of int * int
  let make a b =  (* constructeur *)
    assert(a<b);  (* assertion *)
    Interval(a,b) (* résultat *)
end;;

On créé l'intervalle [1,2] à l'aide de Interval.make 1 2
Par contre si on créé Interval.make 2 1 on a une erreur à l'exécution :

Exception: Assert_failure ("", 11, 4)
(* 11 et 4 indiquent la ligne et la colonne où l'erreur s'est produite *)

Avantage : le programme ne construit pas d'intervalle invalide.

Inconvénient : l'erreur n'est pas détectée à la compilation.

Maintenant discutons cet avantage. Certes le programme ne commet pas l'erreur de construire un intervalle invalide. Néanmoins le programme produit tout de même une erreur qui s'avère tout aussi fatale. Car il est trop tard pour corriger cette erreur. Il n'y a aucune contre-mesure possible. Vous pouvez toujours remplir un rapport d'erreur cela n'empêchera pas le programme de mal s'exécuter tant que l'erreur ne sera pas corrigée par le programmeur. Car c'est lui le responsable de l'erreur, pas l'utilisateur.

La programmation par contrat ressemble plus à un mécanisme de signalement qu'un à mécanisme de prévention. Pour faire de la prévention le seul bon moment c'est à la compilation. À l'exécution on ne peut plus ni agir ni réagir. À l'exécution il est trop tard.

Un jour un programmeur m'a dit

Un jour pas si lointain, un programmeur expérimenté m'a dit :

Citation :

Hé bien justement ...

Types dépendants

Les types dépendants proposent une approche radicalement différente.

Pour le besoin de notre discussion Coq fera très bien l'affaire comme représentant des langages à types dépendants.

Après avoir lancé la commande en ligne coqtop on entre ce code dans la console :

Inductive interval : nat -> nat -> Prop :=
Interval : forall min max, min < max -> interval min max.

À présent essayons de créer l'intervalle [1,2] :

Coq < Eval compute in Interval 1 2.
     = Interval 1 2
     : 1 < 2 -> interval 1 2

Ce que coq nous dit c'est que Interval 1 2 n'est pas un intervalle mais une fonction du type 1 < 2 vers le type interval 1 2 . Quel est donc ce mystérieux type 1 < 2 ? C'est le type d'une preuve que 1 est < que 2 . C'est le type du paramètre manquant pour la construction pleine et entière d'un intervalle [1,2] valide.
Pour fabriquer cette preuve nous chargeons les capacités arithmétiques de base avec Require Import Arith.Arith_base.

À présent nous disposons de lt_n_Sn , c'est une preuve qu'un entier n est plus petit que son successeur S n .
Nous allons utiliser cet argument à bon escient car 2 est le successeur de 1 . Il s'ensuit que lt_n_Sn 1 est de type 1 < 2 .
Nous pouvons maintenant construire l'intervalle [1,2] :

Coq < Eval compute in Interval 1 2 (lt_n_Sn 1).
     = Interval 1 2 (lt_n_Sn 1)
     : interval 1 2

Cette fois le résultat est bien du type interval .   
Toutefois notre situation est encore précaire, par exemple comment construire [0,9] alors que 9 n'est pas le successeur de 0 ?

Hé bien nous disposons de lt_0_Sn qui est une preuve que 0 est < qu'un successeur quelconque. Or 9 est le successeur de 8. Il s'ensuit que lt_0_Sn 8 est de type 0 < 9 .

Coq < Eval compute in Interval 0 9 (lt_0_Sn 8).
     = Interval 0 9 (lt_0_Sn 8)
     : interval 0 9

Il reste un dernier cas, le cas général, où la borne inférieure n'est pas zéro et où la borne supérieure n'est pas son successeur.

Par exemple [1,9]. Cette fois nous allons devoir faire la preuve à la main.

Commençons par l'énoncer comme un fait lt_1_9 :

Coq < Fact lt_1_9 : 1 < 9.             

Coq entre alors en proof mode , il veut bien accepter ce fait si vous lui en fournissez une démonstration. Ce passage de coq en  proof mode est visible dans l'invite : elle passe de Coq < à lt_1_9 < .

Fournissez-lui l'argumentaire repeat constructor.
Puis affirmez Qed. ( Quod Erat Demonstrandum ) pour quitter le proof mode .

Coq < Fact lt_1_9 : 1 < 9.
1 subgoal

  ============================
   1 < 9

lt_1_9 < repeat constructor.
Proof completed.

lt_1_9 < Qed.
repeat constructor.

lt_1_9 is defined

Coq < Eval compute in Interval 1 9 lt_1_9.
     = Interval 1 9 lt_1_9
     : interval 1 9

Petit théorème

Jusqu'à présent on a utilisé que des intervalles à bornes constantes.

Bien entendu les intervalles peuvent aussi avoir des bornes variables.

Pour l'illustrer on va démontrer un tout petit théorème qui dit dire que b est strictement borné par a et c est équivalent à affirmer l'existence de 3 intervalles [ a,b ] [ b,c ] et [ a,c ].

On va appeler ce petit théorème bounded_iff_intervals :

Theorem bounded_iff_intervals :
  forall a b c, a < b < c <-> interval a b /\ interval b c /\ interval a c.

Puis, pour le prouver, on utilise les 5 tactiques qui suivent :

split qui décompose 1 but a ⇔ b en 2 buts a ⇒ b et a ⇐ b , 1 but a < b < c en 2 buts a < b et b < c ou encore 1 but a ⋀ b en 2 buts a et b .

intro H qui transforme la condition d'un but en une hypothèse H .

destruct H qui décompose une hypothèse H .

apply A qui fait valoir un argumentaire A .

exact H qui fait valoir une hypothèse H .

Proof.
  split.
  (* -> *)
  intro H.
  destruct H as (Hab,Hbc).
  split.
  apply (Interval a b Hab).
  split.
  apply (Interval b c Hbc).
  apply (Interval a c (lt_trans a b c Hab Hbc)).
  (* <- *)
  intro H.
  destruct H as (Hab,(Hbc,Hac)).
  split.
  destruct Hab. exact H.
  destruct Hbc. exact H.
Qed.

Commandes

Comme tout logiciel console, coqtop possède son lot de commandes purement utilitaires.

Les commandes en proof mode :

Restart. Reprendre la preuve à son début.

Undo. Défaire la dernière tactique.

Abort All. Abandonner la preuve et quitter le proof mode .

Les commandes top level :

Quit. Quitter coqtop.

Reset Initial. Réinitialiser coqtop.

Check expr . Affiche le type de l'expression.

Sous GTK2+ coqtop est accompagné de l'environnement graphique Coq IDE.

Récapitulatif du code

Inductive interval : nat -> nat -> Prop :=
Interval : forall min max, min < max -> interval min max.

Require Import Arith.Arith_base.

Eval compute in Interval 1 2 (lt_n_Sn 1).
Eval compute in Interval 0 9 (lt_0_Sn 8).

Fact lt_1_9 : 1 < 9.
  repeat constructor.
Qed.

Eval compute in Interval 1 9 lt_1_9.

Theorem bounded_iff_intervals :
  forall a b c, a < b < c <-> interval a b /\ interval b c /\ interval a c.
Proof.
  split.
  (* -> *)
  intro H.
  destruct H as (Hab,Hbc).
  split.
  apply (Interval a b Hab).
  split.
  apply (Interval b c Hbc).
  apply (Interval a c (lt_trans a b c Hab Hbc)).
  (* <- *)
  intro H.
  destruct H as (Hab,(Hbc,Hac)).
  split.
  destruct Hab. exact H.
  destruct Hbc. exact H.
Qed. 

Pour aller plus loin

Le site officiel .

Le manuel de référence .

La librairie standard .

Le calcul des séquents .

Les types dépendants .