Mission nationale de sauvegarde du patrimoine scientifique et technique contemporain

Description

Titre traduit : programmation and control
Cette fiche identifie le PDF d'un support PowerPoint initial, réalisé par le professeur Abrial pour illustrer une conférence donnée au Collège de France. Cette conférence a pour titre et sujet : "Spécification, construction et vérification de programmes, le parcours d'une pensée scientifique sur une quarantaine d'années".
Son auteur Jean-Raymond Abrial a été en poste à l'IMAG à Grenoble dans les années 1970. Il est le co-concepteur du SGBD SOCRATE (un Système de Gestion de Base de Données de type "réseau"), ainsi que de travaux sur la sémantique des langages de programmation, et de ce fait a contribué à créer les langages Z, B et event-B.
- Z est une méthode de notation, datant de la fin des années 1970 et issue de la théorie des ensembles, réalisée dans le but de faciliter l'édition de spécifications dont l'implémentation, en termes de programmes informatiques, puisse être "vérifiable".
- B, qui date pour sa part de la fin de années 1980, vise à "automatiser" la programmation. B a été utilisé avec succès par la RATP pour la programmation informatique en ADA de l'automatisation de la ligne n° 14 du métro parisien. L'objectif était de limiter le nombre des tests en les remplaçant par des preuves interactives, tout en conservant un bon degré de fiabilité et de confiance.
- Event-B est un élément du projet européen Rodin, qui a prit place à partir de 2002.

Utilisation

Cette conférence donnée au Collège de France sur invitation reconnaît les compétences de Jean-Raymond Abrial en matière de langages de programmation, et l'aptitude qu'il a développé pour en vérifier à la fois la conformité et la fiabilité.
La conférence montre les efforts entrepris entre 1980 et 2002 pour que les programmes informatiques intervenant dans des automatismes (ou en intelligence artificielle) puissent être "vérifiés" de manière interactive, tout en s'affranchissant des méthodologies trop frustes que sont les tests. Car la méthode par tests est non seulement extrêmement coûteuse, mais surtout elle s'avère incapable de couvrir toute la variété des cas qui peuvent exister dans l'utilisation des automatismes dans le monde réel.