Bertrand Meyer's technology+ blog
Software engineering, programming methodology, languages, verification, general technology, publication culture, and more
A core aspect of our verification work is the use of “strong” contracts, which express sophisticated specification properties without requiring a separate specification language: even for advanced properties, there is no need for a separate specification language, with special notations such as those of first-order logic; instead, one can continue to rely, in the … Read more
The European Software Engineering Conference takes place every two years in connection with the ACM Foundations of Software Engineering symposium (which in even years is in the US). The next ESEC/FSE will be held for the first time in Russia, where it will be the first major international software engineering conference ever. It comes at … Read more
The study of agile methods is good for your skeptical bones. “Build the simplest thing that works, then refactor if needed.” Maybe. Maybe. But what about getting it right the first time around? Erich Kästner wrote an apposite ditty on this topic [1]: They tell you it’s OK if first you fail; OK perhaps … Read more
Actually it is not a musical but an extensive survey. I have long been fascinated by the notion of loop invariant, which describes the essence of a loop. Considering a loop without its invariant is like conducting an orchestra without a score. In this submitted survey paper written with Sergey Velder and Carlo Furia … Read more
Alexander Kogtenkov pointed out to me that precursor work to my papers on the Alias Calculus [1] [2] had been published by John Whaley and Martin Rinard [3]. There are some significant differences; in particular my rules are simpler, and their work is not explicitly presented as a calculus. But many of the basic ideas … Read more
Both Gary Leavens and Jim Horning commented (partly here, partly on Facebook) about my Domain Theory article [1] to mention that Larch had mechanisms for domain modeling and specification reuse. As Horning writes: The Larch Shared Language was really all about creating reusable domain theories, including theorems about the domains. See, for example [2] and … Read more
Program verification is making considerable progress but is hampered by a lack of abstraction in specifications. A crucial step is, almost always, absent from the process; this omission is the principal obstacle to making verification a standard component of everyday software development. 1. Steps in software verification In the first few minutes of any … Read more
In the Eiffel user discussion group [1], Ian Joyner recently asked: A lot of people are now using Result as a variable name for the return value in many languages. I believe this first came from Eiffel, but can’t find proof. Or was it adopted from an earlier language? Proof I cannot offer, but … Read more