Michiel Helvensteijn schrieb:
Denis Koroskin wrote:
Because a function precondition indicates the set of admissible states
before execution of a function. Emphasis on *before* and *function*.
Allowing them anywhere inside a function body will only improve the
feature.
BTW, it is already allowed, just use 'debug' instead of 'in':
Or just use an assertion without an enclosing scope?
The difference between a precondition (in) and an arbitrary assertion inside
the function body is that the precondition is part of the public interface,
whereas the function implementation is not.
TBH, I'd just drop the whole DBC feature from a language, it creates more
problems than solves.
I, on the other hand, believe it's the future of program verification.
I also find them very useful with inherited functions.
That they can be inherited wouldn't be intuitive (and not as easily
possible) with an 'in' block nested into the function block.
