New preprint: Seamless and Traceable Requirements

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

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 paper: seeding contradiction

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

Bertrand Meyer and Reto Weber: Meaning as ProgramsProgramming 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.

New preprint: Software engineering as a domain to formalize

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.

Freely accessible books

Recently I prepared some of my books for free access on the Web (after gaining agreement from the publishers). Here are the corresponding links. They actually point to pages that present the respective books and have further links to the actual PDF versions.

Although the texts are essentially those of the books as published, I was able in most cases to make some improvements, in particular to the formatting, and to introduce some hyperlinking, for example in table of contents, to facilitate online navigation.

If you cite any of these books please use the links given here. Then you know that you are referring your readers to a legal and up-to-date version. In particular, there are a plethora of pirated copies of Object-Oriented Software Construction on various sites, with bad formatting, no copyright acknowledgment, and none of the improvements.   academia.edu hosts one of them, downloadable. I wrote to them and they did not even answer.

Here are the books and the links.

  • Introduction to the Theory of Programming Languages (Prentice Hall, 1990):  A general introduction to formal reasoning about programs and programming languages. Written without a heavy formal baggage so as to be understandable by programmers who do not have a special mathematical background. Full text freely available from here.
  • Object Success (Prentice Hall, 1995): . A general presentation of object technology, meant in particular for managers and decision-makers, presenting the essential OO ideas and their effect on project management and corporate culture. Full text freely available from here.
  • Object-Oriented Software Construction, 2nd edition (Prentice Hall, 1997): . The best-known of my books, providing an extensive (and long!) presentation of object technology, with particular emphasis on software engineering aspects, including Design by Contract. Introduced many ideas including some of the now classic design patterns (Command, called “undo-redo”, Bridge, called “handle” etc. Full text freely available from here.

In addition, let me include links to recent books published by Springer; they are not freely available, but many people can gain free access through their institutions:

  • Touch of Class: An Introduction to Programming Well Using Objects and Contracts. My introductory programming textbook, used in particular for many years for the intro programming course, altogether to something like 6000 students over 14 years, at ETH Zurich (and nourished by experience). The Springer page with  the text (paywall) is here. There is also my own freely accessible book page with substantial extracts (read for example the chapter on recursion): here.
  • Agile! The Good, the Hype and the Ugly A widely used presentation of agile methods, serving both as tutorial and as critique. The Springer page with  the text (paywall) is here. There is also my own freely accessible book page with substantial extracts: here.
  • Handbook of Requirements and Business Analysis (Springer, 2022). A short but extensive textbook on requirements engineering. The Springer page with  the text (paywall) is here. My own book page, which will soon have substantial extracts and supplementary material, is here.

Also note the volume which I recently edited, The French School of Programming, Springer, 2024, with 13 chapters by top French computer scientists (and a chapter by me). The Springer page  is here.

My full list of books is here. Full publication list in chronological order: here.

 

The French School of Programming

July 14 (still here for 15 minutes) is not a bad opportunity to announced the publication of a new book: The French School of Programming.

The book is a collection of chapters, thirteen of them, by rock stars of programming and software engineering research (plus me), preceded by a Foreword by Jim Woodcock and a Preface by me. The chapters are all by a single author, reflecting the importance that the authors attached to the project. Split into four sections after chapter 1, the chapters are, in order:

1. The French School of Programming: A Personal View, by Gérard Berry (serving as a general presentation of the subsequent chapters).

Part I: Software Engineering

2. “Testing Can Be Formal Too”: 30 Years Later, by  Marie-Claude Gaudel

3. A Short Visit to Distributed Computing Where Simplicity Is Considered a First-Class Property, by Michel Raynal

4. Modeling: From CASE Tools to SLE and Machine Learning, by Jean-Marc Jézéquel

5. At the Confluence of Software Engineering and Human-Computer Interaction: A Personal Account,  by Joëlle Coutaz

Part II:  Programming Language Mechanisms and Type Systems

6. From Procedures, Objects, Actors, Components, Services, to Agents, by  Jean-Pierre Briot

7. Semantics and Syntax, Between Computer Science and Mathematics, by Pierre-Louis Curien

8. Some Remarks About Dependent Type Theory, by Thierry Coquand

Part III: Theory

9. A Personal Historical Perspective on Abstract Interpretation, by Patrick Cousot

10. Tracking Redexes in the Lambda Calculus, by  Jean-Jacques Lévy

11. Confluence of Terminating Rewriting Computations, by  Jean-Pierre Jouannaud

Part IV: Language Design and Programming Methodology

12. Programming with Union, Intersection, and Negation Types, by Giuseppe Castagna

13, Right and Wrong: Ten Choices in Language Design, by Bertrand Meyer

What is the “French School of Programming”? As discussed in the Preface (although Jim Woodcock’s Foreword does not entirely agree) it is not anything defined in a formal sense, as the variety of approaches covered in the book amply demonstrates. What could be more different (for example) than Coq, OCaml (extensively referenced by several chapters) and Eiffel? Beyond the differences, however, there is a certain je ne sais quoi of commonality; to some extent, in fact, je sais quoi: reliance on mathematical principles, a constant quest for simplicity, a taste for elegance. It will be for the readers to judge.

Being single authors of their chapters, the authors felt free to share some of their deepest insights an thoughts. See for example Thierry Coquand’s discussion of the concepts that led to the widely successful Coq proof system, Marie-Claude Gaudel’s new look at her seminal testing work of 30 years ago, and Patrick Cousot’s detailed recounting of the intellectual path that led him and Radhia to invent abstract interpretation.


The French School of Programming
Edited by Bertrand Meyer
Springer, 2024. xxiv + 439 pages

Book page on Springer site
Amazon US page
Amazon France page
Amazon Germany page

The book is expensive (I tried hard to do something about it, and failed). But many readers should be able to download it, or individual chapters, for free through their institutions.

It was a privilege for me to take this project to completion and work with such extraordinary authors who produced such a collection of gems.

New article: scenarios versus OO requirements

Maria Naumcheva, Sophie Ebersold, Alexandr Naumchev, Jean-Michel Bruel, Florian Galinier and Bertrand Meyer: Object-Oriented Requirements: a Unified Framework for Specifications, Scenarios and Tests, in JOT (Journal of Object Technology), vol. 22, no. 1, pages 1:1-19, 2023. Available here with link to PDF  (the journal is open-access).

From the abstract:

A paradox of requirements specifications as dominantly practiced in the industry is that they often claim to be object-oriented (OO) but largely rely on procedural (non-OO) techniques. Use cases and user stories describe functional flows, not object types.

To gain the benefits provided by object technology (such as extendibility, reusability, and reliability), requirements should instead take advantage of the same data abstraction concepts – classes, inheritance, information hiding – as OO design and OO programs.

Many people find use cases and user stories appealing because of the simplicity and practicality of the concepts. Can we reconcile requirements with object-oriented principles and get the best of both worlds?

This article proposes a unified framework. It shows that the concept of class is general enough to describe not only “object” in a narrow sense but also scenarios such as use cases and user stories and other important artifacts such as test cases and oracles. Having a single framework opens the way to requirements that enjoy the benefits of both approaches: like use cases and user stories, they reflect the practical views of stakeholders; like object-oriented requirements, they lend themselves to evolution and reuse.

The article builds in part on material from chapter 7 of my requirements book (Handbook of Requirements and Business Analysis, Springer).

Statement Considered Harmful

I harbor no illusion about the effectiveness of airing this particular pet peeve; complaining about it has about the same chance of success as protesting against split infinitives or music in restaurants. Still, it is worth mentioning that the widespread use of the word “statement” to denote a programming language element, such as an assignment, that directs a computer to perform some change, is misleading. “Instruction” is the better term.

A “statement” is “something stated, such as a single declaration or remark, or a report of fact or opinions” (Merriam-Webster).

Why does it matter? The use of “statement” to mean “instruction” obscures a fundamental distinction of software engineering: the duality between specification and implementation. Programming produces a solution to a problem; success requires expressing both the problem, in the form of a specification, and the devised solution, in the form of an implementation. It is important at every stage to know exactly where we stand: on the problem side (the “what”) or the solution side (the “how”). In his famous Goto Statement Considered Harmful of 1968, Dijkstra beautifully characterized this distinction as the central issue of programming:

Our intellectual powers are rather geared to master static relations and our powers to visualize processes evolving in time are relatively poorly developed. For that reason we should do (as wise programmers aware of our limitations) our utmost to shorten the conceptual gap between the static program and the dynamic process, to make the correspondence between the program (spread out in text space) and the process (spread out in time) as trivial as possible.

Software verification, whether conducted through dynamic means (testing) or static techniques (static analysis, proofs of correctness), relies on having separately expressed both a specification of the intent and a proposed implementation intended to realize that intent. They have to remain distinct; otherwise we cannot even define what it means that the program should be correct (correct with respect to what?), and even less what it means to validate the program (validate it against what?).

In many approaches to verification, the properties against which we validate programs are called assertions. An assertion expresses a property that should hold at some point of program execution. For example, after the assignment instruction a := b + 1, the assertion ab will hold. This notion of assertion is used both in testing frameworks, such as JUnit for Java or PyUnit for Python, and in program proving frameworks; see, for example, the interactive Web-based version of the AutoProof program-proving framework for Eiffel at autoproof.sit.org, and of course the entire literature on axiomatic (Floyd-Hoare-Dijkstra-style) verification.

The difference between the instruction and the assertion is critical: a := b + 1 tells the computer to do something (change the value of a), as emphasized here by the “:=” notation for assignment; ab does not direct the computer or the computation to do anything, but simply states a property that should hold at a certain stage of the computation if everything went fine so far.

In the second case, the word “states” is indeed appropriate: an assertion states a certain property. The expression of that property, ab, is a “statement” in the ordinary English sense of the term. The command to the computer, a := b + 1, is an instruction whose effect is to ensure the satisfaction of the statement ab. So if we use the word “statement” at all, we should use it to mean an assertion, not an instruction.

If we start calling instructions “statements” (a usage that Merriam-Webster grudgingly accepts in its last entry for the term, although it takes care to define it as “an instruction in a computer program,” emphasis added), we lose this key distinction.

There is no reason for this usage, however, since the word “instruction” is available, and entirely appropriate.

So, please stop saying “an assignment statement” or “a print statement“; say “an assignment instruction” and so on.

Maybe you won’t, but at least you have been warned.

Recycled This article was first published in the “Communications of the ACM” blog.

“Object Success” now available

A full, free online version of Object Success
(1995)

success_cover

 

I am continuing the process of releasing some of my earlier books. Already available: Introduction to the Theory of Programming Languages (see here) and Object-Oriented Software Construction, 2nd edition (see here). The latest addition is Object Success, a book that introduced object technology to managers and more generally emphasized the management and organizational consequences of OO ideas.

The text (3.3 MB) is available here for download.

Copyright notice: The text is not in the public domain. It is copyrighted material (© Bertrand Meyer, 1995, 2023), made available free of charge on the Web for the convenience of readers, with the permission of the original publisher (Prentice Hall, now Pearson Education, Inc.). You are not permitted to copy it or redistribute it. Please refer others to the present version at bertrandmeyer.com/success.

(Please do not bookmark or share the above download link as it may change, but use the present page: https:/bertrandmeyer.com/success.) The text is republished identically, with minor reformatting and addition of some color. (There is only one actual change, a mention of the evolution of hardware resources, on page 136, plus a reference to a later book added to a bibliography section on page 103.) This electronic version is fully hyperlinked: clicking entries in the table of contents and index, and any element in dark red such as the page number above, will take you to the corresponding place in the text.

The book is a presentation of object technology for managers and a discussion of management issues of modern projects. While it is almost three decades old and inevitably contains some observations that will sound naïve  by today’s standards, I feel  it retains some of its value. Note in particular:

  • The introduction of a number of principles that went radically against conventional software engineering wisdom and were later included in agile methods. See Agile! The Good, the Hype and the Ugly, Springer, 2014, book page at agile.ethz.ch.
  • As an important example, the emphasis on the primacy of code. Numerous occurrences of the argument throughout the text. (Also, warnings about over-emphasizing analysis, design and other products, although unlike “lean development” the text definitely does not consider them to be “waste”. See the “bubbles and arrows of outrageous fortune”, page 80.)
  • In the same vein, the emphasis on incremental development.
  • Yet another agile-before-agile principle: Less-Is-More principle (in “CRISIS REMEDY”, page 133).
  • An analysis of the role of managers (chapters 7 to 9) which remains largely applicable, and I believe more realistic than the agile literature’s reductionist view of managers.
  • A systematic analysis of what “prototyping” means for software (chapter 4), distinguishing between desirable and less good forms.
  • Advice on how to salvage projects undergoing difficulties or crises (chapters 7 and 9).
  • A concise exposition of OO concepts (chapter 1 and appendix).
  • A systematic discussion of software lifecycle models (chapter 3), including the “cluster model”. See new developments on this topic in my recent “Handbook of Requirements and Business Analysis”, Springer, 2022, book page at bertrandmeyer.com/requirements.
  • More generally, important principles from which managers (and developers) can benefit today just as much as at the time of publication.

The download link again (3.3 MB): here it is.