Présentation
Quand pouvons-nous dire que deux programmes sont équivalents, au sens où ils ont les mêmes comportements observables ? Ou qu'un programme en raffine un autre, au sens où tous les comportements observés du premier correspondent à des comportements possibles du second ? Ces questions se posent dans plusieurs domaines des sciences du logiciel, des méthodologies de développement logiciel par raffinements de spécifications à la vérification de la correction des compilateurs en passant par le test de non-régression et la correction automatique d'exercices de programmation. Les notions d'équivalence et de raffinement entre programmes occupent également une place importante dans la théorie des langages de programmation : la définition la plus naturelle, à savoir l'équivalence contextuelle, étant particulièrement difficile à utiliser, de nombreuses autres approches, moins directes mais plus utilisables, ont été étudiées. Le cours fera le point sur cette diversité d'approches et d'utilisations, en insistant particulièrement sur les techniques de bisimulations, de relations logiques, et de logiques relationnelles.