Discussion :

[james-mi]

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 :

Code :

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

1
2
3
let pre_condition cond f x =
  assert (cond x);
  f x

- or je voudrais éviter d'envoyer f à ma précondition, ce n'est pas vraiment gênant, mais par principe ...
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 :

Code :

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

let positive x = x >= 0

-je me demande comment renvoyer quelque chose comme "failed condition "positive""...

J'ai donc tenté une autre approche. Elle fonctionne en partie :

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

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
 
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

comme je l'ai dit cela fonctionne sur fact, mais je ne suis pas allé beaucoup plus loin pour l'instant.

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 ?

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

me renvoie :

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

... voilà c'est tout ... pour aujourd'hui ...

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 ...

[LLB]

1- ne fonctionnent que sur les fonction à un seul argument

Cet argument peut être un tuple. Éventuellement, tu peux appeler la fonction suivante :

Code :

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

let curry f x y = f (x, y)

J'ai donc tenté une autre approche. Elle fonctionne en partie

J'ai une préférence pour les listes de couples. C'est plus léger (pas de déclaration préalable).

-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"

C'est une limitation de Caml (pour rendre l'inférence plus efficace).

Proposition rapide (j'ai pas vraiment testé) :

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
21
let test_cond l test =
  List.iter (fun (str,f) -> if not (test f) then failwith str) l
 
let add_DBC f pre post x =
  test_cond pre (fun f -> f x);
  let res = f x in
  test_cond post (fun f -> f res x);
  res
 
let rec fact' = function
  | 0 -> 1
  | n -> n * fact' (n-1)
 
let fact =
  let preconds =
    ["x positive", (fun x -> x >= 0) ;
     "x pas trop grand", (fun x -> x <=12) ]
  and postconds =
    ["res positive", (fun res x -> res >= 0) ;
     "res >= x", (fun res x -> res >= x) ]
  in add_DBC fact' preconds postconds

Je n'ai pas trop le temps d'expliquer, j'espère que c'est assez clair.

[james-mi]

oui merci c'est assez clair.

C'est beaucoup plus léger que mon code initial.

une question sur

Code :

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

1
2
3
4
 
let add_DBC f pre post x =
  test_cond pre (fun f -> f x);
  ...

le (fun f -> f x) va lier x à tout fonction f passée en argument à la fun anonyme, c'est cela ? (quand je dis lier, je ne suis pas sûr d'avoir le bon vocabulaire ...)

comme dans :

Code :

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

1
2
3
4
5
6
7
 let test = let x = 5 in (fun f -> f x);;
val test : (int -> 'a) -> 'a = <fun>
 
test fact;;
- : int = 120
# test succ;;
- : int = 6

si c'est juste, alors j'ai compris ton approche ...

je vais m'atteler à la décliner pour plusieurs arguments, tu m'as donné la piste avec x de type tuple