Oliver Hoog wrote:
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.
And that's not even an option for interfaces that have "in" blocks,
something not implemented.
By and large, my opinion is that either we implement DbC correctly (with
contract inheritance) or we drop it from the language. As of now it's
completely redundant.
Andrei
