Nous présentons une spécification, une dérivation et une preuve de correction totale de l'algorithme de Schorr-Waite pour un marquage en profondeur d'un graphe binaire codé par des pointeurs. Notre approche est purement algébrique et fonctionnelle, depuis une spécification simple jusqu'à un programme récursif terminal simulant le langage C. Puis, nous obtenons par des transformations élémentaires un véritable programme en C, impératif et itératif.