Prouver l’absence des erreurs dans les logiciels n’est pas souvent source de préoccupation. “Et si mon programme plante ? Bah, peu importe, je vais juste le relancer.” Mais parfois, un programme qui plante pose de gros problèmes : cela peut mener à des morts, coûter beaucoup d’argent ou compromettre des données confidentielles. Un tel logiciel est dit critique, et il est alors intéressant de prouver certaines propriétés comme l’absence d’erreurs d’exécutions (comme les divisions par 0), que le résultat est ce qu’on attend ou que le programme termine suffisamment vite.
L’interprétation abstraite est une méthode générale permettant de prouver de telles propriétés en utilisant une approximation de la sémantique. L’exemple le plus classique est la règle des signes pour la multiplication : quel que soit la valeur de deux nombres, s’ils ont le même signe, le résultat est positif. Grâce à une connaissance partielle sur l’état des données, on déduit des propriétés sur le résultat. Souhaitablement, on déduit des conditions assez précises pour prouver les propriétés d’intérêt.
En général, les propriétés qui nous intéressent (comme l’absence d’erreurs) ne sont pas calculable : le théorème de Rice nous instruit qu’il n’existe pas d’algorithme qui détermine si un programme ne contient pas d’erreur. Pour trouver tous les bugs automatiquement, nous devons accepter de détecter des bugs qui n’existent que dans l’approximation de la sémantique. Le but est de construire une approximation suffisamment précise pour prouver ce qu’on veut, mais suffisamment grossière pour passer à l’échelle dans les applications réelles.
Cet exposé est une introduction à l’interprétation abstraite motivée par des exemples.