Jean-Raymond Abrial, Z, Socrate, B, Event-B, Rodin

Les 16 cas de relations binaires avec les papygrammes, NIAM, Merise, UML, Z0, B, notation de E. Codd (schémas relationnels n-aires) et la notation Oc Habrias Henri Henri.Habrias@univ-nantes.fr   1 Notation Z0, B, etc . — La notation créée par J.R. Abrial a évoluée au cours du temps. Il y eu les premiers écrits d’Abrial sur Z , puis après son séjour à Oxford , la notation décrite par J.M. Spivey dans La Notation Z (traduction française de Michel Lemoine, Masson). En ce qui concerne la notation des relations, celle de B est la même que celle de Spivey pour les 16 cas que nous présentons. En pratique en B on donne la spécification d’une relation dans le sens le plus contraint. Par exemple, on préférera une fonction totale à la relation inverse qui serait une relation "quelconque". — Avec la notation NIAM, il n’y a que deux symboles, celui d’unicité (représenté par une ligne, comme dans la notation du modèle relationnel n-aire on souligne la clé de la relation-type) et celui d...

  https://link.springer.com/content/pdf/10.1007/978-3-662-43652-3_1.pdf   https://abz-conf.org/publication/voisina14/ The Rodin Platform Has Turned Ten Laurent Voisin1 and Jean-Raymond Abrial2 1 Systerel, Aix-en-Provence, France laurent.voisin@systerel.fr http://www.systerel.fr 2 Marseille, France jrabrial@neuf.fr Abstract. In this talk, we give an historical account of the development of the Rodin Platform during the last 10 years. Keywords: Event-B, formal methods, tooling 

  https://www.academia.edu/143129452/Deux_crayons_Ontologie_ensembliste Abstract . Nous partons d’un énoncé d’Alain de Libera sur une situation dérite par Spade : ”j’ai devant moi deux stylos à bille noirs. Le point crucial est : combien de couleurs vois-je ? Deux réponses s’offrent. La première : je ne vois qu’une seule couleur (croire aux universaux), c’est le réalisme. A l’opposé, le nominalisme est caractérisé par celui qui voit deux noirceurs, autant que de stylos”. Nous montrons comment un langage de spécification formelle comme B permet de traiter la question. Abstract. We start with a statement by Alain de Libera on a situation Spade says: "I have two black ballpoint pens in front of me. The Crucial point is: how many colors do I see? There are two answers. The first: I see only one color (believe in universals), it's realism. On the other hand, nominalism is characterized by the one that sees two blacknesses, as many as pens". We show how a A formal specifi...

    Thierry Lecomte Clearsy et Jean-Raymond Abrial en 2014 au NNI à Tokyo   https://en.wikipedia.org/wiki/National_Institute_of_Informatics

  https://www.cs.utexas.edu/~EWD/ewd08xx/EWD879.PDF C'est Marc Guyomard qui m'a rappelé ce texte. Il l'avait quasiment gardé en mémoire. "Trip report London 14-17 févirer 1984" "The occasion was the Royal Society Discussion Meeting on Mathematical Logic and Programming Languages"   traduction Le chat : Après le déjeuner, la dernière session a été lancée par J.R. Abrial sur "La construction de programmes comme exercice mathématique". Il a souligné l'importance d'étudier "le cadre mathématique dans lequel chaque programme est supposé se comporter. [...] L'expérience montre que la quantité d'outils logiques et mathématiques à utiliser dans la construction de la plupart des programmes informatiques est assez faible." Il a listé les ensembles, fonctions, relations, nombres naturels, séquences et arbres. Je me suis trouvé en accord partiel, tout en ayant le sentiment de "Oui, mais...". Dans son discours, i...

 "The reason to treat two examples is because they have been drawn from vastly different fields: the one dealing with prime numbers is a so-called scientific application, the other, dealing with the idiosyncrasies of Flexowriters, is a so-called clerical application   These two fields are often regarded as completely foreign to each other : the successful application of the same discipline as illustrated below gives a strong support to the assumption that the difference between scientific and clerical machine usage is by no means an inherent difference, but more probably the result of a difference in intellectual level and professional training of the people engaged . "  pages 1-14 of Edsger W. Dijkstra, Selected Writings 0n Computing: A Personal Perspective, Springer-Verlag, 1982. ISBN O-387-90652-5 https://repositories.lib.utexas.edu/server/api/core/bitstreams/76936ac9-b135-4720-a20f-c399b8a320c9/conten t 

   Jean-Raymond Abrial (1938, 2025) Jean-Raymond Abrial died on May 26, 2025, the day before the conference held as part of the Scientific Days of the University of Nantes, which discussed his work and its application in various fields.    J.-R. Abrial was born in 1938 in Versailles. After studying at the Prytanée militaire de la Flèche, he attended the École Polytechnique.    In 1960 , he became a marine engineer. He received a French government scholarship at Stanford University and then at the French Navy Programming Center, where he worked on a version of the LTR (Real-Time Language) language. It was there that Gérard Le Lann, who was part of the team that designed the Internet, met him. For him, J.-R. Abrial is "one of the greatest French computer scientists! He is reluctant to embrace the "fashions" that more or less regularly shake up scientific communities. Freedom to think, to create, and freedom to spread! "     In Grenoble, at a univer...

