Sponsored Link •
Bill Venners: Are there parts of contracts that are difficult or impossible to express in a formal language, that you can only express in a human language?
Bertrand Meyer: The simple answer is yes. There are really three reasons why it
sometimes feels hard to express a contract in terms of a programming language. As a
background, the way contracts are expressed in Eiffel is very simple: they are just
Boolean expressions. Boolean expressions are intended precisely to express runtime true
or false properties—properties that at any point in the execution may hold or not
hold. That's exactly how Boolean expressions are used, for example, in an if-then-else
construction. That's also how they are used to express contracts in Eiffel, with one major
old keyword. The
makes it possible to express in a post-condition that a certain property at the completion
of a routine is relative to a certain property on entry to the routine. If you have, for
example, a routine that adds a certain amount of money to a bank account, obviously the
post-condition of this routine is going to have to express that the new balance is related to
the old balance. The new balance must be the balance before the execution of the routine
plus some amount. The only way to express this properly is to have some notation to
refer to the original value of the balance. So with this major, but single, extension, the
language of contracts in Eiffel is just the language of Boolean expressions.
There are three occasions in which this approach of using Boolean expressions may appear restrictive. One occasion that is justified—where you will have to resort to human language descriptions instead of formal ones—is when you have externally visible properties. For example, if you have in a graphical library an operation that changes the color of a certain pixel on the screen to red, you'd like to describe a post-condition that says the resulting color is red. Maybe to some extent you can do that, but what you really want to express is that if a person is sitting at a terminal, and the person is not color blind, he or she will accept that the new color is red. Clearly this kind of assertion cannot be expressed in a formal language, because it refers to properties outside of the realm of the software program. In practice it may not be such a big deal, because what you usually want in practice is not necessarily the guarantee that someone accepts the color as red, but the guarantee that the RGB value of the pixel being displayed is within a certain range. And of course that can be expressed as a purely Boolean property.
The second occasion where Boolean expressions may seem restrictive is one that scares most people who have looked at the issue from a theoretical perspective: the language of Boolean expressions is relatively limited and doesn't have first-order predicate calculus. This has led some people who design the specification mechanisms for programming languages, or in the case of UML, for modeling languages, to include facilities from first-order predicate calculus as a language extension. I think that is largely a mistake. At least we don't need to do this in Eiffel, because we have a high-level mechanism known as agents to describe essentially high-level functional operations on objects. So anything that you may want to express on a complex object that would seem to require first-order predicate calculus can be expressed actually quite nicely within the confines of the programming language.
What is quite easy to express with Boolean expressions, for example, is a property that if you're adding an element at the end of a list, the last element of the list is now the one that you just added. That's quite easy to express, and it's definitely expressed in the corresponding Eiffel concept. What is less easy to express is the property that all the other elements of the list, the ones that you haven't touched, are still there, in the same order, and are equal to their previous values. This kind of assertion seems to require special language extensions and has led people to suggest introducing first-order predicate calculus. But what we've found is that apart from the agents mechanisms, which has been in Eiffel now for a number of years, there's really no need for introducing first-order predicate calculus, or there exists operators. We can basically express those assertions in the realm of the programming language.
Also, first-order predicate calculus isn't good enough anyway. A typical kind of property that you might want to express, say, in a class invariant for a graph class, is that the graph has no cycles. This is not expressible as a first-order predicate calculus property. On the other hand, it is expressible as a Boolean expression if you accept including function calls in the Boolean expression. So that particular argument for extending the assertion language or for expressing contracts in English goes away at least in the long term. In the short term, these techniques of expressing high-level ambitious properties are still under development, and you will still find for that kind of property assertions expressed informally as comments.
The third occasion where defining contracts using Boolean expressions raises issues is non-functional contracts. Maybe I shouldn't go into this too much, because this is more of a research issue. Nevertheless, once you have completely expressed all the functional contracts—the contracts that specify what the input may be to operations, what outputs are legitimate, and what globally consistency constraints must be maintained—you might still want to express as part of the specification things like: this operation will always execute in less than half a millisecond, or this particular component will never use more than 300 kilobytes. These are performance contracts, and it's a quite interesting research area. I think there will be usable results in this area in the next few years, but it falls beyond the realm of Design by Contract as it is generally understood in practice today.
Bill Venners: That was actually my next question: is performance part of the contract? It does seem that performance is important in the contract sense. People want quality of service guarantees.
Bertrand Meyer: Right. Absolutely. It's very important. I think everyone realizes this. The problem is that it is pretty difficult to ensure and test. And it also has to be defined properly. When you define, for example, a response time, is it a minimum response time? Is it a maximum response time? Is it an average response time? If so, what is the statistical distribution? I don't think these questions have no possible answers, but they make the issue quite delicate. And they have no direct counterpart with functional contracts. So performance contracts are definitely an area in which more work is needed and actually is being performed.
Come back Monday, December 15 for the fifth installment of a conversation with C# creator Anders Hejlsberg. If you'd like to receive a brief weekly email announcing new articles at Artima.com, please subscribe to the Artima Newsletter.
Bertrand Meyer is the author of Object-Oriented Software Construction, which
is available on Amazon.com at:
Bertrand Meyer's Home Page at ETH, the Swiss Institute of Technology:
The Grand Challenge of Trusted Components, presented by Bertrand Meyer at the International
Conference on Software Engineering, May 2003:
The Structure and Interpretation of Computer Programs, by Harold Abelson and Gerald Jay Sussman
with Julie Sussman:
Find out more about Eiffel at:
The Eiffel language FAQ:
The 2001 Interview with Programming Expert Bertrand Meyer in InformIT:
(Gratuitously long URL omitted...)