Sémantique différentielle des programmes

Computer programs are rarely written in one fell swoop. Instead, they are written in a series of incremental changes.It is also frequent for software to get updated after its initial release. Such changes can occur for various reasons, such as adding features, fixing bugs, or improving performances for instance. It is therefore important to be able to represent and reason about those changes, making sure that they indeed implement the intended modifications.In practice, program differences are very commonly represented as textual differences between a pair of source files, listing text lines that have been deleted, inserted or modified. This representation, while exact, does not address the semantic implications of those textual changes. Therefore, there is a need for better representations of the semantics of program differences.Our first contribution is an algorithm for the construction of a correlating program, that is, a program interleaving the instructions of two input programs in such a way that it simulates theirsemantics. Further static analysis can be performed on such correlating programs to compute an over-approximation of the semantic differences between the two input programs. This work draws direct inspiration from an article by Partush and Yahav, that describes a correlating program construction algorithm which we show to be unsound on loops that include `break` or `continue`statements. To guarantee its soundness, our alternative algorithm is formalized and mechanically checked within the Coq proof assistant.Our second and most important contribution is a formal framework allowing to precisely describe and formally verify semantic changes.This framework, fully formalized in Coq, represents the difference between two programs by a third program called an oracle.Unlike a correlating program, such an oracle is not required to interleave instructions of the programs under comparison, and may “skip” intermediate computation steps. In fact, such an oracle is typically written in a different programming language than the programs it relates, which allows designing correlating oracle languages specific to certain classes of program differences, andcapable of relating crashing programs with non-crashing ones.We design such oracle languages to cover a wide range of program differences on a toy imperative language. We also prove that our framework is at least as expressive as Relational Hoare Logic by encoding several variants as correlating oracle languages, proving their soundness in the process.Les programmes informatiques sont rarement écrits d'un seul coup, et sont au contraire composés de changements successifs. Il est également fréquent qu'un logiciel soit mis à jour après sa sortie initiale. De tels changements peuvent avoir lieu pour diverses raisons, comme l'ajout de fonctionnalités ou la correction de bugs. Il est en tout cas important d'être capable de représenter ces changements et de raisonner à leur propos pour s'assurer qu'ils implémentent les changements voulus.En pratique, les différences entre programmes sont très souvent représentées comme des différences textuelles sur le code source, listant les lignes de textes ajoutées, supprimées ou modifiées. Cette représentation, bien qu'exacte, ne dit rien de leurs conséquences sémantiques. Pour cette raison, il existe un besoin pour de meilleures représentations des différences sémantiques entre programmes.Notre première contribution est un algorithme de construction de programmes de corrélation, c'est-à-dire, des programmes entrelaçant les instructions de deux autres programmes de telle sorte qu'ils simulent leur sémantiques. Ces programmes de corrélation peuvent alors être analysés pour calculer une sur-approximation des différences sémantiques entre les deux programmes d'entrée. Ce travail est directement inspiré d'un article de Partush et Yahav, qui décrit un algorithme similaire, mais incorrect en présence de boucles avec des instructions `break` ou `continue`. Pour garantir la correction de notre algorithme, nous l'avons formalisé et prouvé à l'aide de l'assistant de preuve Coq.Notre seconde et plus importante contribution est un cadre formel permettant de décrire précisément et de formellement vérifier des différences sémantiques. Ce cadre, complètement formalisé en Coq, représente la différence entre deux programmes à l'aide d'un troisième programme que nous appelons oracle. Contrairement à un programme de corrélation, un oracle n'entrelace pas nécessairement les instructions des deux programmes à comparer, et peut « sauter » des calculs intermédiaires.Un tel oracle est généralement écrit dans un langage de programmation différent des programmes à comparer, ce qui permet de concevoir des langages d'oracles spécifiques à certaines classes de différences, capables de mettre en relation des programmes qui plantent avec des programmes qui s'exécutent correctement.Nous avons conçu de tels langages d'oracles pour couvrir un large éventail de différences sur un langage impératif jouet. Nous avons également prouvé que notre cadre est au moins aussi expressif que celui de la Logique Relationnelle de Hoare en encodant plusieurs variantes de cette dernière sous forme de langages d'oracles, prouvant leur correction dans la foulée