My body is ugly [Re: Contextualizing keywords]

[Michiel Helvensteijn]

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