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
