L'arithmétique de séparation

National audienceNous, praticiens de la preuve de programmes, souhaitons que le processus de la vérification soit le plus automatique possible. Les meilleurs outils pour cela sont à l'heure actuelle les démonstrateurs SMT, qui combinent notamment la logique du premier ordre et l'arithmétique linéaire. Par opposition, le raisonnement inductif n'est pas un point fort des démonstrateurs automatiques. Or, les programmes utilisant des pointeurs le font souvent pour manipuler des structures récursives : listes, arbres, etc. Dans cet article, nous décrivons une approche qui permet d'amener la preuve de programmes avec pointeurs à la portée des démonstrateurs automatiques. L'idée consiste à projeter une structure récursive sur un domaine numérique, de sorte que les propriétés de possession et de séparation deviennent exprimables en terme de simples inégalités arithmétiques. En plus de simplifier la preuve, cela permet une spécification claire et naturelle. On illustre cette approche avec l'exemple classique du renversement en place d'une liste simplement chaînée