Following on from http://www.eiffelroom.com/blog/colin_adams/correctness_conditions_for_calling_an_agent, I have thought about the following scheme (it would require ECMA to be amended to require a tag on assertions, but this should be done anyway. Also, the tag would have to be unique with all the preconditions for a given feature - likewise for postconditions.):
<eiffel> class ROUTINE


