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 following method declaration exhibits most of the syntax of
This declaration of the
sqrt double a
a >= 0
result >= 0 && result * result == a;
sqrt method indicates that
the method has one argument, of type
double, and that
it returns a value of type
double. The name in
(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
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:
(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
(referred to as foo'') then the full postcondition that
is applicable to foo'' becomes
A && B. So,
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
B from the postcondition example,
if they were preconditions, the full condition that would be
applicable to foo'' would be
A || B.
What happens when a precondition fails? That depends. To enable
method precondition checking, you must pass
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
class is set. Similarly, providing
:cc-post sets the
postconditions_enabled, which enables
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
message "precondition not met"
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
abort() when a raised condition is not handled.
Then you can print a backtrace to see where and how the actual
Similar to precondition checking, a failed postcondition check invokes
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-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:
This could be a method to add an object to the end of an
add All object
[self length] == old ([self length]) + 1
&& self[[self length] - 1] == object;
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.
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
- 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
- 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.