Bertrand Meyer

See http://bertrandmeyer.com/about

A paean to programming

by

A Google search for something entirely unrelated led me to a very old issue of the Daily Nexus, the student newspaper of the University of California, Santa Barbara, where I was teaching back then.  Apparently (I had forgotten all about it of course) I was piqued by a student’s letter to the editor, where he complained of having to sit all day hacking at a terminal just because he had been told to study computer science to get a high-paying job.  I felt compelled to write a response (published on 24 April 1984 under the editor-provided title “Monster”) affirming that CS is not all about money.

My letter appears below, copy-pasted in full. The nice thing about it is that I would write it in exactly the same way today. The scary thing about it is that I would write it in exactly the same way today! Well, actually, let me qualify that: I would replace “which” by “that” in the second paragraph, and in the penultimate one I would not separate the verb  “convey” from its complement. So it is good to know that in forty-one years minus one day I have learned at least two things.

From: UCSB Daily Nexus, 24 April 1984, page 3, available here.

Monster

Editor, Daily Nexus:

In a letter published in the April 17 Nexus, Paul Dechant complains that he must sit “night after night” in the terminal room instead of devoting his time to more gratifying occupations. I checked my lists: he is not in any of my classes. Good; nobody likes to feel like a monster…

The part of his letter that worries me more, however, is the question which he asks: “Is this the price I must pay for a decent grade in a major which promises a healthy salary?” I appreciate Dechant’s frankness, and I have no doubt that it reflects a common view of what majoring in Computer Science is all about, but still, I find this definition bothering. Is it really so that the only argument for choosing a scientific or engineering major is the prospect of making big bucks? How sad! There is so much more to it.

How about intellectual challenges? I may have some ground to speak about this, since as a student I was what in the U.S. would be called a double major, and got degrees both in science and the humanities. I can testify that the choice between the two is not a matter of greed alone; the borderline between “vocational” and “educational” is not that clear. There is cultural value in science, too! The sheer excitement of entering a new scientific field like computer science, where so much remains to be discovered, is my view of a good enough motivation. By the way, one of the challenges that people in my field (software engineering) are tackling has something to do with Mr. Dechant’s frustration: does programming have to be such a trauma? Can we find a way to deal with problems so that people don’t have to sit “night after night” to get their programs running? In fact, some of our teaching is already concerned with this. It’s called programming methodology and I am sure it can help.

Now think about what computers really are: one of the most fabulous kind of machines ever devised by mankind, but different from all the machines invented before in that they can solve not just one problem, but any problem which is presented to them, provided the problem and the solution technique can be described in complete detaiI. A computer is thus more of a “meta-machine,” and computer science is really the science of problem-solving. How do we master this power and put it to good use? Doesn’t this present some challenges worthy of devoting part of your life to them? I think it does and I hope some of my teaching is able to convey, however imperfectly, this excitement.

There is nothing wrong in considering the potential financial rewards when choosing a major. I would hate to think, however, that all our students are sitting there just because they or their parents have read in Time or Fortune magazine that one may get rich by going into software.

Bertrand Meyer

Visiting Professor

Computer Science Department

New article: obituary of Niklaus Wirth

by

Bertrand Meyer: Obituary for Niklaus Wirth, in Formal Aspects of Computing, volume 37, issue 2, pages 1-11, published 3 March 2025, available here (publisher’s site).

Shortly after Niklaus Wirth — Turing Award winner for his many seminal contributions including Pascal, Algol W, Modula, virtual machines, Lilith/Ceres, railway diagrams, PL/360, seminal textbooks…  — passed away last year, I wrote a long blog article about him. Jim Woodcock, editor of Formal Aspects of Computing, asked me to adapt it for the journal. The result has just been published.

It is not a traditional eulogy; rather, a free-ranging discussion of Wirth’s achievements and my personal analysis of his ideas. Wirth’s career is well-documented elsewhere; my article does not replace encyclopedia entries (or the many talks by Wirth and interviews of him available for example on YouTube), but is more like one side (sadly) of a dialog on programming, languages, methods, tools and the evolution of our common discipline.