Managing the Construction of Large Computerized Systems Prof. Jean-Raymond Abrial The subject mentioned in the title of this short article does not seem, at first glance, to be a genuine research subject . Although there are, from time to time, some famous breakdowns of large computerized systems as, for instance, recently at SBB in Zurich, it seems nevertheless that these systems are working nowadays in a satisfactory fashion. As a consequence, their construction process must have been mastered, otherwise such disasters would have occurred more frequently. This was clearly the case at the beginning of last century with an emerging technology such as avionics. There were lots of crashes due to the fact that people did not know how to construct good airplanes. The main reason for this was that they did not understand yet the theory of flight mechanics, which was in its infancy. In our case, however, the situation is a bit different from that of early avionics in that there is no cl...

 "Dans La Nausée, un personnage dit que l'autodidacte est celui qui s'instruit par ordre alphabétique.   - Supere aude ! "  p. 137, Pierre Assouline, L'annonce, Gallimard, 2025       https://fr.wikipedia.org/wiki/Sapere_aude     Je suis bien un autodidacte en informatique. J'ai commencé par Z de Jean-Raymond Abrial et j'ai fini par B du même Jean-Raymond Abrial !  Ce qu'on appelle l'ordre alphabétique inverse. https://www.canalacademies.com/emissions/le-sens-des-mots/mot-pour-mot/dictionnaires-et-si-lon-prenait-lordre-alphabetique-a-lenvers     Si vous n'avez pas la nausée, je peux vous en fournir un peu : https://fr.wikipedia.org/wiki/La_Naus%C3%A9e  

  https://www.sciencedirect.com/science/article/pii/0898122175900115   " SETL est un langage de programmation de très haut niveau basé sur la théorie mathématique des ensembles . Il a été à l'origine développé près Jacob T. Schwartz au Courant Institute of Mathematical Sciences de la NYU . Il existe une variante nommée ISETL (de l'anglais Interactive SET Language ) permettant de faire de la programmation sur des ensembles mathématiques . SETL fournit deux types de données de base : Les ensembles non ordonnés et les suites (appelées également tuples ). Les éléments des ensembles et des tuples peuvent être de n'importe quel type arbitraire, y compris les ensembles et les tuples eux-mêmes. Les fonctions sont fournis en tant qu'ensembles de paires (c.-à-d., tuples de longueur 2) et peuvent avoir des domaines et de codomaines de types arbitraires. Les opérations primitives dans SETL incluent, entre d'autres, l'appartenance ensembliste, l'union,...

 Constructing the Reals from the Integers (an Exercise in Mathematical Methodology) Jean-Raymond Abrial and Dominique Cansell Marseille and Lessy, France, EBRP Abstract . This paper contains a formal presentation of the construction of Real Numbers as proposed by various authors some years ago. One insists in presenting this mathematical work in a systematic fashion inherited from the usage of formal methods in system modeling. This work is a preparation for a complete mechanized development with a theorem prover. This work was done in 2012 and proved using Rodin in 2021 in the EBRP project. Some (little) errors are detected and corrected during the proof   Tout est ici : https://www.irit.fr/EBRP/wp-content/uploads/CA_real_V9.pdf  

 Ce qui suit est la retranscription des mots que j'ai adressés le jeudi 5 juin en hommage à Jean- Raymond Abrial devant sa famille et ses amis réunis. [Discours complété ici par quelques explications]. Je n'ai évoqué alors qu'une petite partie de ce que Jean-Raymond a apporté à l'informatique, que ce soit en France ou dans le monde. Mais j'ai voulu surtout montrer ce qu'il a apporté à ceux qui comme moi ont eu la chance de travailler avec lui, guidés par lui dans un espace informatique nouveau, l'espace en construction de ce qui s'appelle aujourd'hui les Systèmes d'Information. L'histoire, pour nous, a commencé l'hiver 1968. Le terme « nous» m'associe à deux étudiants fraîchement diplômés, l'un, Georges Beaume, comme moi licencié en Mathématiques Appliquées de l'université de Grenoble et le troisième, Robert Morin, diplômé Ingénieur de l'INPG . C'est en leur nom que j'ai parlé, mais aussi en celui de tous ceux qui ...

  https://www.patstec.fr/MEDIAS/005-005-000014010/8148.pdf SGBD (Système de Gestion de Base de Données) CLIO – Définition et manipulation de données – 1990. Document pour travaux dirigés d’étudiants à Grenoble. Ce document est disponible dans la collection de l’ACONIT, Association pour un conservatoire de l’informatique et de la télématique, Grenoble, fiche n°24639-04 Auteurs : C. Collet, M.C. Fauvet Document de 27 pages. Edition : IMAG – Institut de Mathématiques Appliquées de Grenoble, Travaux dirigés pour la Maîtrise de Sciences et Techniques (cours ESI2) Date : 12 Décembre 1990. Le logiciel CLIO, objet de ces travaux dirigés pour étudiants, est un SGBD (Système de Gestion de Base de Données) qui est une version dérivée du SGBD appelé SOCRATE, inventé en 1970, à l’Université Scientifique et Médicale de Grenoble, par l’équipe de Jean-Raymond Abrial. SOCRATE avait été ensuite industrialisé par la SSII française ECA-Automation. ECA-Automation a été rachetée en 1983 par Thomson-CSF ...

 Frege in  Frege Gottlob, Ecrits logiques et philosophiques, Traduction et introduction de Claude Imbert, Points, Essais, Seuil, 1971, ISBN : 2-02-022966-2, page 75   https://fr.wikipedia.org/wiki/Gottlob_Frege   https://www.normalesup.org/~sage/Reflexions/Sciences/GFlogiPhil.pdf  

 Collecté par Henri Habrias  JS 2025, Journées Scientifiques de l'université de Nantes 27 mai 2025  " [...] les mathématiques sont une science où l'on ne sait jamais de quoi on parle ni si ce que l'on dit est vrai" Bertrand Russell (1818) " [...] les mathématiques sont la seule science où l'on sait toujours de quoi l'on parle et où l'on est certain que ce que l'on dit est vrai " Emile Borel , après avoir cité B. Russell in Les grands courants de la pensée mathématique, dir. par Le Lionnais F. ,Hermann, 1997 1 Introduction, autour de la conférence de J.R. Abrial au Collège de France Le 1 avril 2015, Jean-Raymond Abrial, invité par Gérard Berry [1] dans le cadre du Séminaire : Prouver les programmes : pourquoi, quand, comment ? au Collège de France, a prononcé une conférence intitulée : Spécication, construction et vérification de programmes : le parcours d'une pensée scientifique sur une quarantaine d'années Il existe une versio...

    https://www.researchgate.net/publication/281884827_Application_d'ontologies_formelles_au_droit#fullTextFileContent Selon B. Bachimont, « Une ontologie est une représen- tation linguistique et formelle des concepts d’un domaine pour un contexte applicatif. L’aspect linguistique renvoie au fait que les concepts sont tirés de la langue du do- maine et doivent rester intelligibles pour les spécialistes. L’aspect formel renvoie au fait que les concepts doivent être manipulables par la machine et produire un compor- tement prédictible. » et, en paraphrasant Gruber (7) on peut dire qu’une ontologie formelle est une « spécification for- melle d’une conceptualisation ». Cet article rapporte une expérimentation d’une telle « ontologie formelle » avec le langage B (1; 10) qui utilise la logique des prédicats du premier ordre et la théorie des ensembles. Nous avons choisi B de préférence à un autre langage comme KIF (6) parce que B utilise la puissance de la théorie des en- sembles ...

 Henri Habrias (ancien professeur à l'IUT de Nantes) assisté de Marc Guyomard (ancien professeur à l'ENSATT de Lannion)   Une histoire des concepts, méthodes et outils du génie logiciel du IVe siècle av. J.C. à juin 2025. Par une bibliographie chronologique, avec citations d'auteurs, et un focus sur les travaux de Jean-Raymond Abrial et les méthodes formelles. Index des concepts, méthodes et outils et des noms cités, 92 pages.   https://www.researchgate.net/publication/394026329_Event-B_et_la_plateforme_Rodin   A l'occasion des JS2025 Conférence  J.R. Abrial, un pionnier du développement scientifique des langages informatiques et des méthodes formelles et de leur application à grande échelle dans l’industrie, 27 mai 2025  

 Jean-Raymond aimait lire Nicolas Bouvier. Moi aussi. La dernière fois il m'avait parlé de Poisson scorpion. https://fr.wikipedia.org/wiki/Le_Poisson-scorpion   Et je viens de retrouver Chronique japonaise , Petite Bibliothèque Payot. Et sur la couverture une estampe de Hokusai. Alors que je viens de visiter l'expo Hokusai au château des ducs de Bretagne, à Nantes, dans les "Pays de la Loire".  Quelle merveille !  Je ne vais pas vous en faire des citations ! je citerai tout le livre. 

