On 10/27/2011 9:04 PM, bearophile wrote:
> Agreed. In fact, it occurred to me the other day that we could write
> contracts as
>
> void foo(T t)
> {
> scope(in) {
> // pre-condition contracts
> }
> scope(out) {
> // post-condition contracts
> }
> // ...body of function...
> }
>
How do you replace out(result) with scope(out) {} ?
I am not sure that we need to. D2 has two forms of the 'out()' statement
now: 'out(result)' and 'out(...)' [as it is shown in the DPL book, or
just 'out' in current practice].
The only reason to have an 'out(result)' form is to declare that we
intend to use the magic 'result' symbol in the post-condition testing.
Does this mean that, if we *don't* pre-declare 'out(result)' that the
symbol 'result' can have some *other* meaning in the post-condition?
That strikes me as a source of subtle bugs, if a programmer might
accidentally fail to declare 'out(result)' and thereby get different
semantics in the post-condition code without having changed that code.
I think the thing to do is to just declare 'out' as we currently do [or
'scope(out)' as I am proposing], and treat the 'result' symbol magically
in the post-condition code whether or not it is pre-declared -- that is,
have the compiler find it and interpret it as the magic returned-value.
-- Davidson