Its appearance in Formal Aspects of Computing is apposite: even though Wirth would probably not have characterized himself as a formal methods person, he did work with Tony Hoare on axiomatic language specifications, and all his work shows  the same kind of precision and rigor that characterizes formal methods work. I hope my account of his contributions will help make them better known and perpetuate his memory.

Reminder: my full annotated publication list is here.

New preprint: Lessons from Formally Deployed Software Systems

by

Li Huang, Sophie Ebersold, Alexander Kogtenkov, Bertrand Meyer and Yinling Liu, Lessons from Formally Verified Deployed Software Systems, submitted for publication (since March 2023), preprint available here for the full version (with detailed review of all 32 projects) and here for a shorter one (with same core content but only 11 detailed reviews, the others summarized in a table).

Formal methods of software construction, using mathematical techniques to ensure their correctness and (whenever possible) to prove it using automatic tools, now have a long history but they remain controversial. Questions linger, in particular, on their applicability in an industrial setting. This is the kind of question with opinions galore but limited published evidence. This article is a detailed survey of 32 formally-verified industrial systems, intended to provide firm data on the state of application of formal methods to industry —successes, challenges, limitations, lessons.

The paper resulted from an attempt to identify as many  such formally-verified systems actually deployed in industry as possible. Some of the projects were selected thanks to a questionnaire that we sent out to many forums; others were found through a variety of sources. Out of many initially identified projects the articles covers 32; other than interest and relevance, the criteria for selection included our ability to find detailed information about them and verify that information. Whenever possible we used published accounts, but for some of the most interesting systems deployed in industry little is available in the literature; we only retained those for which we could get and validate information from the projects themselves, over the course of many interactions.

The article is focused on facts and figures, not opinions. Although the authors are actively engaged in using formal methods, we have no axe to grind, if only because we know, from that very practice, what the challenges are. The article is neither for formal methods nor against formal methods; it helps readers form their own opinions by providing a wealth of carefully verified information about projects that have applied formal verification in an industrial setting. I can safely assert that there is no comparable body of work available anywhere; while there have been excellent surveys of formal methods and software verification before (the article has a dedicated section in which it reviews many of them), none has gone into the present study’s level of detailed study and analysis of actual projects, much of which not available anywhere else (particularly in the case of information gleaned from interacting with the project members themselves but not previously published).

I believe therefore that this study deserves to be known by anyone interested in software verification and formal methods. There are two versions: the long version contains the description of all selected 32 projects. The short one, cut to the page limit of the intended journal (see next) has these details for only 11 systems, chosen to be representative (typically, one example for each general category, e.g. compilers); the properties of the others are summarized in a table. The introduction, overview, general analysis, discussion and conclusions are the same, so if you just want to get an overall idea you can start with the short version.

Presenting the article as a “new preprint” is somewhat of a twist since its first version was available in March of 2023 and the current version is from last October. The paper has been under review for ACM Computing Surveys for over two years; this is not the right place to complain about the process, but let me politely say that we are a bit frustrated since on our side we did all that was requested. (I am thankful to Moshe Vardi who, alone of all people whom I solicited for help, managed to get something moving at some point.) Given the way things have been going and even though the authors did everything requested of them I would not bet that it will eventually be published; if nothing else, the more time passes the more self-fulfilling becomes the criticism of obsolescence. The study took a full year (2022), and the initial version was submitted in March 2023. All information on the selected projects was carefully checked and updated a year later (February 2024), but no new projects were added then. So the article is not meant to be the last word for eternity; rather, it presents of snapshot of the state of the art at one particular moment. In this role — and whether it ends up published or forever remains Samizdat — I hope it will be useful.

 

Reminder: my full annotated publication list is here.

New preprint: Seamless and Traceable Requirements

by

