Method Preconditions and Postconditions
TOM Home
TOM Tasks

Download TOM
TOM Software
Bug Database
Mailing Lists

tiggr at

Short Cuts:

all of 'em
tom [an error occurred while processing this directive]
tesla [an error occurred while processing this directive]
mu [an error occurred while processing this directive]
tomgtk [an error occurred while processing this directive]

all of 'em
tom 1.1.1
tomgtk 0.11
tesla 0.91
gp 0.5
mu 1.0

GIF free NOW!

Method preconditions and postconditions provide a mechanism to explicitly express the expectations and promises of a method in such a way that they can be checked by the program. As far as I know, Eiffel was the first language to actively employ this paradigm.

Method conditions as currently implemented in TOM have (almost) the same semantics as in Eiffel. This TOM highlight only provides insights on the How in TOM, not the Why of method conditions. To learn more about method conditions and why you would want them, read some Eiffel or Business Object Notation (BON) book, visit some Eiffel site (e.g. starting at Yahoo's Eiffel index), or read the LDBC answer in the comp.lang.eiffel FAQ.

The basics

The following method declaration exhibits most of the syntax of method conditions:

double (result)
  sqrt double a
  a >= 0
  result >= 0 && result * result == a;
This declaration of the sqrt method indicates that the method has one argument, of type double, and that it returns a value of type double. The name in parentheses, `(result)', following the return type provides a name to refer to the value returned, which is useful in method conditions, as we will see.

Following the `signature' of the method is pre a >= 0. This precondition states that the invocation of this method is only valid if the argument a is larger than or equal to 0. This condition is checked by the method itself; not by the caller of the method. Since in TOM, the sender of a message resulting in the invocation of a method is not known, TOM methods always check the method conditions, even when the invoking object is self.

Following the precondition is post result >= 0 && result * result == a. This is the postcondition, and it states that the sqrt method is supposed to return a number that is larger than 0 and the square of which equals the original argument, just like what you'd expect from a function that computes the square root of a number.


So far, we've shown some nice syntax, but haven't explained why adding that syntax would be a worthwhile addition to the language. The crux is that method conditions are inherited by overriding methods. The easy application of this is shown by postconditions. Given the following (abstract) method:

(referred to as foo), which is redefined in a subclass:

redefine void
(referred to as foo'). Then the postcondition that is applicable to foo' is the one specified for foo. If, in addition, a further redefinition specifies its own postcondition:

redefine void
(referred to as foo'') then the full postcondition that is applicable to foo'' becomes A && B. So, if either A or B is not met, the postcondition for foo'' already fails.

With method preconditions, things are a little different. The (Eiffel) idea is that a subclass can not demand more from a method invocation than a superclass can, since an instance of the subclass must be usable at every location where an instance of the superclass is expected (the essence of covariance). Because of this, preconditions can not be strengthened: additional method preconditions weaken the total condition. In terms of the A and B from the postcondition example, if they were preconditions, the full condition that would be applicable to foo'' would be A || B.

The details

What happens when a precondition fails? That depends. To enable method precondition checking, you must pass :cc-pre on the command line of the program that you want to run with precondition checking enabled. This option is handled by the tom library unit: when specified, the variable preconditions_enabled of the tom.Runtime class is set. Similarly, providing :cc-post sets the variable postconditions_enabled, which enables postcondition checking.

When a precondition fails, the following method invocation is executed:

[self preconditionFailed cmd];

The default implementation of this method is provided by the instance (All) like this:

  preconditionFailed selector sel
    for self
    class condition-condition
    message "precondition not met"
    selector sel]

This raises a condition, which must be handled or the program will exit, printing which method of which object failed. You can of course override this method in your own classes, or replace the default implementation if the default behaviour does not suite your needs. When running under a debugger, provide :rt-core on the command line to make the program stop in abort() when a raised condition is not handled. Then you can print a backtrace to see where and how the actual problem happened.

Similar to precondition checking, a failed postcondition check invokes the method postconditionFailed.

Unless directed to do otherwise, the TOM compiler will include the method condition checks in the code that it outputs. If you feel confident without them, provide -fno-pre-checks or -fno-post-checks to disable emission of precondition and postcondition checking code, respectively, or -fno-checks to disable both.


There is one more syntactical thing to postconditions: the old operator, for example as used in this method:

  add All object
  [self length] == old ([self length]) + 1
  && self[[self length] - 1] == object;
This could be a method to add an object to the end of an Indexed collection. The postcondition states that the length after the method invocation is 1 more than the old length, which is the length upon entering the method. Furthermore the object will have ended up at the highest index.

The semantics of old is plain and simple: its value is the value of the operand as it was evaluated upon entering the method.

The nasty

A few points are worth noting:
  • TOM does not have class invariants. The most important reason is that the sender of a message is never known, so the code can not know when a method call from another object has finished, indicating the moment to check the invariants, or whether it was a call from self, which would not be a moment to check the invariant.
  • Method conditions are just expressions; you can do in them whatever you like. However, it is imperative that you do not put any side effects in them. You want your program to behave identical with or without condition checking.
  • If you use (the value of) an argument in a postcondition, remember not to modify its value in the method body.
  • If you change or add a precondition or a postcondition, all redefinitions of that method must be recompiled for the change to take effect.
  • The strict Eiffel rules concerning precondition and postconditions seem not to be universally applicable to a language like TOM, in which classes can be extended and posed. Eiffel puts too much stress on the precondition posing requirements on the client of a routine, in which case the widening preconditions make sense. They are less useful if you consider the requirements to reflect on the history of the program's execution as it lead up to a particular method invocation. A class might think `foo' is a good prerequisite for a method; a subclass might require that in addition `bar' must also be met. It poses requirements on all clients of the object instead of only the client doing this particular method call.
  • Multi-threading in TOM is not part of the language, and the mechanism of overloading the precondition syntax to mean that an object has to wait until the condition becomes true (as in ISE Eiffel) will not be adopted.

Up: Highlights
Copyright © 1997-2002 Programmers Without Deadlines