Bertrand Meyer's technology+ blog

Li Huang (PhD student at SIT) will be presenting at an ISSRE workshop the paper Improving Counterexample Quality from Failed Program Verification, written with Manuel Oriol and me. One can find the text on arXiv here. (I will update this reference with the official publication link when I have it.)

The result being presented is part of a more general effort at combining proofs and tests (with other papers in the pipeline). The idea of treating proofs and tests as complementary rather than competing methods of software verification is an old pursuit of mine (which among other consequences resulted in the creation with Yuri Gurevich of the Tests and Proofs conference, which I see is continuing to run). A particular observation is that failure means a different thing for proofs and tests.

A failed test provides interesting information (in fact it is a successful proof — of incorrectness). A successful proof is, of course, also interesting (in principle it should be end of the story), whereas a successful test tells us very little. But in the practice of program proving the common occurrence is failure to prove a program element correct. You are typically left with no clue as to the source of the failure. In the AutoProof verification system for Eiffel, we are able to rely on the underlying technology (Boogie and Z3) to extract a counterexample which gives concrete evidence: as with a failed test, a programmer can in general quickly understand what is wrong.

In other words, the useless negative result of the bottom-left entry of the above picture can produce a useful result:

The general approach is the subject of another article but this one focuses on producing tests that are actually significant for the programmer. If you get very large values, you will not immediately be able to relate to them. Hence the need for a process of minimization, described in the article. The results on our examples are encouraging, making it possible to evidence the bug on very small integer values.

Reference

Li Huang, Bertrand Meyer and Manuel Oriol: Improving Counterexample Quality from Failed Program Verification, 6th International Workshop on Software Faults, October 2022. Preprint available on arXiv here. The program workshop is available here; the presentation is on Monday, 31 October, 15:55 CET (7:55 AM Los Angeles, 10:55 New York).

I am happy to announce the publication of the Handbook of Requirements and Business Analysis (Springer, 2022).

It is the result of many years of thinking about requirements and how to do them right, taking advantage of modern principles of software engineering. While programming, languages, design techniques, process models and other software engineering disciplines have progressed considerably, requirements engineering remains the sick cousin. With this book I am trying to help close the gap.

The Handbook introduces a comprehensive view of requirements including four elements or PEGS: Project, Environment, Goals and System. One of its principal contributions is the definition of a standard plan for requirements documents, consisting of the four corresponding books and replacing the obsolete IEEE 1998 structure.

The text covers both classical requirements techniques and novel topics such as object-oriented requirements and the use of formal methods.

The successive chapters address: fundamental concepts and definitions; requirements principles; the Standard Plan for requirements; how to write good requirements; how to gather requirements; scenario techniques (use cases, user stories); object-oriented requirements; how to take advantage of formal methods; abstract data types; and the place of requirements in the software lifecycle.

The Handbook is suitable both as a practical guide for industry and as a textbook, with over 50 exercises and supplementary material available from the book’s site.

You can find here a book page with the preface and sample chapters.

To purchase the book, see the book page at Springer and the book page at Amazon US.

It is easy to engage in generalities; it is risky to make firm predictions. In the first case there is no reckoning; in the second one the actual events can prove you wrong for everyone to see.

I am taking the risk. Here is my prediction: Putin’s energy blackmail (Western Europe will freeze this winter!) will fail. We’ll have some trouble but by and large we’ll be OK.

The basic reason is simple: great idea (from the blackmailer’s viewpoint), terrible execution. (Do we see a pattern there?) If you are going to freeze Europe by cutting off gas, you keep the suspense until the last minute and shut off the valves in October, leaving your targets no time to react.

Instead they did it all wrong! They started making noises in the Spring and cutting off supplies in August. The result: people listened. Governments and technocrats got to work, with some time to get organized. A company such as EDF in France is sometimes criticized as too big and monolithic, but they know their business, which is to provide energy, and are pretty good at it. I would bet that they and their counterparts in the electricity and gas industries all over the continent are working day and night to find alternative sources.

In addition, no day passes without some announcement of new energy-saving measures. Some may seem like for show only but the accumulated result will be significant. Recently everyone (for example the usually better inspired Guardian) was mocking Macron’s prime minister Borne and her ministers for showing up to work in padded jeans and sweaters to save on heating, but that kind of message can be influential. (Almost a half-century ago Jimmy Carter was telling Americans that instead of turning the temperature to 19 degrees C in summer and 21 in winter they should do the reverse. He too was derided. But he was right and that kind of advice will finally come to pass. One of the few positive outcomes of the current tragedy.)

So yes, you succeeded in making yourself a big nuisance. And no, it won’t destroy us. It will make us stronger — also warmer.