Discussion :

[james-mi]

Résumé des épisodes précédents :
dans un thread précédent sur la qualité en OCaml, nous avons écrit, comme tout un chacun lors de ses premiers pas en Caml, une fonction factorielle toute bête :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
# let rec factorial n = if n=0 then 1 else n * factorial (n - 1);;
val factorial : int -> int = <fun>
 
# factorial 5;;
- : int = 120

C'est court, c'est simple, ça fonctionne, on pourrait s'en satisfaire. Or si l'on creuse un peu, les choses se compliquent :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
# factorial 25;;
- : int = -71303168

pire (?) :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
# factorial 50;;
- : int = 0

et ne me parlez pas de :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
# factorial (-1);;
Stack overflow during evaluation (looping recursion?).

Bon, c'est alors que SpiceGuid nous propose :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
let rec factorial n =
    assert(n >= 0);
    match n with
    | 0 -> 1
    | m -> m * factorial (m - 1);;
val factorial : int -> int = <fun>

formidable, nous avons résolu le cas factorial (-1) qui renvoie maintenant :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
# factorial (-1);;
Exception: Assert_failure ("", 92, 4).

SpiceGuid, j'aime particulièrement cette approche que j'ai un (tout petit) peu expérimenté dans Eiffel via le Design by Contract, la voie royale pour la qualité dans les langages impératifs.

je voudrais bien maintenant éviter les problèmes que posent

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

factorial 25

comme ceci par exemple :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
let rec factorial n =
    assert(n >= 0);
    match n with
    | 0 -> 1
    | m -> let result = m * factorial (m - 1) in result;
    assert(result > 0);;

le compilateur rejette cela avec un grand mugissement dont la signification m'est, à cette heure tardive, inaccessible. Je suspecte une écriture trop "impérative" à son goût.

Pensons fonctionnel, toujours plus fonctionnel - après bien des tâtonnements :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
let rec factorial n =
    assert (n >= 0);
    match n with
    | 0 -> 1
    | m -> let result = m * factorial (m - 1)	 in
	 if result >0 	then result
			else assert false;;

me renvoie bien les "assertion failures" ad hoc.

Néanmoins le code n'est pas bien joli, en particulier j'aimerais tellement que l'assert de "sortie" soit aussi élégamment disposé que le premier...

Ahh, la beauté (empoisonnée) des "require" et "ensure" (* =assert *) d'Eiffel dans :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
11
12
13
   factorial: NUMBER is
      require
	 is_abstract_integer;
	 is_positive
      local
	 n: NUMBER;
      do
	 ...
      end;
      ensure
	 Result.is_abstract_integer;
	 Result.is_positive
      end;

Eiffel génère une signature de chaque fonction/procédure qui reprend les "require" et "ensure", ce qui est très précieux pour en documenter l'usage.

Quelqu'un a une idée pour rendre ce code joli dans le chameau ?

[Garulfo]

Le problème ici est simplement la taille d'un entier.
Implémente des entiers arbitrairement grand (avec des listes par exemple) et tu auras résolu ton problème (pas en performance)...

En Scheme ce problème ne se pose pas (celui des grands entiers). Celui de la performance est toujours là.

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
11
12
> (define (factoriel n)
    (define (f-aux n a)
      (if (< n 2)
          a
          (f-aux (- n 1) (* a n))
          )
      )
    (f-aux n 1)
    )
 
> (factoriel 25)
15511210043330985984000000

Le problème existe dans tout langage où les entiers sont bornés (donc quasiment tous)

[alex_pi]

Avant de vouloir résoudre le problème, est ce qu'au moins du comprends pourquoi tu te retrouves avec des résultats négatifs, puis nuls ?

[Invité]

de toute façon, tu pourras pas calculer factorielle de n au dela de 12 avec des entiers. Donc autant mettre dans la condition du début que n doit être compris entre 1 et 12.

Si tu veux calculer la factorielle de n pour des n plus grand que douze, il faut utiliser une autre structure de données que les entiers. J'en voit deux possibles : les chaînes de caractère (string) et les listes (char list).

