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

  We searched for it for over a year, in France and elsewhere. Dominique Cansell has found the TSI issue number. We will tell you how to access it.   http://dominique.cansell.free.fr/JRA-TSI-1984.pdf   "Spécifier ou comment matérialiser l'abstrait" Jean-Raymond Abrial, 1984 TSI 0752-4072/84/03/201-19 AFCET-Bordas Illustration with an example. For people interested into the genesis of B  

 cité par Hubert Haddad in Le nouveau magasin d'écriture,  Editions Z, Zulma Vous êtes bien sur un blog consacré entre autres à Z ! Je vous conseille ce livre, 939 pages. A éviter au lit, il est trop lourd.     Quoted by Hubert Haddad in *Le nouveau magasin d'écriture*, Editions Z, Zulma You're definitely on a blog dedicated, among other things, to Z! I recommend this book, 939 pages. Avoid reading it in bed; it's too heavy.     Alors n'hésitez pas à critiquer, corriger les billets de ce blog. So feel free to criticize and correct the posts on this blog.  

 Abrial, JR. (2003). B # : Toward a Synthesis between Z and B. In: Bert, D., Bowen, J.P., King, S., Waldén, M. (eds) ZB 2003: Formal Specification and Development in Z and B. ZB 2003. Lecture Notes in Computer Science, vol 2651. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44880-2_12 In this paper, I present some ideas and principles underlying the realization of a new project called B # . This project follows the main ideas and principles already at work in B, but it also follows a number of older concepts developed in Z. In B # , the intent is to have a formal system to be used to model complex system in general, not only software systems.  https://link.springer.com/chapter/10.1007/3-540-44880-2_12  

 On trouve des choses étonnantes sur la Toile. Je ne devrais pas m'étonner. J'ai bien enregistré un document où j'appelle Papygram ce qui est un diagramme sagittal ou arrow diagram ou mapping diagram . J'avais fait confiance à un collègue professeur de maths qui m'avait nommé ainsi ces diagrammes. Et j'avais plaisir à faire connaître monsieur et madame Papy, mathématiciens belges sur lesquels Dieudonné avait écrit. Le papygram ce ne sont pas deux patates avec des flèches allant de l'une à l'autre, mais une grosse patate avec des éléments dans la patate qui sont reliés par des flèches. C'est une autre représentation des relations.  Cette correction étant faite, revenons à notre découverte.  Voici ce que je viens de trouver. Le texte est un bel hommage à Jean-Raymond Abrial. Mais l'auteur parle de Jean-Marie Charles Abrial. Je comprends pourquoi il arrive que les "IA" nous étonnent. Notez que sur la page que je colle ci-dessous, dans une...

  https://www.atelierb.eu/en/presentation-of-the-b-method/b-and-its-different-languages/ This page lists various terms that relate to the so-called “B formal method”. As the B method evolves, some common terms lose their original meaning. We feel the need to complete some definitions already given on Wikipedia   Merci Clearsy pour cette page que nous reproduisons ici avec quelques liens B B evokes, in the field of formal methods, the “B” language, the “B” method, the reference book: the B Book. Its ancestor is Z, a specification language based on mathematical notations. B also includes refinement and proof, two techniques that are an integral part of B. B LANGUAGE A language referring to set theory and predicate logic, also including a syntax for describing “substitutions”, operations, and links between machines, refinements and implementations. The description of the language and that of the refinement and ...

 Abrial, JR. (2018). On B and Event-B: Principles, Success and Challenges. In: Butler, M., Raschke, A., Hoang, T., Reichl, K. (eds) Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2018. Lecture Notes in Computer Science(), vol 10817. Springer, Cham. https://doi.org/10.1007/978-3-319-91271-4_3 " 2.1 Differences One of the main differences between B and Event-B concerns operations (in B) and events (in Event-B). Each operation in B is usually defined together with a pre-condition containing a predicate that must be true for the operation to be able to be called. On the other hand, each event in Event-B is usually defined together with a guard containing a predicate that must be true for the event to be able to occur. 2 This results in having both pre-conditions or guards being assumptions when doing a proof on an operation or on an event (e.g. invariant preservation proofs). So far thus, there are no differences between the two. However, both diffe...

 2013 From Z to B and then Event-B : Assigning Proofs to Mea- ningful Programs, J.-R. Abrial. E.B.Johnsen, L. Petre (eds) Integrated Formal Me- thods. IFM 2013. Lecture Notes in Computer Science, vol 7940, pp. 1-15 https://doi.org/10.1007/978-3-642-38613-8_1   Cet article est très proche de l'exposé que fera en français Jean-Raymond Abrial au Collège de France le 1e avril 2015 https://www.college-de-france.fr/fr/agenda/seminaire/prouver-les-programmes-pourquoi-quand-comment/specification-construction-et-verification-de-programmes-le-parcours-une-pensee-scientifique-sur-une   This article is very close to the presentation that Jean-Raymond Abrial will give in French at the Collège de France on April 1, 2015 From Z to B and then Event-B: Assigning Proofs to Meaningful Programs Jean-Raymond Abrial Marseille, France jrabrial@neuf.fr The very first paper on Z [1] was published in 1980 (at the time, the name Z was not “invented”), then the book on the B method [2] was publish...

 Stevens, N., Hoffmann, A. L., & Florini, S. (2021). The unremarked optimum: whiteness, optimization, and control in the database revolution. Review of Communication , 21 (2), 113–128.  https://doi.org/10.1080/15358593.2021.1934521 https://www.tandfonline.com/doi/full/10.1080/15358593.2021.1934521   " ABSTRACT The 1970s saw major transformations in how computerized databases were conceived, developed, and designed. Part of a broader shift in how software applications were developed, these transformations—sometimes referred to as “the database revolution”—introduced new and then-novel approaches to structuring and arranging digital data, optimizing them for usability and convenience. At the same time, however, the rhetoric of innovation and revolution surrounding this moment in database development obscures the ways it helped concentrate and extend particular kinds of racialized power and, in particular, whiteness (i.e., those norms and values congenial to ...

  https://english.ecnu.edu.cn/content.jsp?urltype=news.NewsContentUrl&wbtreeid=1599&wbnewsid=1870 Jean-Raymond Abrial, a world-famous French computer scientist who is the enabler of Shanghai’s first driverless metro train, won the International Scientific and Technological Cooperation Award of the People’s Republic of China in Beijing on Jan. 9. Of the five foreign scientists winning the honor at the Great Hall of the People, Abrial is the only one who cooperates with a Shanghai partner - ECNU. Shanghai’s first automated metro train "1701", just arrived at Zhujiajiao depot in Qingpu recently, and is scheduled to be put on trial operation on Line 17 at yearend.  The credit should be given to Abrial, who develops the industry-level safety-critical software systems for driverless train in partnership with ECNU’s School of Computer Science and Software Engineering. A professor at Swiss Federal Institute of Technology in Zurich and a member of European Acade...

  https://en.wikipedia.org/wiki/Xidian_University   https://oice.xidian.edu.cn/info/1010/2013.htm   "   On the morning of the 11th, Professor Abrial delivered an academic report entitled "Software and System Developments Using Formal Models, Refinements, and Proofs with Event-B" in classroom 608 of the North Campus. In his report, Professor Abrial introduced the role of formal modeling methods in system development, comparing it with UML, and emphasizing the solid semantic foundation behind Event-B. He then discussed the role of Event-B in relation to the Rodin platform he initiated in recent years, demonstrating its application scenarios with practical examples. In the afternoon of the 11th, a formal methods academic seminar was held in the Software Institute conference room A918 of the old Science and Technology Building on the North Campus. Faculty and students from the Software Institute, as well as Professor Duan Zhenhua, Associate Professor Tian Cong, a...

  https://www.youtube.com/watch?v=GGSYlBYidXc This is the Keynote titled "An Exercise in Mathematical Engineering: Stating and Proving Kuratowski Theorem" by Invited Speaker Jean-Raymond Abrial (Chair: Camilo Rueda) ICTAC2015   researchr explore calendar search You are not signed in Sign in Sign up External Links DOI DBLP Google Google Scholar MSAS Cite Key Abrial15 Statistics References: 0 Cited by: 0 Reviews: 0 Bibliographies: 0 PDF [Upload PDF for personal use] Researchr Researchr is a web site for finding, collecting, sharing, and reviewing scientific publications, for researchers by researchers. Sign up for an account to create a profile with publication list, tag and review your related work, and share bibliographies with your co-authors. An Exercise in Mathematical Engineering: Stating and Proving Kuratowski Theorem Jean-Raymond Abrial . An Exercise in Mathematical Engineering: Stating and Proving Kuratowski Theorem . In Martin Leucker , Camil...

  https://jean-raymond-abrial.blogspot.com/2025/07/jean-raymond-abrial-1938-2025.html

  At the upcoming SBMF 2025 International Conference ( https://sbmf2025.ufrpe.br/ ) to be held in Recife, Brazil (2–5 December 2025), Metrópole Digital - IMD/UFRN and CLEARSY will present their latest joint work on the formal verification of C code generated from B models. Our paper, “Bridging the B-Method and ACSL: Towards Verified C Code,” explores how to strengthen the trust in automatically generated software — a key issue for safety-critical systems. While the B-Method guarantees correctness of the specification and implementation models, ensuring that its generated C code still adheres to these properties remains a challenge. To address this, we propose a systematic generation of ACSL assertions from B models. ACSL is the specification language used by Frama-C ( https://frama-c.com/ ), enabling formal verification of C code. This approach bridges formal design and static analysis, allowing engineers to verify that critic...

Click on the image to read   https://jean-raymond-abrial.blogspot.com/2025/11/specifier-ou-comment-materialiser.html

Technique et Science Informatique, vol.3,n°3, 1984  Cet article est introuvable. Je me suis souvenu que je l'avais utilisé dans mon livre "Introduction à la spécification". Tout n'est pas perdu ! This article is no longer available. I remembered that I had used it in my book "Introduction to Specification". All is not lost! J'avais conservé la présentation de l'article, la voici : Click on the images to read the text   I had kept the article's presentation; here it is:     Le livre et l'avant-propos de Michael Jackson.  The book: and the foreword by Michael Jackson .     Voici les deux premiers paragraphes de l'article : Here are the first two paragraphs of the article :              

henri.habrias@univ-nantes.fr      " une question se pose alors. Où J.-R. Abrial a-t-il appris à utiliser ces mé- thodologies "projet" ? Un premier niveau de réponse est donné par Abrial qui écrit (dans une réponse à J. Ricodeau)    "Dans la Marine nous avions initialisé cette approche". Il y aurait donc eu transfert de savoir-faire entre la Marine Nationale et l'IMAG. On vient de voir que dans cette méthodo- logie il y a une insistance marquée sur la phase de "spécification". Peut-on avoir un second niveau de questionnement sur ce point précis ? En quoi la Marine aurait-elle pu avoir des dispositions spécifiques pour mettre ainsi en avant la phase de spécification ? La réponse nous semble être que "la Marine" y est disposée parce que, très tôt dans son histoire dès l'année 1676 du temps de Colbert, la Marine a appris à spécifier, en commençant par ce qui concernait les "toiles" (a) pour les voiles de navires" (b) J...

  https://velo.wiki.ls2n.fr/lib/exe/fetch.php?media=undefined:tsi-v22n1-2004-bpresent-futur-recherche-ens.pdf   B : passé, présent, futur Jean-Raymond Abrial Published in Techniques et sciences… 1 February 2003 Abstract Cet article est une presentation non technique, mais rigoureuse, de la methode B. Il s'adresse aux lecteurs qui ont entendu parler de B et qui souhaitent en savoir davantage. Il indique quelle est la demarche initiale de B et sa raison d'etre, c'est-a-dire la modelisation de logiciels et plus generalement des systemes. Il precise ensuite ce qu'est un modele et decrit les concepts importants de la methode, a savoir le raffinement, la decomposition et la genericite. La methode B permet d'envisager les modeles sous deux aspects: la vision locale et la vision globale. Le deuxieme aspect utilise une nouvelle facon d'ecrire le B, appelee B-evenementiel. La correction des logiciels produits par la methode B est assuree par des preuves mathem...

Ouvrages publiés sur Z Henri Habrias henri.habrias@univ-nantes.fr  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 cap- tured 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.  Tony Hoare 1 En anglais   1.1 Bibliographie Z  Dans Nicholls, ed., Z User Workshop, York, 1991, Springer-Verlag, 1992, on trouvera une bibliographie en partie commentée de 299 références d'articles et de livres sur Z. Bristish Computer Society (BCS) Institution of Electrical Engineers ( EEE), Numéro Spécial sur Z, Software Engi- neering Journal, vol n°4, n°1, January 1989. A noter que le nom de J.R. Abrial n'y apparaît pas. 1.2 Revue et livres  J.M. Spivey, Understanding ...

  https://velo.wiki.ls2n.fr/lib/exe/fetch.php?media=velo:programmation_statique_z_-_bm.pdf Static Programming, The Z Language (Excerpt from the book Programming Methods)   Programmation statique, Le Langage Z Extrait du livre Méthodes de programmation, Bertrand Meyer, Claude Baudoin, Collection de la Direction des Études et Recherches d’Électricité de France, Eyrolles, 1978, ISBN-10 : 221201581X "Méthodes de Programmation (Programming Methodology), Eyrolles, Paris, 1978; third revised edition, 661 pages, 1984. Translation: Russian (Mir Publishing )   Histoire de ce livre par B. Meyer ( https://se.inf.ethz.ch/old/people/meyer/publications/ ) " We wrote this book fresh out of school and managed to convince the publisher to include everything (other publishers wanted us to trim it down to 250 pages). It is a compendium of programming methodology, programming techniques, fundamental algorithms and data structures. It emphasizes program correctness, through assertion techniqu...

  April 1984 IEEE Transactions on Software Engineering SE-10(2):128 - 142 DOI: 10.1109/TSE.1984.5010215 Source IEEE Xplore Abstract A specification of the UNIX filing system is given using a notation based on elementary mathematical set theory. The notation used involves very few special constructs of its own. The specification is detailed enough to capture the filing system's behavior at the system call level, yet abstracts from issues of data representation, whether in programs or on the storage medium, and from the description of any algorithms which might be used to implement the system. The presentation of the specification is in several stages, each new stage building on its predecessors; major concepts are introduced separately so that they may be easily understood. The notation used allows these separate stages to be joined together to give a complete description of each filing system operation-including its error conditions. Features of the specification nota...

 Brien, S. (1994). The Development of Z. In: Andrews, D.J., Groote, J.F., Middelburg, C.A. (eds) Semantics of Specification Languages (SoSL). Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3229-5_1   Z is a model-oriented specification language, which originated in the early 1980s. The first description by Abrial included a structuring mechanism called a class, which was very similar to a schema (i.e. a combination of a declaration and a constraining predicate). The Z style has developed as a result of tackling practical examples and adapting the notation to their needs; this has resulted in a style and notation that is widely applicable to the description of certain kinds of computer system, particularly the client-server model. With the publication of Sufrin’s Z Handbook the development and understanding of Z had progressed. A type inference system and rules for reasoning were provided and the notions of schem...