[Christopher Petrilli]
I notice you mention post/pre conditions (something that UML obviously talks about). I wonder if we want to do a bit of research on Eiffle and it's contractual description. The only thing I wonder is if some of this is actually useful programatically, if that makes sense? It's great info, but is it useful at runtime?
Eiffel takes this all very seriously, and supplies several variants of assertions that are individually togglable. Preconditions verify a method is called according to its docs; postconditions verify a method does what it's advertised to do; anyone who takes debugging seriously is writing verification code of that kind anyway, and Eiffel automates it to an extraordinary degree. Note that's only the tip of "the contract" part: inherent in any contracting scheme is the ability to sub-contract. A subcontractor cannot require more, nor deliver less, than the original contract specifies. So, in Eiffel, for a subclass S that overrides a base class B's method M, the preconditions for S.M are magically OR'ed with the preconditions for B.M (S.M can't require more than B.M, but it may require less), and the postconditions for S.M are magically AND'ed with the postconditions for B.M (S.M can't deliver less than B.M, but it may deliver more). The language guarantees to keep all this stuff straight for you, and the doc-generation system for Eiffel knows all about it too. This isn't a collection of random debugging features in Eiffel: it's all in support of a particular formal theory of program design. if-you-can't-check-a-thing-at-runtime-you-can't-know-whether- it's-been-satisfied-ly y'rs - tim