an old topic (pun intended)

[Davidson Corry]

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.

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");
     }

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