Maria Naumcheva, Sophie Ebersold, Jean-Michel Bruel and Bertrand Meyer, UOOR: Seamless and Traceable Requirements, submitted for publication, February 2025, preprint available on arXiv.

This article grew out of Maria Naumcheva’s PhD thesis defended on December 18 at the University of Toulouse (I will write separately about the thesis as a whole). It is part of a general effort at systematic requirements engineering, reflected in earlier articles by the some or all of the same group of authors (see my publication list) and in my requirements book. Here is a short version of the abstract for the article:

In industrial practice, requirements are an indispensable element of any serious software project. In the academic study of software engineering, requirements are one of the heavily researched subjects. And yet requirements engineering, as practiced in industry, makes shockingly sparse use of the concepts propounded in the requirements literature.

The present paper starts from an assumption about the causes for this situation and proposes a remedy to redress it. The posited explanation is that change is the major factor affecting the practical application of even the best-intentioned requirements techniques. No sooner has the ink dried on the specifications than the system environment and stakeholders’ views of the system begin to evolve.

The proposed solution is a requirements engineering method, called UOOR, which unifies many known requirements concepts and a few new ones in a framework entirely devised to accommodate and support seamless change throughout the project lifecycle. The method encompasses the commonly used requirements techniques such as scenarios, and integrates them into the seamless software development process. The work presented here introduces the notion of seamless requirements traceability, which relies on the propagation of traceability links, themselves based on formal properties of relations between project artifacts.

As a proof of concept, the paper presents a traceability tool to be integrated into a general-purpose IDE that provides the ability to link requirements to other software project artifacts, display notifications of changes in requirements, and trace those changes to the related project elements.

The UOOR approach is not just a theoretical proposal but has been designed for practical use and has been applied to a significant real-world case study: Roborace, a competition of autonomous racing cars.

Reminder: my full annotated publication list is here.

New preprint: Loop unrolling — formal definition and application to testing

by

Li Huang, Bertrand Meyer and Reto Weber, New preprint: Loop unrolling:  formal definition and application to testing, February 2025, submitted to publication. Available here on arXiv and also here.

Abstract

Testing coverage criteria usually make a gross simplification: they assume that loops will have their bodies executed 0 or 1 time. How much (specificall,y how many bugs) are we missing as a result?

This article defines loop unrolling formally (removing common misconceptions of the topic), shows how loop unrolling was applied to a testing framework (using program-proving techniques as well), in line with our test-and-proofs work of the past several years), and presents detailed empirical evidence about the effect on finding bugs.

(Some of the initial ideas were recorded earlier in an unpublished technical note.)

Reminder: my full annotated publication list is here.

New preprint: a standard framework for research on bugs and automatic program repair

by

Preprint of new article: Victoria Kananchuk, Ilgiz Mustafin and Bertrand Meyer, Bugfix: a standard language, database schema and repository for research on bugs and automatic program repair, submitted for publication, February 2025. Available on arXiv here. Also available here.

What this is in a nutshell (there is a longer abstract below): a proposal for, and first steps towards, helping work on Automatic Program Repair (APR) by providing a common framework, including: a language for describing bugs and fixes in a standard way; the same functionality available as an API (using JSON); and a repository (a database) accessible in that framework and containing  numerous bugs and fixes produced by researchers and practitioners.

The article draws on a short paper at the APR workshop of ICSE last year; I plan to use it as a basis for my keynote at the next workshop at ICSE in Ottawa on May 29. Rather than a paper describing firm results, this paper is meant to start a process; quoting from one of the final paragraphs:

The present work should be viewed as a community-service contribution: it is meant to help everyone interested in bugs and their automatic repair, particularly researchers in the field, to achieve new advances by relieving them of common and repetitive tasks, facilitating the assessment of new techniques, and making it possible to compare the effectiveness of competing or complementary approaches by providing a common reference.

It remains to see if anyone is interested!

