Résumé
Il y a deux principaux types de méthodes formelles pour la preuve de programme : les méthodes générales, qui s’adressent à tous les types de programmes et seront présentées dans ce cours, et celles de la vérification de modèles (model-checking), qui s’intéressent principalement aux programmes à espaces d’états finis et aux circuits électroniques et seront traitées dans le cours no 5 du 25 mars 2015.
La nécessité de traiter les programmes comme des objets mathématiques à part entière a été reconnue par A. Turing dès 1949. Il a alors introduit la notion d’assertion associant un prédicat logique à un point de contrôle du programme, ainsi que l’importance de la notion d’ordre bien fondé pour montrer la terminaison des programmes. Son approche par assertions est la première que nous traiterons dans le cours. Elle a été étendue et perfectionnée par R. Floyd, C.A.R. Hoare, E.W. Dijkstra, et bien d’autres, pour aboutir à une théorie et une pratique complètes de la définition logique des langages de programmation et de la vérification de programmes, applicables initialement aux programmes séquentiels impératifs. La notion d’assertion a été ensuite étendue en celle de contrat (assume/guarantee) à respecter par les fonctions ou modules d’un programme, applicable aussi aux langages objets et aux langages parallèles.
