“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.

The legacy of Barry Boehm

August of last year brought the sad news of Barry Boehm’s passing away on August 20. If software engineering deserves at all to be called engineering today, it is in no small part thanks to him.

“Engineer” is what Boehm was, even though his doctorate and other degrees were all in mathematics. He looked the part (you might almost expect him to carry a slide rule in his shirt pocket, until you realized that as a software engineer he did not need one) and more importantly he exuded the seriousness, dedication, precision, respect for numbers, no-nonsense attitude and practical mindset of outstanding engineers. He was employed as an engineer or engineering manager in the first part of his career, most notably at TRW, a large aerospace company (later purchased by Northrop Grumman), turning to academia (USC) afterwards, but even as a professor he retained that fundamental engineering ethos.

 

boehm_tichy_basili

 

LASER Summer School, Elba Island (Italy), September 2010
From left: Walter Tichy, Barry Boehm, Vic Basili (photograph by Bertrand Meyer)

Boehm’s passion was to turn the study of software away from intuition and over to empirical enquiry, rooted in systematic objective studies of actual projects. He was not the only one advocating empirical methods (others from the late seventies on included Basili, Zelkowitz, Tichy, Gilb, Rombach, McConnell…) but he had an enormous asset: access to mines of significant data—not student experiments, as most researchers were using!—from numerous projects at TRW. (Basili and Zelkowitz had similar sources at NASA.) He patiently collected huge amounts of project information, analyzed them systematically, and started publishing paper after paper about what works for software development; not what we wish would work, but what actually does on the basis of project results.

