Cette thèse se place dans la tradition de l’étude de la théorie mathématique des langages de programmation, et plus précisément du développement de l’outillage sémantique pour leur étude. Afin de définir la sémantique d’un langage formel, une méthode éprouvée est la construction d’une équivalence comportementale : une telle équivalence permet d’identi- fier des programmes ayant le même comportement (c’est-à-dire qu’ils produisent les mêmes résultats, qu’ils accomplissent les mêmes communications, etc), et ce même si ce sont des programmes qui parviennent à ce résultat (ou à ces communications, dans le cas d’un langage concurrent) d’une manière tout à fait distincte.
Étudier de telles équivalences comportementales permet d’abstraire la syntaxe des lan- gages, pour en extirper le contenu significatif, sémantique. Cependant, la concrétisation de cette opération par la preuve de l’équivalence de deux programmes peut être, dans certain cas, d’une extrême difficulté. Ainsi, si la définition de telles équivalences est aujourd’hui une question largement explorée et résolue, leur utilisation en pratique pose problème.
C’est pourquoi il est courant de faire appel à un outillage de techniques de preuves, permettant de faciliter la preuve que deux programmes ont bien le même comportement. De ce point de vue, la bisimilarité [Mil89] est une équivalence comportementale notable, car elle est définie par une telle technique de preuve : la méthode de la bisimulation, à qui elle doit dans une large mesure son succès – d’autant que cette méthode constitue aussi une technique de preuve pour d’autres équivalences. En effet, la bisimilarité est une équivalence plus fine que la plupart des autres équivalences considérées en pratique : pour montrer que deux programmes sont équivalents, il suffit souvent de montrer qu’ils sont bisimilaires (lorsque c’est possible). Les méthodes inspirées de la bisimilarité sont aujourd’hui utilisées dans de nombreux domaines de l’informatique, dans la théorie des automates par exemple [BP13, BP15], ou encore, en pratique, dans la certification du compilateur CompCert [Ler].
Cette méthode est d’autant plus robuste qu’elle a été au fur et à mesure enrichie de di- verses améliorations, dont entre autres les techniques dites « modulo » [Mil89, San98, PS11] (« up to » en anglais). Si la théorie de ces améliorations constitue un sujet d’étude à part entière, elle a également été comparée par Sangiorgi [San15] à la technique d’unicité des solutions des équations. Plus précisément, Sangiorgi établit une correspondance entre les techniques « modulo contextes » et la technique d’unicité des solutions. Cette technique propose d’utiliser une équation récursive entre programmes, dotée de la propriété d’unicité des solutions, caractérisant les équations dont tous les programmes qui sont solutions sont aussi équivalents entre eux (pour une équivalence comportementale donnée – ici, la bisimi- larité). Pour prouver que deux programmes sont équivalents, il suffit alors de prouver qu’ils sont chacun solution de ladite équation ; la preuve d’équivalence nécessaire pour le justifier étant souvent plus simple qu’une preuve d’équivalence directe entre les deux programmes.
Toute équation n’admet pas l’unicité des solutions : ainsi, l’équation X = X admet tout programme comme solution. Pour utiliser une telle technique, il est donc vital de caractériser les équations admettant l’unicité des solutions, en proposant un ensemble de conditions suffisantes pour le garantir. Milner, dans son ouvrage pionnier sur la concurrence [Mil89], dans lequel il définit la bisimilarité, les techniques modulo, et les techniques d’unicité des solutions, donne un tel critère, qui s’appuie sur la notion syntaxique de « garde » : une équation est gardée si une opération doit nécessairement se produire avant toute récursion, c’est-à-dire avant que la variable d’équation n’apparaisse. Ainsi, l’équation X = X n’est pas gardée, mais pour une opération op, garantissant une forme de précédence, l’équation X = op(X ) le serait. Cependant le critère proposé par Milner est contraignant, en ce qu’il interdit également toute forme de concurrence dans l’équation considérée. Cela est dû au fait que l’on considère des équivalences comportementales faibles : c’est-à-dire que l’on abstrait le programme du nombre de ses étapes de calcul internes (ou un protocole concurrent du nombre de synchronisations internes). considérant uniquement les opérations « visibles ». Or, dans ce cadre, le critère syntaxique habituel de garde ne garantit pas que des opérations visibles doivent se produire avant qu’apparaisse la variable récursive. Il est intéressant de constater que les techniques modulo également souffrent de limitations dans le cadre d’une équivalence faible, pour des raisons similaires.
Le langage CSP, proposé par Hoare [Hoa85], et dont on considère généralement une sémantique dénotationnel le, c’est-à-dire une sémantique mathématique abstraite, possède également une théorie de la récursion et d’unicité des solutions. En particulier, si les critères de Hoare sont soumis aux mêmes limitations que les critères de Milner, Roscoe [Ros92, Ros97] propose une garantie bien plus flexible pour garantir l’unicité des solutions pour une équivalence faible, reposant sur le concept de divergence : un programme diverge s’il a la possibilité de procéder à un nombre infini d’opérations internes, impossibles à constater pour un observateur extérieur.
Gratuit
Disciplines