Posts tagged ‘Touch of Class’

## Publish no loop without its invariant

There may be no more blatant example of  the disconnect between the software engineering community and the practice of programming than the lack of widespread recognition for the fundamental role of loop invariants.

Let’s recall the basics, as they are taught in the fourth week or so of the ETH introductory programming course [1], from the very moment the course introduces loops. A loop is a mechanism to compute a result by successive approximations. To describe the current approximation, there is a loop invariant. The invariant must be:

1. Weak enough that we can easily ensure it on a subset, possibly trivial, of our data set. (“Easily” means than this task is substantially easier than the full problem we are trying to solve.)
2. Versatile enough that if it holds on some subset of the data we can easily (in the same sense) make it hold on a larger subset — even if only slightly larger.
3. Strong enough that, when it covers the entire data, it yields the result we seek.

As a simple example, assume we seek the maximum of an array a of numbers, indexed from 1. The invariant states that Result is the maximum of the array slice from 1 to i. Indeed:

1. We can trivially obtain the invariant by setting Result to be a [1]. (It is then the maximum of the slice a [1..1].)
2. If the invariant holds, we can extend it to a slightly larger slice — larger by just one element — by increasing i by 1 and updating Result to be the greater of the previous Result and the element a [i] (for the new  i).
3. When the slice covers the entire array — that is, i = n — the invariant tells us that Result is the maximum of the slice a [1..n], giving us the result we seek.

You cannot understand the corresponding program text

```    from
i := 1; Result := a [1]
until i = n loop
i := i + 1
if Result < a [i] then Result := a [i] end
end```

without understanding the loop invariant. That is true even of people who have never heard the term: they will somehow form a mental image of the intermediate situation that justifies the algorithm. With the formal notion, the reasoning becomes precise and checkable. The difference is the same as between a builder who has no notion of theory, and one who has learned the laws of mechanics and construction engineering.

As another example, take Levenshtein distance (also known as edit distance). It is the shortest sequence of operations (insert, delete or replace a character) that will transform a string into another. The algorithm (a form of dynamic programming) fills in a matrix top to bottom and left to right, each entry being one plus the maximum of the three neighboring ones to the top and left, except if the corresponding characters in the strings are the same, in which case it keeps the top-left neighbor’s value. The basic operation in the loop body reads

```      if source [i] = target [j] then
dist [i, j] := dist [i -1, j -1]
else
dist [i, j] := min (dist [i, j-1], dist [i-1, j-1], dist [i-1, j]) + 1
end```

