Re: Solution à base de types variants en ADA

Oui, c'est bien la méthode B et l'atelier B qui est derrière tout ça. C'est un successeur du formalisme Z qui a inspiré le langage Eiffel et sa programmation par contrat.

Son inventeur, Jean-Raymond Abrial, est revenu sur l'histoire de ces approches dans une conférence au Collège de France dont voici la présentation :

Cette présentation est celle d’un chercheur vieillissant qui porte un regard historique sur les trente dernières années de son travail.

Il y a deux sortes de chercheurs : les prolifiques et les monomaniaques. Je fais partie de la seconde catégorie, car j'ai toujours pratiqué le même genre d’investigations, à savoir la spécification et la construction vérifiée de systèmes informatisés.

Ce travail, autant théorique que pratique, s’est concrétisé au cours de toutes ces années dans trois formalismes voisins : Z, B et Event-B (dont je ne suis pas, loin de là, le seul contributeur). Je vais tenter d’expliciter comment les idées que contiennent ces formalismes et les outils correspondants ont lentement émergés de façon parfois erratique.

Je tenterai aussi de préciser les multiples influences qui ont participé à cette évolution. En particulier, je montrerai comment plusieurs réalisations industrielles ont permis de progresser dans ce domaine. Mais je soulignerai aussi les échecs et parfois les rejets de la part de communautés tant universitaires qu’industrielles.

Pour finir, je proposerai quelques réflexions et approches pour le financement de recherches telles que celle-ci.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.