Table des matières:
Pour corriger ses programmes le plus simple est de suivre les appels
de fonction en ``traçant'' sa fonction, avec la primitive trace:
#let rec fib x = if x <= 1 then 1 else fib (x - 1) + fib (x - 2);; fib : int -> int = <fun> #trace "fib";; La fonction fib est dorénavant tracée. - : unit = () #fib 3;; fib <-- 3 fib <-- 1 fib --> 1 fib <-- 2 fib <-- 0 fib --> 1 fib <-- 1 fib --> 1 fib --> 2 fib --> 3 - : int = 3 #untrace "fib";; La fonction fib n'est plus tracée. - : unit = ()
La difficulté est évidemment que l'impression obtenue avec la trace n'est pas vraiment informative dans le cas d'arguments ou de résultats polymorphes. Considérons un programme de tri simple (le tri à bulle):
let echange i j v = let aux = v.(i) in v.(i) <- v.(j); v.(j) <- aux;; echange : int -> int -> 'a vect -> unit = <fun> let une_passe_vect fin v = for j = 1 to fin do if v.(j - 1) > v.(j) then echange (j - 1) j v done;; une_passe_vect : int -> 'a vect -> unit = <fun> let tri_bulle_vect v = for i = vect_length v - 1 downto 0 do une_passe_vect i v done;; tri_bulle_vect : 'a vect -> unit = <fun> #trace "une_passe_vect";; La fonction une_passe_vect est dorénavant tracée. - : unit = () #let q = [| 18; 3; 1 |];; q : int vect = [|18; 3; 1|] #tri_bulle_vect q;; une_passe_vect <-- 2 une_passe_vect --> <fun> une_passe_vect* <-- [|<poly>; <poly>; <poly>|] une_passe_vect* --> () une_passe_vect <-- 1 une_passe_vect --> <fun> une_passe_vect* <-- [|<poly>; <poly>; <poly>|] une_passe_vect* --> () une_passe_vect <-- 0 une_passe_vect --> <fun> une_passe_vect* <-- [|<poly>; <poly>; <poly>|] une_passe_vect* --> () - : unit = ()
La fonction une_passe_vect étant polymorphe son vecteur
argument est imprimé comme un vecteur de valeurs polymorphes,
[|<poly>; <poly>; <poly>|], et l'on ne suit pas
l'évolution des calculs.
La solution simple à ce problème est de travailler avec une version monomorphe de la fonction à corriger. On obtient facilement cette version monomorphe traçable, en utilisant une contrainte de type. En général, cela suffit à comprendre et à corriger l'erreur qui s'était glissée dans la fonction polymorphe. Il suffit ensuite de supprimer la contrainte de type pour revenir à une version polymorphe de la fonction maintenant corrigée. Dans le cas du tri, il est même possible que le caractère polymorphe obtenu ne soit pas un desiderata conscient du programmeur, mais une conséquence insoupçonnée des comparaisons polymorphes de Caml!
Dans notre cas du tri, il suffit donc de contraindre l'argument de
la fonction echange à être un vecteur d'entiers pour
tracer correctement les appels de fonctions:
let echange i j (v : int vect) = [...] echange : int -> int -> int vect -> unit = <fun> [...] une_passe_vect : int -> int vect -> unit = <fun> [...] tri_bulle_vect : int vect -> unit = <fun> #trace "une_passe_vect";; La fonction une_passe_vect est dorénavant tracée. - : unit = () #let q = [| 18; 3; 1 |];; q : int vect = [|18; 3; 1|] #tri_bulle_vect q;; une_passe_vect <-- 2 une_passe_vect --> <fun> une_passe_vect* <-- [|18; 3; 1|] une_passe_vect* --> () une_passe_vect <-- 1 une_passe_vect --> <fun> une_passe_vect* <-- [|3; 1; 18|] une_passe_vect* --> () une_passe_vect <-- 0 une_passe_vect --> <fun> une_passe_vect* <-- [|1; 3; 18|] une_passe_vect* --> () - : unit = ()
Les fonctions prédéfinies peuvent être tracées comme les autres, aux problèmes de polymorphisme évoqués plus haut près, mais elles posent un problème supplémentaire: vous les partagez avec le système interactif. Cela implique que tous les appels à la fonction qui sont faits par le système interactif, sont désormais tracés aussi. Par exemple:
#trace "map";; La fonction map est dorénavant tracée. #[];; map <-- <fun> map --> <fun> map* <-- [<poly>] map* --> [<poly>] - : 'a list = []
La fonction map est en effet utilisée par le système
interactif pour ses besoins propres (analyse syntaxique, typage,
compilation, édition des liens et évaluation de la phrase tappée). Si
ce comportement ne vous convient pas, il faut définir votre propre
fonction équivalente à la fonction prédéfinie, et tracer cette
nouvelle version:
#untrace"map";;
map <-- <fun>
map --> <fun>
map* <-- [<poly>]
map* --> [<poly>]
La fonction map n'est plus tracée.
- : unit = ()
#let map f l = map f l;;
map : ('a -> 'b) -> 'a list -> 'b list = <fun>
#trace "map";;
La fonction map est dorénavant tracée.
- : unit = ()
#[];;
- : 'a list = []
#map succ [1];;
map <-- <fun>
map --> <fun>
map* <-- [<poly>]
map* --> [<poly>]
- : int list = [2]
C'est un cas particulier subtil du phénomène précédent: si vous
tracez une des fonctions prédéfinies utilisées pendant la
trace, le mécanisme de trace se met évidemment à boucler. Ce
phénomène apparaît par exemple si vous tenter de tracer l'une des
fonctions d'impression du bel imprimeur format, que la trace utilise pour
imprimer les valeurs; même chose pour les fonctions
d'entrées-sorties. Si l'espionnage de ces fonctions s'avère
indispensable, il faut impérativement, comme dans le paragraphe
précédent, redéfinir les fonctions en cause avant de les utiliser. Ce
sont ces nouvelles versions des fonctions prédéfinies que vous
tracerez.
Pour suivre l'évolution des variables mutables d'un programme la trace ne suffit pas, il faut un mécanisme supplémentaire qui permet d'arrêter le programme en cours d'exécution et d'interroger son état interne, c'est le correcteur symbolique avec son mode pas à pas.
L'exécution en mode pas à pas d'un programme fonctionnel a un sens un peu délicat à définir et à comprendre. On fait intervenir des événements d'exécution qui se produisent par exemple au passage d'un paramètre ou à l'entrée d'un filtrage, ou encore à la sélection d'une clause de filtrage. La progression de l'exécution est comptée par ces évènements, indépendamment des instructions exécutées par la machine.
Malgré la difficulté d'implémenter ce mécanisme, un tel mode
d'exécution existe sous Unix (c'est le correcteur de programme
camldebug), malheureusement il fait intervenir des traits
avancés d'Unix, et n'est donc pas portable sur les micros ordinateurs
Macintosh ou PC. Sur ces machines, il faut effectivement utiliser la
trace ou bien l'impression de messages explicites dans ses
programmes.
En fait l'expérience prouve que pour les programmes complexes, on
corrige ses programmes en utilisant l'impression explicite (à l'aide
de printf ou le bel imprimeur ``format''), car cela
permet de n'afficher que les données pertinentes et de façon bien plus
compacte et adaptée qu'un imprimeur générique.
L'impression explicite est certainement pas une mauvaise méthode: même sous Unix l'expérience prouve que les programmeurs utilisent peu le correcteur pas à pas: ils préfèrent espionner leurs programmes à l'aide d'impression insérées directement dans le programme, et s'assurer de la cohérence des invariants à l'aide d'assertions testées dynamiquement.
Contacter l'auteur Pierre.Weis@inria.fr