Bertrand Meyer's technology+ blog

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.

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.

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.

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.

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.

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.

Academic life includes self-governance and require people to sit in committees, take on various duties, serve as director of studies, graduate program director, chair of PhD chair of external relations, department vice chair or chair, dean…

Not everyone wants to play. It is not rare to encounter faculty members who tell you bluntly that as researchers they are too good to waste their time on boring organizational tasks that any mere mortal, or at least any mere academic, can fulfill.

This common situation came to my mind, as I was reading an outstanding new (2022) biography of Louis Pasteur by Michel Morange [1], when I came across the chapter on Pasteur’s return to the École Normale Supérieure in 1857. Excerpting and translating:

He was given two titles: administrator, and director of studies. The function of administrator consisted of supervising the life of students living on campus and to oversee the canteen as well as the dormitory rooms. It was part of his duties to check the correct operation of doors and windows, and to commission any necessary paintwork. He was more generally responsible for maintaining order inside the school and to monitor the student’s attire as well as their behavior.

Impressive! That was a time of highest scientific productivity for Pasteur (in spite of major personal tragedies), with one breathtaking discovery after the other, including anaerobiosis (life without air), pioneering studies of fermentation, preparing and performing numerous experiments, carefully refuting spontaneous generation… He was also a dedicated teacher, giving numerous lectures and exposing students to his research.

Remember Pasteur the next time a colleague tells you that his research is too indispensable to the progress of humankind to allow him to take on organizational tasks. If Pasteur could find time for his evening round of checking the dorm doors, for telling the students to dress better, and for overseeing new paint jobs, maybe you can be director of studies for the department for a couple of years.

Such willingness to take on management duties is part of the price academics pay for the many benefits of academic self-governance. The alternative is to be managed by bean-counting manager types who do not understand academia. Or, perhaps a more immediate risk, to let the bad scientists (who will find the time) take on these tasks. A look at thriving top universities usually reveals that, at the helm, there is a top scientist. Someone who succeeded in education and research and is devoting a few years to moving the institution forward. Lesser universities are managed by lesser academics. If the good people shirk their responsibilities, the bad ones will take over. Or is your research more important than Louis Pasteur’s?

References

[1] Michel Morange, Pasteur, Payot, 2022. In French. (Other books by Morange have been translated into English, particularly his History of Biology by Princeton University Press, but I do not know about this one.)