Eiffel

Just another day at the office

by

In the past few weeks I wrote a program to compute the aliases of variables and expressions in an object-oriented program (based on a new theory [1]).

For one of the data structures, I needed a specific notion of equality, so I did the standard thing in Eiffel: redefine the is_equal function inherited from the top class ANY, to implement the desired variant.

The first time I ran the result, I got a postcondition violation. The violated postcondition clauses was not even any that I wrote: it was an original postcondition of is_equal (other: like Current)  in ANY, which my redefinition inherited as per the rules of Design by Contract; it reads

symmetric: Result implies other ~ Current

meaning: equality is symmetric, so if Result is true, i.e. the Current object is equal to other, then other must also be equal to Current. (~ is object equality, which applies the local version is is_equal).  What was I doing wrong? The structure is a list, so the code iterates on both the current list and the other list:

from
    start ; other.start ; Result := True
until (not Result) or after loop
        if other.after then Result := False else
              Result := (item ~ other.item)
              forth ; other.forth
        end
end

Simple enough: at each position check whether the item in the current list is equal to the item in the other list, and if so move forth in both the current list and the other one; stop whenever we find two unequal elements, or we exhaust either list as told by after list. (Since is_equal is a function and not produce any side effect, the actual code saves the cursors before the iteration and restores them afterwards. Thanks to Ian Warrington for asking about this point in a comment to this post. The new across loop variant described in  two later postings uses external cursors and manages them automatically, so this business of maintaining the cursor manually goes away.)

The problem is that with this algorithm it is possible to return True if the first list was exhausted but not the second, so that the first list is a subset of the other rather than identical. The correction is immediate: add

Result and other_list.after

after the loop; alternatively, enclose the loop in a conditional so that it is only executed if count = other.count (this solution is  better since it saves much computation in cases of lists of different sizes, which cannot be equal).

The lesson (other than that I need to be more careful) is that the error was caught immediately, thanks to a postcondition violation — and one that I did not even have to write. Just another day at the office; and let us shed a tear for the poor folks who still program without this kind of capability in their language and development environment.

Reference

[1] Bertrand Meyer: The Theory and Calculus of Aliasing, draft paper, available here.

Void safety: Getting rid of the spectre of null-pointer dereferencing

by

A spectre is haunting programming — the spectre of null-pointer dereferencing. All the programming languages of old Europe and the New World have entered into a holy alliance to make everyone’s programs brittle:  Java, C, Pascal, C++, C# and yes, until recently, Eiffel.

The culprit is the use of references to denote objects used in calls: in

         x.f (...)

the value of x is a reference, which normally denotes an object but could at any time be void (or “null”). If this happens, the resulting “void call” will cause an exception and, usually, a crash.  No amount of testing can remove the risk entirely; the only satisfactory solution is a static one, enforcing void safety at the language level.

To this end, Eiffelists of various nationalities have assembled in the Cloud and sketched the following manifesto, to be published in the English language:

        Avoid a Void: The Eradication of Null Dereferencing
        Bertrand Meyer, Alexander Kogtenkov, Emmanuel Stapf
        White paper available here.

Contracts written by people, contracts written by machines

by

What kind of contract do you write? Could these contracts, or some of them, be produced automatically?

The idea of inferring contracts from programs is intriguing; it also raises serious epistemological issues. In fact, one may question whether it makes any sense at all. I will leave the question of principle to another post, in connection with some of our as yet unpublished work. This is, in any case, an active research field, in particular because of the big stir that Mike Ernst’s Daikon created when it appeared a few years ago.

Daikon [1] infers loop invariants dynamically: it observes executions; by looking up a repertoire of invariant patterns, it finds out what properties the loops maintain. It may sound strange to you (it did to Mike’s PhD thesis supervisor [2] when he first heard about the idea), but it yields remarkable results.

In a recent paper presented at ISSTA [3], we took advantage of Daikon to compare the kinds of contract people write with those that a machine could infer. The work started out as Nadia Polikarpova’s master’s thesis at ITMO  in Saint Petersburg [4], in the group of Prof. Anatoly Shalyto and under the supervision of Ilinca Ciupa from ETH. (Ilinca recently completed her PhD thesis on automatic testing [5], and is co-author of the article.) The CITADEL tool — the name is an acronym, but you will have to look up the references to see what it means — applies Daikon to Eiffel program.

CITADEL is the first application of Daikon to a language where programmers can write contracts. Previous interfaces were for contract-less languages such as Java where the tool must synthesize everything. In Eiffel, programmers do write contracts (as confirmed by Chalin’s experimental study [6]). Hence the natural questions: does the tool infer the same contracts as a programmer will naturally write? If not, which kinds of contract is each best at?

To answer these questions, the study looked at three sources of contracts:

  • Contracts already present in the code (in the case of widely used libraries such as EiffelBase, equipped with contracts throughout).
  • Those devised by students, in a small-scale experiment.
  • The contracts inferred by Daikon.

What do you think? Before looking up our study, you might want to make your own guess at the answers. You will not find a spoiler here; for the study’s results, you should read our paper [3]. All right, just a hint: machines and people are (in case you had not noticed this before) good at different things.

References

 

[1] Michael Ernst and others, Daikon bibliography on Ernst’s research page at the University of Washington.

[2] David Notkin, see his web page.

[3] A Comparative Study of Programmer-Written and Automatically Inferred Contracts, by Nadia Polikarpova, Ilinca Ciupa and me, in ISSTA 2009: International Symposium on Software Testing and Analysis, Chicago, July 2009, online copy available.

[4] ITMO (Saint-Petersburg State University of Information Technologies, Mechanics and Optics), see here.

[5] Ilinca Ciupa, Strategies for random contract-based testing; PhD thesis, ETH Zurich, December 2008. For a link to the text and to her other publications see Ilinca’s ETH page.

[6] Patrice Chalin,  Are practitioners writing contracts? In Rigorous Development of Complex Fault-Tolerant Systems, eds. Jones et al.,  Lecture Notes in Computer Science 4157, Springer Verlag, 2006, pages 100-113.