Invariant and pre/post-conditions order

[bearophile]

Walter:

> My reasoning is it (1) doesn't make any difference and (2) it's always been like 
> that - and if it did make a difference, it would break 10 years of existing code.

In the second code example I've shown I receive an assert error in the wrong place. If a method is buggy, and its post-condition is designed to be able to catch such bugs, I expect to receive an assert error (or enforcement exception) with a line number inside the post-condition, and not very far from it into the invariant.

And my common formal sense tells me that verifying the more general condition first, tailored to spot errors inside the method that has just run, is better than doing it in the other order. But I don't know why, formally.

Maybe Eiffel docs explain the order it uses to run pre/post/invariants. I will try to find how Eiffel is designed here. 
Regarding the breaking, I don't think such change is able to break a lot of D2 code.

Thank you for your answers :-)
Bye,
bearophile