Gérard Berry

Algorithmes, machines et langages

Année 2014-2015

Prouver les programmes : pourquoi, quand, comment ?

Deuxième leçon : De la spécification à la réalisation, au test et à la preuve : les approches formelles

Ce premier cours du cycle « Prouver les programmes : pourquoi, quand, comment » a pour but d'introduire les méthodes formelles de développement et vérification de programmes, en les reliant aux méthodes de programmation, test et validation classiques.

Dès les débuts de l'informatique, la difficulté de faire des programmes justes est apparue comme un problème majeur. Deux approches bien différentes ont été développées : d'une part, le génie logiciel, qui s'est développé lentement mais est maintenant bien en place au moins dans les entreprises sérieuses, et, d'autre part, une approche formelle beaucoup plus scientifique, introduite par Turing dès 1949 et fondée sur l'idée de voir un programme comme une entité mathématique sur laquelle il faut raisonner mathématiquement. C'est cette dernière qui a conduit aux méthodes formelles que nous étudierons cette année et les suivantes. Ces deux approches se sont développées très indépendamment l'une de l'autre et ne commencent à converger que depuis peu de temps : développement et vérification formels apparaissent désormais comme des moyens efficaces voire privilégiés d'éviter les bugs, au moins dans les applications où leur coût humain et matériel peut être catastrophique. Les techniques de vérification formelle ont eu une maturation assez lente, d'une part parce que le sujet est intrinsèquement difficile, d'autre part parce que l'industrie ne s'y est vraiment intéressée que récemment. Mais les choses bougent rapidement, avec des succès de plus en plus fréquents. Et, ce qui ne gâche rien pour un tel enseignement, les chercheurs français jouent un rôle majeur dans ce domaine en plein essor.

Génie logiciel et vérification formelle partagent deux prérequis essentiels : d'abord, la qualité des spécifications initiales, qui doivent être précises, non-contradictoires, et complètes mais sans excès de précision inutile ; ensuite, la qualité des langages de programmation, dont la sémantique doit être précise tout en restant intuitive. Beaucoup de projets industriels échouent encore à cause de leur non-respect de ces contraintes.

Le génie logiciel classique écrit les spécifications en langage habituel et fournit des outils de traçabilité permettant de relier spécifications et réalisation. Pour la validation du résultat, il s'appuie sur des revues de code et surtout sur des tests, ce qui pose deux problèmes majeurs : il est difficile de mesurer ce que les tests testent réellement, et le test n'apporte aucune information sur ce qui n'est pas testé. Mais nous verrons que des systèmes de génération de tests aléatoires dirigés permettent d'obtenir des résultats étonnants.

À l'opposé, les méthodes formelles écrivent les spécifications en langage mathématique, le seul langage rigoureux dont nous disposions réellement, et font aussi progresser ce langage. Les systèmes modernes de typage des programmes permettent de détecter des erreurs dès les premières passes de compilation. Les meilleurs d'entre eux sont directement issus des recherches en sémantique de la programmation, elles-mêmes directement liées à la vérification formelle. Pour aller plus loin, on cherche à remplacer ou compléter les tests dynamiques de validation par des preuves statiques là encore mathématiques, aidées par des systèmes de vérification formelle plus ou moins automatisés. Au contraire des tests, la vérification formelle dit tout sur les propriétés à valider : prouvées vraies, elles le sont en toutes circonstances ; détectées comme fausses, les outils permettent souvent de construire des tests les invalidant et de découvrir ainsi la source de l'erreur. Mais la preuve, techniquement plus difficile que le test, demande une formation particulière. Et elle ne constitue pas forcément une panacée car certaines propriétés comme l'arrêt d'un programme ne sont pas prouvable en général (bien que les choses s'améliorent en pratique).

Après avoir détaillé les problématiques ci-dessus, nous présenterons brièvement les styles de méthodes formelles qui seront détaillées dans la suite du cours, ainsi que leurs applications pratiques : assertions, preuves par réécritures sémantiques formelles, interprétation abstraite, vérifications logiques par assistants de preuve, et vérification automatique de modèles. Un point important de la discussion sera le lien avec la programmation classique. Nous verrons que trois points de vue assez différents coexistent naturellement, ce qui est une des raisons de la multiplicité des techniques précitées :

Programmer comme d'habitude et utiliser les outils de vérification formelle pour complémenter les tests et vérifier un certain nombre de propriétés critique du programme (absence d'erreurs bloquant l'exécution, vérification de prédicats sur les états ou les sorties, etc.). C'est une solution souvent utilisée en conception de circuits électroniques ou en logiciel embarqué.

À l'opposé, abandonner les méthodes classiques en intégrant dans un formalisme logique unique l'ensemble du chemin allant des spécifications formelles au code exécutable, tout en réalisant en permanence des preuves automatiques ou guidées manuellement de la correction de la réalisation par rapport aux spécifications. Cette façon de faire très ambitieuse, généralement fondée sur des assistants de preuve en logique formelle, est utilisée à des degrés divers pour des applications en transports, compilation, systèmes d'exploitation, algorithmes distribués, sécurité informatique, etc.

Entre les deux se placent des méthodes intermédiaires comme l'interprétation abstraite et vérification de modèles, dans lesquelles l'objet vérifié est un modèle plus ou moins abstrait de l'application. On se focalise alors sur le traitement des points difficiles ou dangereux de la spécification en abstrayant ses détails peu significatifs. Cette approche permet de réduire considérablement la taille de la vérification, sans toutefois toujours débusquer le diable qui peut se nicher dans les détails de la réalisation. Elle est souvent privilégiée pour les applications parallèles, distribuées ou temps-réels, ainsi que pour la sécurité informatique.