Then in 1981 came his magnum opus, Software Engineering Economics (Prentice Hall), still useful reading today (many people inquired over the years about projects for a second edition, but I guess he felt it was not warranted). Full of facts and figures, the book also popularized the Cocomo model for cost prediction, still in use nowadays in a revised version developed at USC (Cocomo II, 1995, directly usable through a simple Web interface at softwarecost.org/tools/COCOMO/

Cocomo provides a way to estimate both the cost and the duration of a project from the estimated number of lines of code (alternatively, in Cocomo II, from the estimated number of function points), and some auxiliary parameters to account for each project’s specifics. Boehm derived the formula by fitting from thousands of projects.

When people first encounter the idea of Cocomo (even in a less-rudimentary form than the simplified one I just gave), their first reaction is often negative: how can one use a single formula to derive an estimate for any project? Isn’t the very concept ludicrous anyway since by definition we do not know the number of lines of code (or even of function points) before we have developed the project? With lines of code, how do we distinguish between different languages? There are answers to all of these questions (the formula is ponderated by a whole set of criteria capturing project specifics, lines of code calibrated by programming language level do correlate better than most other measures with actual development effort, a good project manager will know in advance the order of magnitude of the code size etc.). Cocomo II is not a panacea and only gives a rough order of magnitude, but remains one of the best available estimation tools.

Software Engineering Economics and the discussion of Cocomo also introduced important laws of software engineering, not folk wisdom as was too often (and sometimes remains) prevalent, but firm results. I covered one in an article in this blog some time ago, calling it the “Shortest Possible Schedule Theorem”: if a serious estimation method, for example Cocomo, has determined an optimal cost and time for a project, you can reduce the time by devoting more resources to the project, but only down to a certain limit, which is about 75% of the original. In other words, you can throw money at a project to make things happen faster, but the highest time reduction you will ever be able to gain is by a quarter. Such a result, confirmed by many studies (by Boehm and many others after him), is typical of the kind of strong empirical work that Boehm favored.

The CMM and CMMI models  of technical management are examples of important developments that clearly reflect Boehm’s influence. I am not aware that he played any direct role (the leader was Watts Humphrey, about whom I wrote a few years ago), but the models’ constant emphasis on measurement, feedback and assessment are in line with the principles  so persuasively argued in his articles and books.

Another of his famous contributions is the Spiral model of the software lifecycle. His early work and Software Engineering Economics had made Boehm a celebrity in the field, one of its titans in fact, but also gave him the reputation, deserved or not, of representing what may be called big software engineering, typified by the TRW projects from which he drew his initial results: large projects with large budgets, armies of programmers of variable levels of competence, strong quality requirements (often because of the mission- and life-critical nature of the projects) leading to heavy quality assurance processes, active regulatory bodies, and a general waterfall-like structure (analyze, then specify, then design, then implement, then verify). Starting in the eighties other kinds of software engineering blossomed, pioneered by the personal computer revolution and Unix, and often typified by projects, large or small but with high added value, carried out iteratively by highly innovative teams and sometimes by just one brilliant programmer. The spiral model is a clear move towards flexible modes of software development. I must say I was never a great fan (for reasons not appropriate for discussion here) of taking the Spiral literally, but the model was highly influential and made Boehm a star again for a whole new generation of programmers in the nineties. It also had a major effect on agile methods, whose notion of  “sprint ” can be traced directly the spiral. It is a rare distinction to have influenced both the CMM and agile camps of software engineering with all their differences.

This effort not to remain wrongly identified with the old-style massive-project software culture, together with his natural openness to new ideas and his intellectual curiosity, led Boehm to take an early interest in agile methods; he was obviously intrigued by the iconoclasm of the first agile publications and eager to understand how they could be combined with timeless laws of software engineering. The result of this enquiry was his 2004 book (with Richard Turner) Balancing Agility and Discipline: A Guide for the Perplexed, which must have been the first non-hagiographic presentation (still measured, may be a bit too respectful out of a fear of being considered old-guard) of agile approaches.

Barry Boehm was an icon of the software engineering movement, with the unique position of having been in essence present at creation (from the predecessor conference of ICSE in 1975) and accompanying, as an active participant, the stupendous growth and change of the field over half a century.

 

boehm_shanghai

Barry Boehm at a dinner at ICSE 2006, Shanghai (photograph by Bertrand Meyer)

I was privileged to meet Barry very early, as we were preparing a summer school in 1978 on Programming Methodology where the other star was Tony Hoare. It was not clear how the mix of such different personalities, the statistics-oriented UCLA-graduate American engineer and the logic-driven classically-trained (at Oxford) British professor would turn out.

Boehm could be impatient with cryptic academic pursuits; one exercise in Software Engineering Economics (I know only a few other cases of sarcasm finding its refuge in exercises from textbooks) presents a problem in software project management and asks for an answer in multiple-choice form. All the proposed choices are sensible management decisions, except for one which goes something like this: “Remember that Bob Floyd [Turing-Awarded pioneer of algorithms and formal verification] published in Communications of the ACM vol. X no. Y pages 658-670 that scheduling of the kind required can be performed in O (n3 log log n) instead of O (n3 log n) as previously known; take advantage of this result to spend 6 months writing an undecipherable algorithm, then discover that customers do not care a bit about the speed.” (Approximate paraphrase from memory [1].)

He could indeed be quite scathing of what he viewed as purely academic pursuits removed from the reality of practical projects. Anyone who attended ICSE 1979 a few months later in Munich will remember the clash between him and Dijkstra; the organizers had probably engineered it (if I can use that term), having assigned them the topics  “Software Engineering As It Is” and “Software Engineering as It Should Be”, but it certainly was spectacular. There had been other such displays of the divide before. Would we experience something of the kind at the summer school?

No clash happened; rather, the reverse, a meeting of minds. The two sets of lectures (such summer schools lasted three weeks at that time!) complemented each other marvelously, participants were delighted, and the two lecturers also got along very well. They were, I think, the only native English speakers in that group, they turned out to have many things in common (such as spouses who were also brilliant software engineers on their own), and I believe they remained in contact for many years. (I wish I had a photo from that school—if anyone reading this has one, please contact me!)

Barry was indeed a friendly, approachable, open person, aware of his contributions but deeply modest.

Few people leave a profound personal mark on a field. A significant part of software engineering as it is today is a direct consequence of Barry’s foresight.

 

Note

[1] The full text of the exercise will appear shortly as a separate article on this blog.

 

Recycled A version of this article appeared previously in the Communications of the ACM blog.

Logical beats sequential

Often,  “we do this and then we do that” is just a lazy way of stating “to do that, we must have achieved this.” The second form is more general than the first, since there may be many things you can “do” to achieve a certain condition.

The extra generality is welcome for software requirements, which should describe essential properties without over-specifying, in particular without prescribing a specific ordering of operations  when it is only one possible sequence among several, thereby restricting the flexibility of designers and implementers.

This matter of logical versus sequential constraints is at the heart of the distinction between scenario-based techniques — use cases, user stories… — and object-oriented requirements. This article analyzes the distinction. It is largely extracted from my recent textbook, the Handbook of Requirements and Business Analysis [1], which contains a more extensive discussion.

1. Scenarios versus OO

Scenario techniques, most significantly use cases and user stories, have become dominant in requirements. They obviously fill a need and are intuitive to many people. As a general requirement technique, however, they lack abstraction. Assessed against object-oriented requirements techniques, they suffer from the same limitations as procedural (pre-OO)  techniques against their OO competitors in the area of design and programming. The same arguments that make object technology subsume non-OO approaches in those areas transpose to requirements.

Scenario techniques describe system properties in terms of a particular sequence of interactions with the system. A staple example of a use case is ordering a product through an e-commerce site, going through a number of steps. In contrast, an OO specification presents a certain number of abstractions and operations on them, chracterized by their logical properties. This description may sound vague, so we move right away to examples.

2. Oh no, not stacks again

Yes, stacks. This example is rather computer-sciency so it is not meant to convince anyone but just to explain the ideas. (An example more similar to what we deal with in the requirements of industry projects is coming next.)

A stack is a LIFO (Last-In, First-Out) structure. You insert and remove elements at the same end.

 

Think of a stack of plates, where you can deposit one plate at a time, at the top, and retrieve one plate at a time, also at the top. We may call the two operations put and remove. Both are commands (often known under the alternative names push and pop). We will also use an integer query count giving the number of elements.

Assume we wanted to specify the behavior of a stack through use cases. Possible use cases (all starting with an empty stack) are:

/1/

put
put ; put
put ; put ; put       
— etc.: any number of successive put (our stacks are not bounded)

put ; remove
put ; put ; remove
put ; put ; remove ; remove
put ; put ; remove ; remove ; put ; remove

We should also find a way to specify that the system does not support such use cases as

/2/

remove ; put

or even just

/3/

remove

We could keep writing such use cases forever — some expressing normal sequences of operations, others describing erroneous cases — without capturing the fundamental rule that at any stage, the number of put so far has to be no less than the number of remove.

A simple way to capture this basic requirement is through logical constraints, also known as contracts, relying on assertions: preconditions which state the conditions under which an operation is permitted, and postconditions which describe properties of its outcome. In the example we can state that:

  • put has no precondition, and the postcondition

          count = old count + 1

using the old notation to refer to the value of an expression before the operation (here, the postcondition states that put increases count by one).

  • remove has the precondition

count > 0

and the postcondition

count = old count – 1

since it is not possible to remove an element from an empty stack. More generally the LIFO discipline implies that we cannot remove more than we have put.(Such illegal usage sequences are sometimes called “misuse cases.”)

(There are other properties, but the ones just given suffice for this discussion.)

The specification states what can be done with stacks (and what cannot) at a sufficiently high level of abstraction to capture all possible use cases. It enables us to keep track of the value of count in the successive steps of a use case; it tells us for example that all the use cases under /1/ above observe the constraints: with count starting at 0, taking into account the postconditions of put and remove, the precondition of every operation will be satisfied prior to all of its calls. For /2/ and /3/ that is not the case, so we know that these use cases are incorrect.

Although this example covers a data structure, not  requirements in the general sense, it illustrates how logical constraints are more general than scenarios:

  • Use cases, user stories and other  forms of scenario only describe specific instances of behavior.
  • An OO model with contracts yields a more abstract specification, to which individual scenarios can be shown to conform, or not.

3. Avoiding premature ordering decisions

As the stack example illustrates, object-oriented specifications stay away from premature time-order decisions by focusing on object types (classes) and their operations (queries and commands), without making an early commitment to the order of executing these operations.

In the book, I use in several places a use-case example from one of the best books about use cases (along with Ivar Jacobson’s original one of course): Alistair Cockburn’s Writing Effective Use Cases (Pearson Education, 2001). A simplified form of the example is:

1. A reporting party who is aware of the event registers a loss to the insurance company.

2. A clerk receives and assigns claim to a claims agent.

3. The assigned claims adjuster:

3.1 Conducts an investigation.
3.2 Evaluates damages.
3.3 Sets reserves.
3.4 Negotiates the claim.
3.5 Resolves the claim and closes it.

(A reserve in the insurance business is an amount that an insurer, when receiving a claim, sets aside as to cover the financial liability that may result from the claim.)

As a specification, this scenario is trying to express useful things; for example, you must set reserves before starting to negotiate the claim. But it expresses them in the form of a strict sequence of operations, a temporal constraint which does not cover the wide range of legitimate scenarios. As in the stack example, describing a few such scenarios is helpful as part of requirements elicitation, but to specify the resulting requirements it is more effective to state the logical constraints.

Here is a sketch (in Eiffel) of how a class INSURANCE_CLAIM could specify them in the form of contracts. Note the use of require to introduce a precondition and ensure for postconditions.

class INSURANCE_CLAIM feature

        — Boolean queries (all with default value False):
    is_investigated, is_evaluated, is_reserved,is_agreed,is_imposed, is_resolved:

BOOLEAN

    investigate
                — Conduct investigation on validity of claim. Set is_investigated.
        deferred
        ensure
            is_investigated
        end

    evaluate
                — Assess monetary amount of damages.
        require
            is_investigated
        deferred
        ensure
            is_evaluated
            — Note: is_investigated still holds (see the invariant at the end of the class text).
        end

    set_reserve
                — Assess monetary amount of damages. Set is_reserved.
        require
            is_investigated
            — Note: we do not require is_evaluated.
        deferred
        ensure
            is_reserved
        end
 

    negotiate
                — Assess monetary amount of damages. Set is_agreed only if negotiation
                — leads to an agreement with the claim originator.
        require
                   is_reserved
is_evaluated   
                   

        deferred
        ensure
            is_reserved
            — See the invariant for is_evaluated and is_investigated.
        end

    impose (amount: INTEGER)
                — Determine amount of claim if negotiation fails. Set is_imposed.
        require
            not is_agreed
            is_reserved
        deferred
        ensure
            is_imposed
        end

    resolve
                — Finalize handling of claim. Set is_resolved.
        require
            is_agreed or is_imposed
        deferred
        ensure
            is_resolved
        end

invariant                    — “⇒” is logical implication.

is_evaluated is_investigated
is_reserved 
is_evaluated
is_resolved
is_agreed or is_imposed
is_agreed
is_evaluated
is_imposed
is_evaluated
is_imposed
not is_agreed

                          — Hence, by laws of logic, is_agreed not is_imposed

end

Notice the interplay between the preconditions, postconditions and class invariant, and the various boolean-valued queries they involve (is_investigated, is_evaluated, is_reserved…). You can specify a strict order of operations o1, o2 …, as in a use case, by having a sequence of assertions pi such that operation oi has the contract clauses require pi and ensure pi+1; but assertions also enable you to specify a much broader range of allowable orderings as all acceptable.
The class specification as given is only a first cut and leaves many aspects untouched. It will be important in practice, for example, to include a query payment describing the amount to be paid for the claim; then impose has the postcondition payment = amount, and negotiate sets a certain amount for payment.
Even in this simplified form, the specification includes a few concepts that the original use case left unspecified, in particular the notion of imposing a payment (through the command impose) if negotiation fails. Using a logical style typically uncovers such important questions and provides a framework for answering them, helping to achieve one of the principal goals of requirements engineering.

4. Logical constraints are more general than sequential orderings

The specific sequence of actions described in the original use case (“main success scenario”) is compatible with the logical constraints: you can check that in the sequence

investigate
evaluate
set_reserve
negotiate
resolve

the postcondition of each step implies the precondition of the next one (the first has no precondition). In other words, the temporal specification satisfies the logical one. But you can also see that prescribing this order is a case of overspecification: other orderings also satisfy the logical specification. It may be possible for example — subject to confirmation by Subject-Matter Experts — to change the order of evaluate and set_reserve, or to perform these two operations in parallel.

The specification does cover the fundamental sequencing constraints; for example, the pre- and postcondition combinations imply that investigation must come before evaluation and resolution must be preceded by either negotiation or imposition. But they avoid the non-essential constraints which, in the use case, were only an artifact of the sequential style of specification, not a true feature of the problem.

The logical style is also more conducive to conducting a fruitful dialogue with domain experts and stakeholders:

  • With a focus on use cases, the typical question from a requirements engineer (business analyst) is “do you do A before doing B?” Often the answer will be contorted, as in “usually yes, but only if C, oh and sometimes we might start with B if D holds, or we might work on A and B in parallel…“, leading to vagueness and to more complicated requirements specifications.
  • With logic-based specifications, the two fundamental question types are: “what conditions do you need before doing B?” and “does doing A ensure condition C?”. They force stakeholders to assess their own practices and specify precisely the relations between operations of interest.

5. What use for scenarios?

Use-cases and more generally scenarios, while more restrictive than logical specifications, remain important as complements to specifications. They serve as both input and output to more abstract requirements specifications (such as OO specifications with contracts):

  • As input to requirements: initially at least, stakeholders and Subject-Matter Experts often find it intuitive to describe typical system interactions, and their own activities, in the form of scenarios. Collecting such scenarios is an invaluable requirements elicitation technique. The requirements engineer must remember that any such scenario is just one example walk through the system, and must abstract from these examples to derive general logical rules.
  • As output from requirements: from an OO specification with its contracts, the requirements engineers can produce valid use cases. “Valid” means that the operation at every step satisfies the applicable precondition, as a consequence of the previous steps’ postconditions and of the class invariant. The requirements engineers can then submit these use cases to the SMEs and through them to stakeholders to confirm that they make sense, update the logical conditions if they do not (to rule out bad use cases), and check the results they are expected to produce.

6. Where do scenarios fit?

While many teams will prefer to write scenarios (for the purposes just described) in natural language, it is possible to go one step further and, in an object-oriented approach to requirements, gather scenarios in classes. But that point exceeds the scope of the present sketch. We will limit ourselves here to the core observation: logical constraints subsume sequential specifications; you can deduce the ltter from the former, but not the other way around; and focusing on abstract logical specifications leads to a better understanding of the requirements.

Reference

Bertrand Meyer: Handbook of Requirements and Business Analysis, Springer, 2022. See the book page with sample chapters and further material here.

Recycled(This article was first published on the Communications of the ACM blog.)

New paper: optimization of test cases generated from failed proofs

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:

Pasted

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).

 