La méthode est la même avec les deux solutions : il faut créer une fonction qui permette de multiplier deux nombres "longs" entre eux, en le faisant chiffre par chiffre, avec les retenues , ... etc, comme quand on fait la multiplication à la main. C'est cette fonction qui demande le plus de travail.

Ensuite tu peut faire une fonction qui transforme un entier en nombre "long", pour pouvoir utiliser ta fonction factorielle avec un entier en paramètre. Si tu as choisit d'utiliser les chaines de caractères, la fonction existe déjà : string_of_int.

Le résultat :
avec chaînes de caractères

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
# factorial 4 ;;
- : string = "24"

avec liste de caractères

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
# factorial 4 ;;
- : char list = ['2'; '4']

[gorgonite]

La méthode est la même avec les deux solutions : il faut créer une fonction qui permette de multiplier deux nombres "longs" entre eux, en le faisant chiffre par chiffre, avec les retenues , ... etc, comme quand on fait la multiplication à la main. C'est cette fonction qui demande le plus de travail.

on peut aussi se rappeler qu'un entier peut être considéré comme un polynome... et utiliser des algos type Hörner sur ces polynomes

[SpiceGuid]

Ta poscondition ne garanti même pas un résultat correct, par exemple:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
# factorial 31;;
- : int = 738197504

Dans le cas int -> int la bonne précondition est assert(0 <= n && n <= 12).

Autrement il faut généraliser à int -> Big_int.big_int :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
# #load "nums.cma";;
# let rec factorial n =
    assert (n >= 0);
    if n=0 then Big_int.unit_big_int
    else Big_int.mult_int_big_int n (factorial (n - 1));;
val factorial : int -> Big_int.big_int = <fun>
# Big_int.string_of_big_int (factorial 31);;
- : string = "8222838654177922817725562880000000"

Pour la performance il faut passer à la méthode dichotomique décrite au chapitre 45.

[Jedai]

Et si tu n'as pas envie (très raisonnablement) de réécrire l'ensemble des opérations arithmétique de base, tu peux te contenter d'utiliser big_int, de la librairie standard d'OCaml...

--
Jedaï

[LLB]

Quelqu'un a une idée pour rendre ce code joli dans le chameau ?

À partir des fonctions auxilliaires suivantes :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
11
let positive x = x >= 0
let (|>) x f = f x
 
let post_condition cond f x =
  let res = f x in
    assert (cond res);
    res
 
let pre_condition cond f x =
  assert (cond x);
  f x

