an old topic (pun intended)

[Timon Gehr]

On 10/27/2011 10:02 PM, Davidson Corry wrote:
> Oooh! Now we're getting somewhere! You and bearophile have opened my eyes.
>
> On 10/27/2011 1:17 AM, Timon Gehr wrote:
>  > ...your example shows an extreme case and from that you
>  > conclude a general statement. That almost never works.
>
> I merely intended to show that my proposed syntax could *handle* the
> extreme case, not to prove that it was necessary. The "case" I presented
> was not only extreme but silly, and purely for purposes of illustration.
>

Ok, then I apologize.


 > OK, let's try this again.
> I was thinking less of syntax elegance and orthogonality, and more of
> easing the compiler's job. All the compiler would have to do would be to
> pluck (the underlined text)
>
> out(T preT = <some complete expression>)
> ===================================
>
> from the out "argument list" and inject it into the head of the function
> body, as though by mixin. However, your syntax works too:
>
>  > Often it is way more convenient to just write old(exp) than
>  > 1. think of a nice name for capturing the prestate.
>  > 2. change the signature of the out contract.
>  > 3. move the cursor back to where you were before.
>  > 4. write the name again.
>
> Just look for phrases of the form 'out(some complete expression)' in the
> post-condition body, hoist out the 'some complete expression' and
> prepend an 'auto fresh_symbol_x = ', then mix that into the head of the
> function.
>
> In fact, let us make the notation truly D-flavored:
>
> void foo(int n, string s)
> out {
> assert(count == old!count + 1, "count is wrong");
> assert(!old!(test_me(n, s, count)) || test_me(n, s, count), "implication
> fails");
> }
> body {
> // body of foo()...
> }
>
> gets a lowering as
>
> void foo(int n, string s) {
> // prestate-capture injected "mixin"
> auto fresh_symbol_1 = count;
> auto fresh_symbol_2 = test_me(n, s, count);
>
> // body of foo()...
>
> // injected post-condition tests,
> // with the fresh symbols substituted for the expressions
> assert(count == fresh_symbol_1 + 1, "count is wrong");
> assert(!fresh_symbol_2 || test_me(n, s, count), "implication fails");
> }

 From the compiler's point of view, both approaches should have 
comparable complexity.


>
> This approach does not allow you to explicitly declare the type of the
> prestate-capture-expression (all fresh_symbol_n's are auto) nor to name
> it. But as you say, it also relieves you of the *requirement* to name
> and type the expression. And to be honest, I can't think of a situation
> where you would truly *need* to name an old-expression.
>
> Another advantage of the old!expression syntax is that we don't
> introduce an additional keyword 'old' into the language, nor do we
> prevent the programmer from using 'old()' as the name of a function, nor
> do we burden the out block with a funky "argument list".
>
> Spiffy. Thanks, guys!
>
> -- Davidson

Yes, this design has indeed a keyword-issue that your proposal has not. 
I am all for not making it a keyword. The 'body' keyword imho should be 
removed too, there is only one place in the grammar where it is ever 
needed (and there it is completely redundant), therefore it could just 
be lexed as an identifier. That would not break any code.