New book: the Requirements Handbook

cover

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.

pegsThe 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.

Introduction to the Theory of Programming Languages: full book now freely available

itpl_coverShort version: the full text of my Introduction to the Theory of Programming Languages book (second printing, 1991) is now available. This page has more details including the table of chapters, and a link to the PDF (3.3MB, 448 + xvi pages).

The book is a survey of methods for language description, particularly semantics (operational, translational, denotational, axiomatic, complementary) and also serves as an introduction to formal methods. Obviously it would be written differently today but it may still have its use.

A few days ago I released the Axiomatic Semantics chapter of the book, and the chapter introducing mathematical notations. It looked at the time that I could not easily  release the rest in a clean form, because it is impossible or very hard to use the original text-processing tools (troff and such). I could do it for these two chapters because I had converted them years ago for my software verification classes at ETH.

By perusing old files, however,  I realized that around the same time (early 2000s) I actually been able to produce PDF versions of the other chapters as well, even integrating corrections to errata  reported after publication. (How I managed to do it then I have no idea, but the result looks identical, save the corrections, to the printed version.)

The figures were missing from that reconstructed version (I think they had been produced with Brian Kernighan’s PIC graphical description language , which is even more forgotten today than troff), but I scanned them from a printed copy and reinserted them into the PDFs.