Je te propose la fonction suivante (les préconditions et postconditions sont testées à chaque récursion) :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
let rec fact x =
  let fact' = function
    | 0 -> 1
    | m -> m * fact (m - 1)
  in
    (fact' |> post_condition positive |> pre_condition positive) x

(l'argument x sert à contourner une limitation de Caml)


Pour tes autres fonctions, si tu ne veux pas tester les conditions à chaque récursion, tu obtiens un code un peu plus lisible :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
let rec fact = function
  | 0 -> 1
  | m -> m * fact (m - 1)
 
let fact = fact
  |> post_condition positive
  |> pre_condition positive

La 2e définition s'appuie sur (et masque) la première. Tu peux ajouter autant de post/pré conditions que tu le souhaites, l'opérateur |> te permettant de chainer les fonctions de façon élégante.

[james-mi]

Merci à tous pour vos contributions variées et toutes éclairantes ...

Avant de vouloir résoudre le problème, est ce qu'au moins du comprends pourquoi tu te retrouves avec des résultats négatifs, puis nuls ?

J'ai de vagues et anciens souvenirs du codage des entiers sur quelques octets, avec perte d'info quand on dépasse les limites, mais une petite révision ne ferait pas de mal.
Quand à l'obtention des zéros, je suppose que c'est dû à un zéro obtenu une fois, qui se propage ensuite par la multiplication - les zéros de droite ci-dessous par exemple

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
 Big_int.string_of_big_int (factorial 50);;
- : string =
"30414093201713378043612608166064768844377641568960512000000000000"

de toute façon, tu pourras pas calculer factorielle de n au dela de 12 avec des entiers. Donc autant mettre dans la condition du début que n doit être compris entre 1 et 12.

oui c'est une solution mais dans la pré-condition je ne suis pas forcément sensé penser aux problèmes que je pourrais rencontrer (pour factorielle la limite n=12 est connue mais pour une autre fonction, je préfère traiter cela par les bonnes post-conditions, car je peux ne pas penser aux pré-conditions appropriées).
L'idée ici est de trouver la bonne post-condition, qui va me garantir un résultat juste quelle que soit l'implémentation ...

Ta poscondition ne garanti même pas un résultat correct, par exemple:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
# factorial 31;;
- : int = 738197504

Oui, effectivement ma post-condition est très insuffisante - j'ai cherché miux mais ce n'est pas gagné :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
let nnn = fac n and nn = fac (n-1) in (
	(abs (nnn) = n * nn)
	&& (nnn>0) && (nn>0)&&(nnn>nn))

est nettement mieux mais n'est pas suffisant pour garantir tous les résultats.

À partir des fonctions auxilliaires suivantes :

LLB , j'aime beaucoup cette approche qui est centrée sur des pré et post-conditions explicites, "autonomes" et intelligibles, par contre je ne comprends pas bien comment cela fonctionne, en particulier :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
let (|>) x f = f x;;
val ( |> ) : 'a -> ('a -> 'b) -> 'b = <fun>

c'est (encore) un peu du chinois pour moi

de même que la dernière ligne ici :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
let rec fact x =
  let fact' = function
    | 0 -> 1
    | m -> m * fact (m - 1)
  in
    (fact' |> post_condition positive |> pre_condition positive) x

Pour tes autres fonctions, si tu ne veux pas tester les conditions à chaque récursion, tu obtiens un code un peu plus lisible :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
let rec fact = function
  | 0 -> 1
  | m -> m * fact (m - 1)
 
let fact = fact
  |> post_condition positive
  |> pre_condition positive

La 2e définition s'appuie sur (et masque) la première. Tu peux ajouter autant de post/pré conditions que tu le souhaites, l'opérateur |> te permettant de chainer les fonctions de façon élégante.

C'est beaucoup plus lisible, c'est une approche que je trouve excellente, et je trouve ce degré d'abstraction fascinant, j'ai hâte de le maîtriser ... Je suis preneur de toute explication ...

[LLB]

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

let (|>) x f = f x

C'est un opérateur qui sert juste à modifier la notation. Si on écrit :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
-4 |> abs
est équivalent à
abs (-4)
 
[1; 4; -4; -1; 5] |> List.map succ |> List.filter positive
est équivalent à
List.filter positive (List.map succ [1; 4; -4; -1; 5])

Les fonctions sont alors écrites dans l'ordre dans lequel elles sont appliquées (ici : map, puis filter). On peut ajouter à la suite du code autant de fonctions que l'on souhaite, on voit mieux comment les fonctions sont chainées, je trouve.

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

(fact' |> post_condition positive |> pre_condition positive) x

fact' est la fonction factorielle. Cette fonction est donnée en argument à la fonction précondition (qui ajoute une précondition et renvoie la nouvelle fonction). Le résultat est ensuite envoyé à la fonction pre_condition. La fonction renvoyée est alors appliquée avec x en argument.

L'opérateur |> n'a pas de sens en lui-même, il sert juste à changer la syntaxe. Cet opérateur est défini dans la bibliothèque standard de F#. Tu peux trouver quelques explications dans ce cours et sur le forum. Il y a quelques autres opérateurs utiles qui sont présentés.

C'est beaucoup plus lisible, c'est une approche que je trouve excellente, et je trouve ce degré d'abstraction fascinant, j'ai hâte de le maîtriser ... Je suis preneur de toute explication ...

Ca fait partie de la notion d'applications d'ordre supérieur. C'est l'un des fondements de la programmation fonctionnelle, ça permet de factoriser beaucoup de code et "jouer" avec les fonctions.

[LLB]

Et si tu souhaites avoir tes conditions au début de ton code, voici une autre suggestion :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
let (^<) f x = f x
 
let plus2 =
  pre_condition positive  ^<
  post_condition positive ^<
  fun x ->
    x + 2

2 remarques : l'opérateur ^< est défini de la même façon que l'opérateur <| indiqué dans les liens que j'ai donnés... à une différence importante. Il est associatif à droite. C'est ce que l'on veut ici (on a alors des appels de fonctions imbriqués), c'est ce que l'on a dans Haskell (il me semble, avec $). Dans F#, il est possible que <| devienne associatif à droite par la suite. Actuellement, dans Caml (et F#), l'associativité d'un opérateur dépend de son premier caractère. Ce qui oblige à faire une bidouille ici (je ne trouve pas que ^< soit très joli).

De plus, une limitation de Caml interdit la fonction ci-dessus d'être récursive.

Tu pourrais donc définir ta fonction factorielle de la façon suivante (là encore, les conditions ne sont pas testées à chaque récursion) :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
let fact =
  pre_condition positive  ^<
  post_condition positive ^<
  let rec fact' = function
    | 0 -> 1
    | n -> n * fact' (n - 1)
  in fact'

Enfin, il y a une dernière limitation à tous les codes que j'ai présentés ici : les fonctions ne doivent avoir qu'un seul argument (utilise des tuples si tu veux plusieurs valeurs).

[SpiceGuid]

L'idée ici est de trouver la bonne post-condition, qui va me garantir un résultat juste quelle que soit l'implémentation ...

J'ai un exemplaire de Eiffel: le langage 2nd édition et je dois dire que ta vision de la programmation par contrat n'est pas tout à fait la mienne.
Ce qui garanti la justesse du résultat c'est le respect de la précondition.
La postcondition n'a que valeur de documentation, elle renseigne sur quelques propriétés pertinentes de l'implémentation, elle n'a pas pour but de prouver que le résultat est correct.
Du moins c'était la position de Bertrand Meyer à l'époque du langage Eiffel dans sa version 3. Aujourd'hui Bertrand Meyer a fait évoluer son discours vers la notion de complete contracts, selon lui les contrats devraient couvrir la totalité des spécifications. Malheureusement, 3 ans après la standardisation Eiffel ECMA:

• aucun compilateur, pas même celui de Effeil-software, n'implémente ce langage
• SmartEiffel est le seul compilateur open-source et d'après Dominique Colnet il n'implémentera jamais Eiffel ECMA
• le Calcul des Constructions Inductives (une approche fonctionnelle des preuves) est déjà capable de vérifier les spécifications à la compilation tandis qu'un éventuel Eiffel ECMA court toujours après la vérification à l'éxécution

Rien dans tout cela ne me conforte dans l'idée que la postcondition devrait être un complete contract.

[gasche]

Sans définirs des opérateurs dans tous les sens (code équivalent, mais plus compréhensible à première vue) :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
11
let entree_positive fonction = fun x -> assert (x >= 0); fonction x
 
let sortie_positive fonction =
   fun x ->
     let resultat = fonction x in
     assert (resultat > 0);
     resultat
 
let rec fac = function 0 -> 1 | n -> n * fac (n -1)
 
let fac = sortie_positive (entree_positive fac)

Pour régler le problème du "Stack overflow" :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
let fac n =
  let rec fac accu = function
  | 0 -> accu
  | n -> fac (accu * n) (n - 1) in
  fac 1 n

Remarques de style : la fonction locale a le même nom que la fonction globale, ça ne pose pas de problème mais tu peux en choisir un autre comme fac' ou aux_fac par exemple. Tu peux aussi déclarer deux fonctions globales, la deuxième recouvrant la première, comme on fait dans le code de vérification, mais je préfère cette méthode.


Ceci dit, je pense que généralement, la simplicité est bien plus importante que les performances (ou même les vérifications paranoïaques) : si je ne connais pas le contexte d'utilisation, je coderai certainement fac comme ceci :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
let rec fac = function
| 0 -> 1
| n -> n * fac (n - 1)

Si après avoir écrit cette première version (simple et lisible) tu te rends compte que tu utilises ta fonction dans un contexte spécifique (par exemple avec des contraintes de sécurité fortes, ou de performance (même si pour fac ça ne joue pas parce que le dépassement d'entiers pose problème avant le stack overflow)), tu pourras toujours la recoder pour répondre mieux à tes besoins.
Mais globalement, sur l'ensemble de ton code, seule une petite partie sera utilisée dans un contexte sensible, et il serait inutile de tout coder directement de manière compliquée si ça n'est justifié que pour un dixième du code.

Globalement, je te conseille de faire en premier lieu la version la plus simple et claire; si tu as des contraintes supplémentaires (tu ne pourras t'en rendre compte qu'un peu plus tard dans la conception, généralement), tu pourras toujours revenir dessus.

[Jedai]

Pour régler le problème du "Stack overflow"

Quel problème du "Stack overflow" ? Celui qui intervient lorsqu'on veut calculer "fac 100000000" ? Si on le fait avec des int le résultat serait de toute façon faux et si on le fait avec des big_int, on a intérêt à avoir prévu autre chose à faire pendant les quelques jour que la machine mettra pour calculer le résultat de toute façon...

Si on a peur du Stack overflow pour une fonction comme fac, on peut tout de suite abandonner les fonctions récursives !!

--
Jedaï

[gasche]

Certes, mais la tail-rec reste intéressante dans l'absolu (même si comme tu l'as dit ici elle est assez inutile, et même si je trouve que les gens sont trop obsédés par ça en général).

Sinon, plus généralement (c'est à dire pas spécialement sur fac) il me semble qu'avant de passer à Big_int (qui comme tout le monde l'a dit est assez lent), ça vaut le coup de se demander si des types intermédiaires ne rentrent pas. En général (c'est à dire si on veut des types plus grands que Int, mais pas arbitrairement grands non plus), des types comme float ou Int64 permettent d'agrandir pas mal la fenêtre de valeurs accessibles, avec un coup en performances minime.
Avec des floats, fac 170 passe comme un charme (et sans perte de précision à priori).

Ceci dit, il est un peu chiant de devoir convertir toutes ses opérations numériques à chaque fois qu'on veut changer de représentation. Avant que le Malin vienne faire de la propagande pour son langage patent-encumbered avec surcharge d'opérateurs, je prend l'initiative de mentionner mon module Numeric ( implémentation, interface), qui propose une interface (et une syntaxe) plus ou moins unifiée pour les différents types numériques.

[Jedai]

Certes, mais la tail-rec reste intéressante dans l'absolu (même si comme tu l'as dit ici elle est assez inutile, et même si je trouve que les gens sont trop obsédés par ça en général).

Dans cette optique, j'approuve pleinement.

Avec des floats, fac 170 passe comme un charme (et sans perte de précision à priori).

Qu'est ce que tu appelles "perte de précision" ? Parce que fac 170 a 307 chiffres significatifs et en double on n'en récupère que 16 dans la mantisse.

Ceci dit, il est un peu chiant de devoir convertir toutes ses opérations numériques à chaque fois qu'on veut changer de représentation. Avant que le Malin vienne faire de la propagande pour son langage patent-encumbered avec surcharge d'opérateurs, je prend l'initiative de mentionner mon module Numeric ( implémentation, interface), qui propose une interface (et une syntaxe) plus ou moins unifiée pour les différents types numériques.

Je suppose que tu fais allusion à F# ? Néanmoins Haskell est 100% pur sucre libre et patent-free et propose de la surcharge d'opérateur depuis bien longtemps, avec un mécanisme fort intéressant (typeclass).
Ton module est intéressant, néanmoins il ne permet pas de facilement mélanger les différents types numériques (il est fréquent qu'on ait besoin de manipuler des entiers et des flottants dans le même module) et ses opérations cachent les opérations standards sur les flottants. Théoriquement intéressant, mais pas très pratique. Enfin c'est mieux que rien.

--
Jedaï

[Jedai]

Int64 commence à donner des résultat incorrect à partir de 21! .
Int à partir de 13! .
On ne gagne donc que 8 résultats corrects.
Le problème c'est que la factorielle monte vraiment très vite. Après il faut voir à quoi on la destine, il est fort probable qu'une application donnée n'ait besoin que d'une factorielle dans un domaine très restreint, ou d'une propriété très particulière de la factorielle...

--
Jedaï

[gasche]

Néanmoins Haskell est 100% pur sucre libre et patent-free et propose de la surcharge d'opérateur depuis bien longtemps, avec un mécanisme fort intéressant (typeclass).

Certes, mais ça a ses inconvénients aussi (bonjour les messages d'erreur !) et fondamentalement ça me paraît un peu louche de passer de OCaml à Haskell (ou l'inverse) pour des raisons de calcul numérique (vu que clairement c'est pas l'application qui met le plus en valeur les qualités d'aucun des deux langages).

[Jedai]

Certes, mais ça a ses inconvénients aussi (bonjour les messages d'erreur !)

Les messages d'erreurs sont certes un peu durs pour les débutants, mais à part dans des cas d'extrême "Typeclass hackery" ils ne posent pas vraiment de problèmes pour un programmeur habitué.

et fondamentalement ça me paraît un peu louche de passer de OCaml à Haskell (ou l'inverse) pour des raisons de calcul numérique (vu que clairement c'est pas l'application qui met le plus en valeur les qualités d'aucun des deux langages).

Certes, néanmoins la surcharge d'opérateur et de fonctions et les typeclass sont utiles dans tous les domaines, la classe de type Num n'est qu'un exemple particulièrement évident (et tout de même pratique, finalement il est assez courant de manipuler des nombres dans une application à un moment ou à un autre, même si ce n'est pas le but principal du programme).

--
Jedaï

[alex_pi]

J'ai un exemplaire de Eiffel: le langage 2nd édition et je dois dire que ta vision de la programmation par contrat n'est pas tout à fait la mienne.
Ce qui garanti la justesse du résultat c'est le respect de la précondition.
La postcondition n'a que valeur de documentation, elle renseigne sur quelques propriétés pertinentes de l'implémentation, elle n'a pas pour but de prouver que le résultat est correct.
[...]
Rien dans tout cela ne me conforte dans l'idée que la postcondition devrait être un complete contract.

En programmation par contrat, la post-condition a bien vocation a prouver que le programme est correcte, puisque c'est la post-condition qui exprime ce que l'on entend par "correction" du programme ! Simplement, dans un monde parfait, on prouve statiquement (à la compilation ou avant, mais en tout cas avant exécution) que la précondition implique la post-condition, et qu'à l'exécution, on n'a à vérifier que la précondition pour s'assurer du bon fonctionnement de la fonction. Dans un vision encore plus globale, on vérifie statiquement que les préconditions sont vérifiées avant appel de chaque fonction et on se sert de leur post-condition pour prouver la correction de la fonction appelante. Ceci n'est bien sûr pas possible dans le cas d'un usage intéractif.

• ...
• le Calcul des Constructions Inductives (une approche fonctionnelle des preuves) est déjà capable de vérifier les spécifications à la compilation tandis qu'un éventuel Eiffel ECMA court toujours après la vérification à l'éxécution

Après, c'est toujours pareil... Il faut faire un choix entre expressivité et utilisabilité. Autant annoter son code avec des pré et post conditions et quelques invariants de boucle, on peut espérer qu'un jour les programmeurs le feront, autant faire des preuves dans le CCI, il ne faut pas se leurer, seul un petit nombre de cinglés joueront avec ça ! Mais il y a toujours une volonté des cinglés en question de travailler sur des outils prouvant statiquement les codes annotés par des gens "normaux" (quitte à prouver la validité de ces outils en Coq justement), donc tout n'est pas perdu :-)