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

double (result)
  sqrt double a
pre
  a >= 0
post
  result >= 0 && result * result == a;

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.

Inheritance

void
  foo
post
  A;

redefine void
  foo;

redefine void
  foo
post
  B;

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

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:

void preconditionFailed selector sel { [[SelectorCondition for self class condition-condition message "precondition not met" selector sel] raise]; }

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.

old

void
  add All object
post
  [self length] == old ([self length]) + 1
  && self[[self length] - 1] == object;

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

• 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.