Some elements were missing from my earlier resurrection: front matter, preface, bibliography, index. I was able to reconstruct them from the original troff source using plain MS Word. The downside is that they are not hyperlinked; the index has the page numbers (which may be off by 1 or 2 in some cases because of reformatting) but not hyperlinks to the corresponding occurrences as we would expect for a new book. Also, I was not able to reconstruct the table of contents; there is only a chapter-level table of contents which, however, is hyperlinked (in other words, chapter titles link to the actual chapters). In the meantime I obtained the permission of the original publisher (Prentice Hall, now Pearson Education Inc.).

Here again is the page with the book’s description and the link to the PDF:

bertrandmeyer.com/ITPL

 

 

Introduction to axiomatic semantics

itplI have released for general usage the chapter on axiomatic semantics of my book Introduction to the Theory of Programming Languages. It’s old but I think it is still a good introduction to the topic. It explains:

  • The notion of theory (with a nice — I think — example borrowed from an article by Luca Cardelli: axiomatizing types in lambda calculus).
  • How to axiomatize a programming language.
  • The notion of assertion.
  • Hoare-style pre-post semantics, dealing with arrays, loop invariants etc.
  • Dijkstra’s calculus of weakest preconditions.
  • Non-determinism.
  • Dealing with routines and recursion.
  • Assertion-guided program construction (in other words, correctness by construction), design heuristics (from material in an early paper at IFIP).
  • 26 exercises.

