On Thursday, 5 February 2015 at 07:28:36 UTC, Paulo Pinto wrote:
I miss the point about in.
DbC as presentend by Eiffel and adopted in .NET, Ada among
others, the complete contract is on the callee.
It doesn't make sense otherwise.
Conceptually the precondition is a specification that the caller
has to guarantee, and the postcondition is a specification that
the callee guarantees. The enforcement of the contract
specification should be done by the build system which is
"neutral".
I.e. the contractors who wrote the code for the callers and
callees may try to subvert the contract, but the build system
should ideally prevent this. This is of course messed up in D,
since you don't have a separate specification independent of the
implementation, but you could still verify the D code against a
specification to prevent contractors from subverting contracts.
The thought of having the signature/specification before the
implementation was a good one, but readability suffers from
having all the braces. So the D syntax is not as usable as it
should be.
I think D should do this in the body like other languages:
func(){
@require(...);
@ensure(…);
... function body ...
}
or
func(){
@pre(...);
@post(…);
... function body ...
}
or
func(){
pre_assert(...);
post_assert(…);
... function body ...
}