Credits: much of the work (especially the construction of the repository) was carried out by Victoria Kananchuk as part of a master thesis; Ilgiz Mustafin particularly contributed to the JSON interface.

Here is the full abstract:

 

Automatic Program Repair (APR) is a brilliant idea: when detecting a bug, also provide suggestions for correct- ing the program.

Over the past decades, researchers have come up with promising techniques for making APR a mainstay of software development. Progress towards that goal is, however, hindered by the absence of a common frame of reference to support and compare the multiplicity of ideas, methods, tools, programming languages and programming environments for carrying out automatic program repair.

Bugfix, described in this article, is an effort at providing such a framework: a standardized set of notations, tools and interfaces, as well as a database of bugs and fixes, for use by the APR research community to try out its ideas and compare the results on an objective basis. The most directly visible component of the Bugfix effort is the Bugfix language, a human-readable formalism making it possible to describe elements of the following kinds: a bug (described abstractly, for example the permutation of two arguments in a call); a bug example (an actual occurrence of a bug, in a specific code written in a specific programming language, and usually recorded in some repository); a fix (a particular correction of a bug, obtained for example by reversing the misplaced arguments); an application (an entity that demonstrates how a actual code example matches with a fix); a construct (the abstract description of a programming mechanism, for example a “while” loop, independently of its realization in a programming language; and a language (a description of how a particular programming language includes certain constructs and provides specific concrete syntax for each of them — for example Java includes loop, assignment etc. and has a defined format for each of them).

The language is only one way to access this information. A JSON-based program interface (API) provides it in a form accessible to tools, which may record and access such information into databases.

Bugfix includes such a database (repository), containing a considerable amount of bugs, examples and fixes. We hope that this foundational work will help the APR research community to advance the field by providing a common yardstick and repository.

 

Reminder: my full annotated publication list is here.

New paper: seeding contradiction

by

Just published: Li Huang, Bertrand Meyer and Manuel Oriol, Seeding Contradiction: a fast method for generating full-coverage test suites, in Springer Nature Computer Science, vol. 6, no. 4, 2025. The text is available here on the publisher’s site. Also available is a preprint version.

This just published SNCS article and revised and extended from a conference presentation (at ICTSS 2023 in Bergamo, see here on my efforts back then to use AI to locate the conference site). It describes a new and promising test generation method, part of systematic effort at combining tests and proofs, highlighted in the recent PhD defense of Li Huang (about which I did not have the time to write an article, but will soon).

A new method for achieving full test coverage, very fast, without execution. The idea is to insert an incorrect instruction in every path of the program (technically, every basic block). Then, attempt to prove the program correct, using an SMT-solver-based prover. We “seed a contradiction” into the program.

The proof will fail, as expected, but the solver will generate a counter-example which we can turn into a test using the techniques first presented in earlier papers, including this article. The resulting set of tests is guaranteed to achieve 100% coverage! As a matter of fact the result is better than what is usually understood as “full coverage” since in this journal version we have added the possibility of unrolling loops. (Branch coverage and other usual techniques treat a loop as a conditional, executed either once or not at all. We can execute the body several times, based on a provided parameter.)

Caveat: the examples are still fairly small, although some of them are intricate. Even in this current state, the approach and tool hold the promise of using modern program-proving technology to generate, fully automatically, exhaustive test suites.

Reminder: my full annotated publication list is here.

New preprint: Programming Really Is Simple Mathematics

by

Bertrand Meyer and Reto Weber: Meaning as Programs — Programming Really Is Simple Mathematics, February 2025 preprint available here and also on arXiv.

Theories of programming can be quite complicated; the presentation here is a return to essentials, defining programming and associated concepts (programming languages, programming methodology) entirely from elementary set-theoretical concepts.

Unlike much of the work in formal methods, which forces the reader to go through many axioms and definitions for little benefit, this approach, called PRISM (Programming Really Is Simple Mathematics) is axiom-poor and theorem-rich. In fact it has zero axioms: it simply relies on the well-known properties of set theory to define programming on the basis of one set and one relation. Then it builds up programming mechanisms as simple objects (sets, relations, functions, composition…) and proves theorem after theorem highlighting their properties.

This approach was started in a 2015 article (cited in the new publication) but now, thanks to Reto Weber (a PhD student at CIT), it has the benefit of extensive proofs all checked by Isabelle/HOL; the corresponding files are publicly available.

The article covers the general framework, including the mathematical background (basically high-school-level elementary set theory with a few convenient notations for things like domain of a relation), basic constructs, control structures (sequence, conditional, loops of various kinds), refinement (treated as “subset”), specification vs. implementation, contracts, invariants, and concurrency.

The ambition is to reconstruct all of programming in this spirit.

Here is the more formal abstract from the paper itself:

A re-construction of the fundamentals of programming as a small mathematical theory
(“PRISM”) based on elementary set theory. Highlights:

  • Zero axioms. No properties are assumed, all are proved (from standard set theory).
  • A single concept covers specifications and programs.
  • Its definition only involves one relation and one set.
  • Everything proceeds from three operations: choice, composition and restriction.
  • These techniques suffice to derive the axioms of classic papers on the “laws of pro-
    gramming” as consequences and prove them mechanically.
  • The ordinary subset operator suffices to define both the notion of program correctness
    and the concepts of specialization and refinement.
  • From this basis, the theory deduces dozens of theorems characterizing important
    properties of programs and programming.
  • All these theorems have been mechanically verified (using Isabelle/HOL); the proofs
    are available in a public repository.

Reminder: my full annotated publication list is here.

This is much worse than Munich

by

In Munich in 1938, Chamberlain and Daladier made the wrong decision, but they were driven by honorable motives. Chamberlain was weak but wanted to preserve short-term peace at all costs; Daladier was entirely lucid, but he had taken a look at the state of preparation of the French forces and wanted to buy time to rearm (as he did).

Trump and his clique of incompetent, nasty sycophants are an entirely different matter. Without any pretense of doing the right thing, following the clue of the worst figures in history, they are exercising raw, unchecked power, using the sheer language of might. Two and a half centuries of US democracy and its defense (however imperfect) of human rights have been discarded overnight. So have the lessons of WWII and the bitterly-reached triumph of civilization against dictatorship and barbarism.

It is Europe’s turn to step in. Defending Ukraine is defending us all.

New preprint: Software engineering as a domain to formalize

by

Bertrand Meyer, Software engineering as a domain to formalize, available here.

This article is meant as a blog but was written as a standard text and I haven’t had the time to HTML-ize yet. So I am just providing an abstract below, and linking to the PDF which gives the details.

The purpose is simple: start a community project. The description is prospective only and does not claim to describe a finished product. While simple, the idea is ambitious: define the field of software engineering through a formal theory. Unfortunately, much formal methods work) is axiom- and definition-rich and theorem-poor. Here, the goal is to produce the exact reverse: a good theory that starts with a minimal set of definitions and axioms, and tries to derive as many laws as possible.

Here is the abstract of the article:

Software engineering concepts and processes are worthy of formal study; and yet we seldom formalize them. This  article explores what a theory of software engineering could and should look like.


Software engineering research has developed formal techniques of specification and verification as an application of mathematics to specify and verify systems addressing needs of various application domains. These domains usually do not include the domain of software engineering itself. It is, however, a rich domain with many processes and properties that cry for formalization and potential verification.


This article outlines the structure of a possible theory of software engineering in the form of an object-oriented model, isolating abstractions corresponding to fundamental software concepts of project, milestone, code module, test and other staples of our field, and their mutual relationships. While the presentation is only a sketch of the full theory, it provides a set of guidelines for how a comprehensive and practical Theory of Software Engineering should (through an open-source community effort) be developed.

Please write to the author if you are interested in participating. The link to the PDF of the article again: here.