The text can be found at

https://se.inf.ethz.ch/~meyer/publications/theory/09-axiom.pdf

It remains copyrighted but can be used freely. It was available before since I used it for courses on software verification but the link from my publication page was broken. Also, the figures were missing; I added them back.

I thought I only had the original (troff) files, which I have no easy way to process today, but just found PDFs for all the chapters, likely produced a few years ago when I was still able to put together a working troff setup. They are missing the figures, which I have to scan from a printed copy and reinsert. I just did it for the chapter on mathematical notations, chapter 2, which you can find at https://se.inf.ethz.ch/~meyer/publications/theory/02-math.pdf. If there is interest I will release all chapters (with corrections of errata reported by various readers over the years).

The chapters of the book are:

  • (Preface)
  1. Basic concepts
  2. Mathematical background (available through the link above).
  3. Syntax (introduces formal techniques for describing syntax, included a simplified BNF).
  4. Semantics: the main approaches (overview of the techniques described in detail in the following chapters).
  5. Lambda calculus.
  6. Denotational semantics: fundamentals.
  7. Denotational semantics: language features (covers denotational-style specifications of records, arrays, input/output etc.).
  8. The mathematics of recursion (talks in particular about iterative methods and fixpoints, and the bottom-up interpretation of recursion, based on work by Gérard Berry).
  9. Axiomatic semantics (available through the link above).
  10. Complementary semantic definitions (establishing a clear relationship between different specifications, particular axiomatic and denotational).
  • Bibliography