You can run this and see it work, filling the array cell after cell, then delivering the result at (dist [M, N] (the bottom-right entry, M and i being the lengths of the source and target strings. Or just watch the animation on page 60 of [2]. It works, but why it works remains a total mystery until someone tells you the invariant:

Every value of dist filled so far is the minimum distance from the initial substrings of the source, containing characters at position 1 to p, to the initial substring of the target, positions 1 to q.

This is the rationale for the above code: we want to compute the next value, at position [i, j]; if the corresponding characters in the source and target are the same, no operation is needed to extend the result we had in the top-left neighbor (position [i-1, j-1]); if not, the best we can do is the minimum we can get by extending the results obtained for our three neighbors: through the insertion of source [i] if the minimum comes from the neighbor to the left, [i-1, j]; through the deletion of target [j] if it comes from the neighbor above; or through a replacement if from the top-left neighbor.

With this explanation, a mysterious, almost hermetic algorithm instantly becomes crystal-clear.

Yet another example is in-place linked list reversal. The body of the loop is a pointer ballet:

temp := previous
previous
:= next
next
:= next.right
previous.put_right
(temp)

with proper initialization (set next to the value of first and previous to Void) and finalization (set first to the value of previous). This is not the only possible implementation, but all variants of the algorithm use a very similar scheme.

The code looks again pretty abstruse, and hard to get right if you do not remember it exactly. As in the other examples, the only way to understand it is to see the invariant, describing the intermediate assumption after a typical loop iteration. If the original situation was this:

List reversal: initial state

then after a few iterations the algorithm yields this intermediate situation:

List reversal: intermediate state

The figure illustrates the invariant:

Starting from previous and repeatedly following right links yields the elements of some initial part of the list, but in the reverse of their original order; starting from next and following right links yields the remaining elements, in their original order.

Then it is clear what the loop body with its pointer ballet is about: it moves by one position to the right the boundary between the two parts, making sure that the invariant holds again in the new state, with one more element in the first (yellow) part and one fewer in the second (pink) part. At the end the second part will be empty and the first part will encompass all elements, so that (after resetting first to the value of previous) we get the desired result.

This example is particularly interesting because list reversal is a standard interview questions for programmers seeking a job; as a result, dozens of  pages around the Web helpfully present algorithms for the benefit of job candidates. I ran a search  on “List reversal algorithm” [3], which yields many such pages. It is astounding to see that from the first fifteen hits or so, which include pages from programming courses at both Stanford and MIT, not a single one mentions invariants, or (even without using the word) gives the above explanation. The situation is all the more bizarre that many of these pages — read them for yourself! — go into intricate details about variants of the pointer manipulations. There are essentially no correctness arguments.

If you go a bit further down the search results, you will find some papers that do reference invariants, but here is the catch: rather than programming or algorithms papers, they are papers about software verification, such as one by Richard Bornat which uses a low-level (C) version of the example to illustrate separation logic [4]. These are good papers but they are completely distinct from those directed at ordinary programmers, who simply wish to learn a basic algorithm, understand it in depth, and remember it on the day of the interview and beyond.

This chasm is wrong. Software verification techniques are not just good for the small phalanx of experts interested in formal proofs. The basic ideas have potential applications to the daily business of programming, as the practice of Eiffel has shown (this is the concept of  “Verification As a Matter Of Course” briefly discussed in an earlier post [5]). Absurdly, the majority of programmers do not know them.

It’s not that they cannot do their job: somehow they eke out good enough results, most of the time. After all, the European cathedrals of the middle ages were built without the benefit of sophisticated mathematical models, and they still stand. But today we would not hire a construction engineer who had not studied the appropriate mathematical techniques. Why should we make things different for software engineering, and deprive practitioners from the benefits of solid, well-accepted theory?

As a modest first step, there is no excuse, ever, for publishing a loop without the basic evidence of its adequacy: the loop invariant.

#### References

[1] Bertrand Meyer: Touch of Class: Learning to Program Well, Using Objects and Contracts, Springer, 2009. See course page (English version) here.

[2] Course slides on control structures,  here in PowerPoint (or here in PDF, without the animation); see example starting on page 51, particularly the animation on page 54. More recent version in German here (and in PDF here), animation on page 60.

[3] For balance I ran the search using Qrobe, which combines results from Ask, Bing and Google.

[4] Richard Bornat, Proving Pointer Programs in Hoare Logic, in  MPC ’00, 5th International Conference on Mathematics of Program Construction, 2000, available here.

[5] Bertrand Meyer, Verification as a Matter of Course, a post on this blog.

VN:F [1.9.10_1130]
VN:F [1.9.10_1130]

## Touch of Class book page available

The book page for Touch of Class (my introductory programming textbook), announced in the book, is finally available, courtesy Vladimir Tochilin:

touch.ethz.ch

It includes some book extracts (prefaces, table of contents, an entire sample chapter, for which I chose the Recursion chapter), a list of known errata and a wiki page to report new errata, a discussion forum, links to the full set of slides (PowerPoint, PDF) for the associated course, video recordings of that course at ETH, and a special “instructor’s corner” for those having adopted the textbook for their courses.

VN:F [1.9.10_1130]
VN:F [1.9.10_1130]

## Knuth & company

Remember Stacey’s in Palo Alto and San Francisco? Only a decade ago these and other technical bookstores were the mecca of the tech industry, where developers would swarm at any time of day to catch up on the latest releases. One well-known Valley entrepreneur even told me she did her hiring there, spotting customers who looked like developers and picked the right books.

Times have changed. After all the other branches, Stacey’s venerable San Francisco’s store finally closed earlier this year [1], the victim of the bubble’s burst, of Amazon, and of the crisis. Many others in the US and elsewhere met the same fate.

But wait… In Gaul, a little village is resisting the onslaught. A couple of streets away from the Shakespeare and company bookstore immortalized by Hemingway, Scott Fitzgerald and so many others, the Paris technical bookstore Le Monde en Tique [3] is a true legend of its own. Le Monde en Tique has, for the past twenty years, carried the best selection of computer and other technology books within a good thousand kilometers. I was there on Oct. 10, after the European Computer Science Summit (more on ECSS soon) for a book signing of Touch of Class:

The store’s name, “the World in Tics”, is a wink to the many “tics” served by its books, from informatics (computer science and information technology) to “telematics” (computer  communication). Housed in a beautiful stone edifice in the heart of medieval Paris, on a little winding street close to the river, Le Monde en Tique is more than a bookstore: it is a haven for the local developer community, a place to stop by on a Saturday afternoon for a passionate discussion on agility, Ajax or Agitar. There is even a small garden:

There is a secret to Le Monde en Tique’s continued success: the quality of its offerings. The unique skill of  Jean Demétreau and his team is their availability to locate hot new books, including those from the US and elsewhere, before anyone else does; the large Paris bookstores like FNAC, and the Web sites such as fnac.fr and amazon.fr are often several weeks behind. Not just the French sites, as a matter of fact: in the case of Touch of Class, Le Monde en Tique had the book about a month ahead of amazon.com USA. This is why people come from very far away to get both the latest offerings and the classics.

So here’s my plug: whether you have just heard about a great new book, or haven’t heard anything and want to find out what is the latest great new book, this is the place to go. It might already be late when you finally take yourself away from browsing the shelves; but as you go out of the store and walk a few steps, the sight will not be too bad:

#### References

[1] Matthai Kuruvila, Stacey’s Bookstore closing down in S.F., in SFGate (San Francisco Chronicle), 5 January 2009, available here.

[2] Shakespeare and company bookstore in Paris: see here.

[3] Le Monde en Tique bookstore, 6 rue Maître Albert, Paris: see www.lmet.fr.

VN:F [1.9.10_1130]
VN:F [1.9.10_1130]

## The great programming haiku competition

In a few weeks I will be teaching again my Introductory Programming course at ETH, based for the first time on the published “Touch of Class” textbook [1]. For fun (mine if no one else’s) every lecture will conclude with a haiku summarizing the topic.

I made up a few, given below, and am opening a competition for more. Every proposal should be submitted in the form of a comment to this post. Every winner’s haiku and name will appear in the course slides, and in the special Programming Haiku page which will be added to the book’s site. There are four rules:

• The contribution has to be a proper haiku: “three unrhymed lines of five, seven, and five syllables”.
• It must summarize the principal concept of a chapter or main section of the textbook or, better yet, of one of the course’s lectures; see [2] for the lecture plan.
• It must give the book reference (chapter or section) or lecture number or both.
• The prize committee’s members are secret and its judgments final.

Here, for a start, are my own examples.

#### Proof of the undecidability of the halting problem

Section 7.5 of the book; lecture 5.2.

If it stops, it loops,
Yet if it looped, it would stop.

#### Recursion

Chapter 14, especially section 14.3; lecture 9.1.

Often, I call you.
But when the going gets tough,
I will call myself.

#### Topological sort

Chapter 15; lectures 11.1 and 11.2.

Partial to total?
With the right data structures,
O of m plus n.

#### Dynamic binding

Section 16.3; lecture 8.1.

O-O programmers:
How many to screw a bulb?
None whatsoever.

#### Deferred classes

Section 16.5; lecture 8.1.

Do not implement!
Though for a truly Zen spec
You need a contract.

#### References

[1] Touch of Class: An Introduction to Programming Well Using Objects and Contracts, Springer Verlag, 2009. See Amazon page (still wrongly says the book is not yet published).

[2] “Introduction to Programming” course at ETH Zurich, Fall 2009: course page. This does not have the slides yet, but you can see last year’s slides in last year’s page.

VN:F [1.9.10_1130]
VN:F [1.9.10_1130]
Rating: +1 (from 1 vote)

## “Touch of Class” published

My textbook Touch of Class: An Introduction to Programming Well Using Objects and Contracts [1] is now available from Springer Verlag [2]. I have been told of many bookstores in Europe that have it by now; for example Amazon Germany [3] offers immediate delivery. Amazon US still lists the book as not yet published [4], but I think this will be corrected very soon.

The book results from six years of teaching introductory programming at ETH Zurich. It is richly illustrated in full color (not only with technical illustrations but with numerous photographs of people and artefacts). It is pretty big, but designed so that a typical one-semester introductory course can cover most of the material.

Many topics are addressed (see table of contents below), including quite a few that are seldom seen at the introductory level. Some examples, listed here in random order: a fairly extensive introduction to software engineering including things like requirements engineering (not usually mentioned in programming courses, with results for everyone to see!) and CMMI, a detailed discussion of how to implement recursion, polymorphism and dynamic binding and their role for software architecture, multiple inheritance, lambda calculus (at an introductory level of course), a detailed analysis of the Observer and Visitor patterns, event-driven programming, the lure and dangers of references and aliasing, topological sort as an example of both algorithm and API design, high-level function closures, software tools, properties of computer hardware relevant for programmers, undecidability etc.

The progression uses an object-oriented approach throughout; the examples are in Eiffel, and four appendices present the details of Java, C#, C++ and C. Concepts of Design by Contract and rigorous development are central to the approach; for example, loops are presented as a technique for computing a result by successive approximation, with a central role for the concept of loop invariant. This is not a “formal methods” book in the sense of inflicting on the students a heavy mathematical apparatus, but it uses preconditions, postconditions and invariants throughout to alert them to the importance of reasoning rigorously about programs. The discussion introduces many principles of sound design, in line with the book’s subtitle, “Learning to Program Well”.

The general approach is “Outside-In” (also known as “Inverted Curriculum” and described at some length in some of my articles, see e.g. [5]): students have, right from the start, the possibility of working with real software, a large (150,000-line) library that has been designed specifically for that purpose. Called Traffic, this library simulates traffic in a city; it is graphical and of good enough visual quality to be attractive to today’s “Wii generation” students, something that traditional beginners’ exercises, like computing the 7-th Fibonacci number, cannot do (although we have these too as well). Using the Traffic software through its API, students can right from the first couple of weeks produce powerful applications, without understanding the internals of the library. But they do not stop there: since the whole thing is available in open source, students learn little by little how the software is made internally. Hence the name “Outside-In”: understand the interface first, then dig into the internals. Two advantages of the approach are particularly worth noting:

• It emphasizes the value of abstraction, and particular contracts, not by preaching but by showing to students that abstraction helps them master a large body of professional-level software, doing things that would otherwise be unthinkable at an introductory level.
• It addresses what is probably today the biggest obstacle to teaching introductory programming: the wide diversity of initial student backgrounds. The risk with traditional approaches is either to fly too high and lose the novices, or stay too low and bore those who already have programming experience. With the Outside-In method the novices can follow the exact path charted from them, from external API to internal implementation; those who already know something about programming can move ahead of the lectures and start digging into the code by themselves for information and inspiration.

(We have pretty amazing data on students’ prior programming knowledge, as  we have been surveying students for the past six years, initially at ETH and more recently at the University of York in England thanks to our colleague Manuel Oriol; some day I will post a blog entry about this specific topic.)

The book has been field-tested in its successive drafts since 2003 at ETH, for the Introduction to Programming course (which starts again in a few weeks, for the first time with the benefit of the full text in printed form). Our material, such as a full set of slides, plus exercises, video recordings of the lectures etc. is available to any instructor selecting the text. I must say that Springer did an outstanding job with the quality of the printing and I hope that instructors, students, and even some practitioners already in industry will like both form and content.

Front matter: Community resource, Dedication (to Tony Hoare and Niklaus Wirth), Prefaces, Student_preface, Instructor_preface, Note to instructors: what to cover?, Contents

PART I: Basics
1 The industry of pure ideas
2 Dealing with objects
3 Program structure basics
4 The interface of a class
5 Just Enough Logic
6 Creating objects and executing systems
7 Control structures
8 Routines, functional abstraction and information hiding
9 Variables, assignment and references
PART II: How things work
10 Just enough hardware
11 Describing syntax
12 Programming languages and tools
PART III: Algorithms and data structures
13 Fundamental data structures, genericity, and algorithm complexity
14 Recursion and trees
15 Devising and engineering an algorithm: Topological Sort
PART IV: Object-Oriented Techniques
16 Inheritance
17 Operations as objects: agents and lambda calculus
18 Event-driven design
PART V: Towards software engineering
19 Introduction to software engineering
PART VI: Appendices
A An introduction to Java (from material by Marco Piccioni)
B An introduction to C# (from material by Benjamin Morandi)
C An introduction to C++ (from material by Nadia Polikarpova)
D From C++ to C
E Using the EiffelStudio environment
Picture credits
Index

#### References

[1] Bertrand Meyer, Touch of Class: An Introduction to Programming Well Using Objects and Contracts, Springer Verlag, 2009, 876+lxiv pages, Hardcover, ISBN: 978-3-540-92144-8.

[2] Publisher page for [1]: see  here. List price: \$79.95. (The page says “Ships in 3 to 4 weeks” but I think this is incorrect as the book is available; I’ll try to get the mention corrected.)

[3] Amazon.de page: see here. List price: EUR 53.45 (with offers starting at EUR 41.67).

[4] Amazon.com page: see here. List price: \$63.96.

[5] Michela Pedroni and Bertrand Meyer: The Inverted Curriculum in Practice, in Proceedings of SIGCSE 2006, ACM, Houston (Texas), 1-5 March 2006, pages 481-485; available online.

VN:F [1.9.10_1130]