La construction méthodique d'algorithmes répartis est un élément fondamental de la maitrise du parallèlisme ; les algorithmes de contrôle en constituent une classe importante, par le rôle qu'ils sont amenés à jouer dans les systèmes répartis. Ces algorithmes reposent souvent sur l'évaluation d'un prédicat global, qui ne peut être mise en oeuvre que de manière non simultanée et retardée. Après avoir défini formellement ce type d'évaluation, cet article présente une construction méthodique d'un algorithme réparti de détection de la terminaison (il s'agit là d'un des paradigmes de l'observation dans un contexte réparti). Cette construction est obtenue par étapes successives, chacune de ces étapes constituant un pas de dérivation. L'approche suivie ici constitue donc un pas vers l'extension au contexte réparti d'une methode analogue a celle proposée par Gries dans le contexte séquentiel pour la dérivation de programmes.