Numerous exercises are included. The formal models use throughout a small example language called Graal (for “Great Relief After Ada Lessons”).  The emphasis is on understanding programming and programming languages through simple mathematical models.

OOSC-2 available online (officially)

My book Object-Oriented Software Construction, 2nd edition (see the Wikipedia page) has become hard to get. There are various copies floating around the Web but they often use bad typography (wrong colors) and are unauthorized.

In response to numerous requests and in anticipation of the third edition I have been able to make it available electronically (with the explicit permission of the original publisher).

You can find the link on another page on this site. (In sharing or linking please use that page, not the URL of the actual PDF which might change.)

I hope having the text freely available proves useful.

 

PhD and postdoc positions in verification in Switzerland

The Chair of Software Engineering, my group at the Schaffhausen Institute of Technology in Switzerland (SIT), has open positions for both PhD students and postdocs. We are looking for candidates with a passion for reliable software and a mix of theoretical knowledge and practical experience in software engineering. Candidates should have degrees in computer science or related fields: a doctorate for postdoc positions, a master’s degree for PhD positions. Postdoc candidates should have a substantial publication record. Experience is expected in one or more of the following fields:

  • Software verification (axiomatic, model-checking, abstract interpretation etc.).
  • Advanced techniques of software testing.
  • Formal methods, semantics of programming languages.
  • Concurrent programming.
  • Design by Contract, Eiffel, techniques of correctness-by-construction.

Some of the work involves the AutoProof framework, under development at SIT (earlier at ETH), although other topics are also available, particularly in static analysis.

Compensation is attractive. Candidates must have the credentials to work in Switzerland (typically, citizenship or residence in Switzerland or the EU). Although we work in part remotely like everyone else these days, the positions are residential.

Interested candidates should send a CV and relevant documents or links (and any questions) to bm@sit.org.

Panel on methodology and agility, this Monday (20 September)

Today (well, tomorrow as of writing, but when you see this it will probably be today for you) I am participating in a panel discussion with Ivar Jacobson, Robert Martin and Carlos Zapata on “The Future of Methods”, hosted by the SEMAT/Essence movement. It takes place at 18:30 CET (i.e. Paris/Zurich etc.), 12:30 EDT, 9:30 in California. It’s free, but requires registration at https://www.meetup.com/essence-for-agility/events/280316615/.

Should be a good discussion!