Les actes sont ici :    https://hal.science/hal-04975370/document Présentation ”L’école a pour vocation la dissidence, ce qui ne se conçoit qu’à étendre l’espace du lisible et à élargir celui du discutable.” Alain de Libera, Penser au Moyen Age, Seuil, p. 108 La première conférence B a eu lieu à Nantes les 25-26-27 novembre 1996, après la conférence ZB de Nantes les 10-15 octobre 1995. Elle a été suivie des conférences de Montpellier, York, Grenoble, Turku, Guilford, Besançon. La prochaine aura lieu à London en septembre 2008. A l’occasion des conférences de Montpellier et de Grenoble, des sessions éducation ont eu lieu. Les actes en ont été publiés. L’association APCB a organisé des journées à Paris et à Nantes. Celle de Nantes a été consacrée `a l’enseignement. Mais depuis quelques années, il n’y a pas eu de conférence consacrée à l’enseignement. Les travaux de recherche en génie logiciel doivent conduire à la pratique. Et pour cela, il faut passer par l’enseignement, enseig...

 J.-R. Abrial, “Extending B without Changing It (for Developing Distributed Systems),” 1st Conference on the B method, Putting into Practice Methods and Tools for Information System Design, Institut de Recherche en Informatique de Nantes, 1996, pp. 169-190   https://www.academia.edu/127625923/Extending_B_without_Changing_it_for_Developing_Distributed_Systems   Attention ! vous allez lire " By Habrias Henri   J'ai tenté de faire supprimer ça en vain. Il n'est pas facile de "verser" un article sur Academia.edu quand on n'en est pas l'auteur.   

 "One of the first discoveries of the research by the Z team was the necessity of separating small chunks of formal material by paragraphs of informal prose, explaining the relationship between the formal symbols and reality, and motivating the decisions that are captured by the formalisation. The drafting of the informal prose was even more difficult to teach, learn and practice than the mastery of mathematical notations and concepts. "   C.A. R. Hoare, Préface à VDM'90, VDM and Z - Formal Methods in Software Developemnt, LNCS,  ISBN 3-540-52513-0

  At the Vertou Stadium    1.1 First Morning  The wind was favorable. The BN (Biscuiterie Nantaise) factory offered us delicious smells of biscuits. And Guy answered our questions while my grandson was at French soccer practice.    H.H.: You met J.R. Abrial when you did a training course at CEPIA on the Domaine de Voluceau in Rocquencourt. What year was that?      G.L.: In October 1985.   H.H.: I was also there in October and in the spring. We could have met there. But we didn't know each other yet. What did you like about it then?      G.L.: Strong point: instead of vainly trying to prove a problem on any program, we start by creating a specification that can be proven, then we focus only on programs implementing the specification.      H.H.: J.R. Abrial thanks you in the B-Book for your contribution. Tell me about it.      G.L.: I used to work at INSEE on Boulevard Adolphe-Pinard in ...