Posts

J.-R. Abrial, Foreword of the book "SPECIFICATION CASE STUDIEs" edited by Ian Hayes

 Foreword of the book "SPECIFICATION CASE STUDIEs" edited by Ian Hayes Reading formal texts is like meeting people. Sometimes, you understand them straightaway like good friends who take to each other immediately. At other times, it is more difficult. You may parse what you read, but find it impossible to work out any meaning. With the latter, you have to be patient, ask questions, explore the surroundings; in other words, it is better for you to be introduced through some common good friends who volunteer to help you prepare for the first meeting. Large computer programs, to say the least, pertain to the category of formal texts whose meanings are not immediately obvious! For that reason, people have been trying – for some time – to find out what kind of intermediate text would be best suited to play the role of go-between. This book reports on experiments made at Oxford University within this frame- work: it shows how one may communicate ideas and meanings about existing (o...
Post a Comment
Read more

SPECIFICATION CASE STUDIES, Edited by Ian Hayes

    https://staff.itee.uq.edu.au/ianh/Papers/SCS2.pdf SPECIFICATION CASE STUDIES Second Edition Copyright c© 1987, 1992 Prentice Hall International (UK) Ltd Appendices A and B may be copied for educational purposes. Edited by Ian Hayes With Contributions by Bill Flinn Roger Gimson Steve King Carroll Morgan Ib Holm Sørensen Bernard Sufrin ii Contents I Tutorials 1 1 Small examples of specification using mathematics 3 Ian Hayes 1.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.2 A symbol table . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.3 File update . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.4 Sorting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 1.5 Solutions to exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 2 Block-structured symbol table 13 Ian Hayes 2.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.2 Sy...
Post a Comment
Read more

" Specification Models " Ian J. Hayes

Image
Post a Comment
Read more

"Extending B without Changing It (for Developing Distributed Systems),” J.-R. Abrial, 1st Conference on the B method

Image
   
Post a Comment
Read more

The 20th International Symposium on Theoretical Aspects of Software Engineering July 4 - 6, 2026, Shanghai, China

  https://tase2026.github.io/c_cs.html With a celebration of JRA, including a 15-minute talk by Jonathan Bowen 17:00-18:00 Gedenkschrift for Jean-Raymond Abrial
Post a Comment
Read more

Why might we teach "Formal Methods" informally? And to whom? And when? Carroll Morgan

 BCS-FACS Online SeminarDate and time Thursday 25 June, 11:00 am - 1:00 pm Location Online Free registration < https://www.bcs.org/events-calendar/2026/june/hybrid-why-might-we-teach-formal-methods-informally-and-to-whom-and-when/ > Note that this event is online only. Timetable 11:00 am - Talk 12:00 pm - Questions and answers 1:00 pm - Event closes Seminar Details Title: Why might we teach "Formal Methods" informally? And to whom? And when? Speaker: Carroll Morgan Abstract: Formal Methods (for computing) was enabled by Hoare's “An axiomatic basis for computer programming” in 1969, where Formal meant “in the sense of formal logic”, i.e. reasoning based on manipulation of symbols which themselves had no intrinsic meaning (in the sense of Hilbert). Hoare's paper had itself been enabled by Floyd's “Assigning meanings to programs” just two years earlier, whose informal message might well have been -- in retrospect at least -- “Don...
Post a Comment
Read more

Jean-Raymond Abrial: A Scientific Biography of a Formal Methods Pioneer

Jonathan Bowen, Henri Habrias Abstract: Jean-Raymond Abrial is one of the central figures in the development of formal methods for software and systems engineering. Over a career spanning more than five decades, he has played a decisive role in the creation of the Z specification notation, the B-Method, and Event-B and in demonstrating their applicability to large-scale industrial systems. This article presents a scholarly biographical account of Abrial’s life and work, tracing the evolution of his ideas from early work on real-time languages and databases, through foundational contributions to formal specification, refinement, and proof, to the development of industrial-strength tool support such as the Atelier B and the Rodin platform. The article situates Abrial’s contributions within their historical, intellectual, and industrial contexts and assesses their lasting impact on software engineering and formal reasoning about programs.   Published in: IEEE Annals of ...
Post a Comment
Read more