Bonjour,
dans la discussion précédente, vous avez été nombreux à m'aider dans ma recherche la fonction factorielle parfaite - pour comprendre
cette discussion avait dérivé, à ma plus grande satisfaction, vers le sujet du "Design by Contract" - c'est une manière de programmer que j'aime. Certains d'entre vous m'ont fait d'excellentes suggestions, et je les en remercie.
J'ai voulu creuser le sujet, à la fois pour débuter dans OCaml et pour m'ouvrir la possibilité de l'utiliser.
Les approches proposées ont les caractéristiques suivantes :
1- ne fonctionnent que sur les fonction à un seul argument
2-les préconditions proposées sont toutes des fonctions de f et de x, alors que dans l'absolu une précondition n'a pas besoin de prendre f en paramètre, seulement x
exemple :
- or je voudrais éviter d'envoyer f à ma précondition, ce n'est pas vraiment gênant, mais par principe ...
Code : Sélectionner tout - Visualiser dans une fenêtre à part
1
2
3 let pre_condition cond f x = assert (cond x); f x
3-le nommage des pré et postconditions se fait dans la déclaration de la dite précondition, et n'est donc plus accessible pour le programme, qui ne peut pas renvoyer son nom lors d'un échec.
exemple :
-je me demande comment renvoyer quelque chose comme "failed condition "positive""...
Code : Sélectionner tout - Visualiser dans une fenêtre à part let positive x = x >= 0
J'ai donc tenté une autre approche. Elle fonctionne en partie :
et pour l'appliquer :
Code : Sélectionner tout - Visualiser dans une fenêtre à part
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20 type 'a precondition = { rname : string ; rcond : 'a -> bool } (* rname = name of *r*equire condition *) type ('a, 'b) postcondition = { ename : string ; econd : 'a -> 'b -> bool } (* ename = name of *e*nsure condition *) let rec preconds_fold = function | [], _, bool -> bool | _, _, false -> false | h::t, x, true -> preconds_fold (t, x, h.rcond x) let rec postconds_fold = function | [], _, _, bool -> bool | _, _, _, false -> false | h::t, res, x, true -> postconds_fold (t, res, x, h.econd res x) let add_DBC f preconds postconds = fun x -> assert (preconds_fold (preconds, x, true)) ; let res = f x in assert (postconds_assert (postconds, res, x, true)) ; res
comme je l'ai dit cela fonctionne sur fact, mais je ne suis pas allé beaucoup plus loin pour l'instant.
Code : Sélectionner tout - Visualiser dans une fenêtre à part
1
2
3
4
5
6
7
8
9
10
11
12
13
14 let rec fact' = function | 0 -> 1 | n -> n * fact' (n-1) let fact = let preconds = { rname = "x positive" ; rcond = fun x -> x >= 0}:: { rname = "x pas trop grand" ; rcond = fun x -> x <=12}::[] and postconds = { ename = "res positive" ; econd = fun res x -> res >= 0}:: { ename = "res >= x" ; econd = fun res x -> res >= x}:: { ename = "condition bidon" ; econd = fun res x -> false}::[] in add_DBC fact' preconds postconds
Je me pose les questions suivantes :
-dans mes types precondition et postcondition, je trouverais cela plus élégant d'avoir les même labels name et cond. Or le toplevel accepte au moment de la déclaration, mais par la suite lors de l'inférence de type il me dit que des " record field label" sont "mixed"
-je trouverais cela également beaucoup plus élégant de ne définir qu'une seule fonction conds_fold en utilisant un polymorphisme, mais je ne vois pas comment...
-le nom fold est-il parlant et approprié ?
-et j'aimerais pouvoir renvoyer un message d'erreur reprenant le nom de la condition.ename ou .rname ...
-peut-on gagner en concision et lisibilité ? par exemple, dans rcond = fun x -> x >= 0 seul "x>=0" est important, peut on construire le reste à partir l'expression simple ?
-comment faire fonctionner cela sur des fonctions à plusieurs paramètres ?
me renvoie :
Code : Sélectionner tout - Visualiser dans une fenêtre à part
1
2
3
4
5
6 let add' a b = a + b;; let add a b = let preconds = {rname = " " ; rcond = fun (a, b) -> a < b}::[] and postconds = [] in add_DBC add' preconds postconds
... voilà c'est tout ... pour aujourd'hui ...
Code : Sélectionner tout - Visualiser dans une fenêtre à part
1
2 This expression has type ('a * 'a) precondition list but is here used with type int precondition list
Vos avis sont les bienvenus ! Comme je l'ai dit, c'est autant pour apprendre que pour peut-être m'en servir par la suite ...
Partager