Vérification automatisée de programmes impératifs dans un langage à typage dépendant

Abstract

Les langages de programmation disposant d'un système de typage statique encouragent généralement une meilleure robustesse des programmes qui y sont écrits, car les risques de bogues introduits par inadvertance sont réduits par rapports aux systèmes à typage dynamique : plusieurs classes d'erreurs sont identifiées par le compilateur avant qu'un programme ne soit exécuté. Plusieurs travaux actuels visent à exploiter le typage statique pour pousser plus loin ces garanties de robustesse, en permettant d'exprimer formellement, sur un programme ou sur une partie de celui-ci, des contraintes arbitraires et d'en vérifier mécaniquement la conformité. Les techniques actuellement développées sont conçues pour s'appliquer à des langages fonctionnels. Cependant, la programmation fonctionnelle, en dépit de ses avantages au plan de la robustesse, est limitée en ce sens qu'elle n'autorise pas directement la manipulation de la mémoire, ce qui complique, dans certains cas, l'écriture d'algorithmes efficaces. Ce travail vise à introduire une extension dans un langage fonctionnel existant afin de permettre d'écrire des programmes dans un style impératif, c'est-à-dire qui manipulent directement la mémoire, et de vérifier statiquement leur conformité à des propriétés formelles. Programming languages using static type systems generally make for more robust programs, as the risk of bugs being inadvertently introduced into a program written in a statically typed language is lower compared to dynamically typed languages, because compilers are able to flag certain kinds of errors before a program is run. A portion of the current research on the topic aims to leverage static type systems to enforce stronger robustness guarantees by allowing formal properties of a program, or part of it, to be mechanically verified. Methods being currently developed are meant to be used in functional languages. However, despite its advantages in terms of program robustness, the functional programming paradigm prohibits direct memory access and manipulation, which hinders the development of efficient algorithms. This work aims at extending an existing functional language to allow writing programs in an imperative style—that is, programs that directly manipulate their memory—while statically verifying and enforcing their conformity with formal properties.