Michiel Helvensteijn wrote:
Denis Koroskin wrote:
Then I assume you still want to restrict the precondition to being the
first element in the body? Because putting it in there suggests that it
may appear anywhere a statement can.
Why not?
Because a function precondition indicates the set of admissible states
before execution of a function. Emphasis on *before* and *function*.
I would expect the precondition/postcondition to behave exactly as a
nested function, (except that it is automatically executed before/after
the first/last statement in the function is executed), so the lexical
order shouldn't matter. If they were implemented as pure nested
functions, they could safely call other pure nested functions -- so
allowing them to be later in the function would potentially be useful.
It would be strange to put outer function statements before the
precondition, but that's true of any inner function.
