01- Équivalences de programmes : Introduction à l'équivalence et au raffinement entre programmes

Xavier Leroy

Chaire Sciences du logiciel

Année 2026-2027

Collège de France

01- Équivalences de programmes : Introduction à l'équivalence et au raffinement entre programmes

Résumé

Lors d'un développement logiciel, il est fréquent de devoir comparer les comportements de plusieurs versions du même fragment de programme afin de s'assurer qu'il n'y a pas de régression. Nous avons présenté deux exemples : l'optimisation (amélioration des performances) par réécriture progressive du code source, et la méthodologie de développement par raffinements successifs d'une spécification. Nous avons ensuite défini informellement les notions d'équivalence et de raffinement entre programmes, qui correspondent respectivement à l'égalité et à l'inclusion des ensembles de comportements observables. Ces notions sont faciles à caractériser pour des langages simples comme les expressions arithmétiques, mais deviennent de plus en plus délicates lorsqu'on ajoute des traits au langage comme les fonctions, l'évaluation paresseuse, l'ordre supérieur, le non-déterminisme, l'abstraction de types, ainsi que les fonctions et objets avec état mutable interne.

Nous avons ensuite défini l'équivalence observationnelle, aussi appelée équivalence contextuelle de Morris, en faisant une analogie avec les jeux de tests exhaustifs. En raison de sa définition très générale et de ses bonnes propriétés mathématiques, cette équivalence est considérée comme « l'étalon-or » des équivalences de programmes. Cependant, elle est très difficile à démontrer directement, ce qui explique pourquoi d'autres techniques de preuve d'équivalence ou de raffinement sont nécessaires. Nous en avons mentionné quatre : les sémantiques dénotationnelles, les bisimulations, les relations logiques et les logiques relationnelles, qui seront étudiées dans les séances suivantes du cours.