Résumé
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.
