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. -- Michiel Helvensteijn
