On 10/26/2011 5:19 PM, bearophile wrote:
out(result, X preX = exprX, Y preY = exprY) { //<== prestate
I'd like something lighter, syntax-wise, where the is no need to state new and
old names and types:
> out(result, exprX, exprY) {
And then the compiler lets you access in the postcondition the old variables in
some standard way, like:
in.exprX, in.exprY
Despite this is is probably better looking:
old.exprX, old.exprY
I had intended for 'exprX' to represent some complex expression, not
simply a symbol. For instance, what if the prestate that you want to
capture is not merely the value-at-entry of some single datum, but
rather a "meta-prestate" computed from multiple source data?
For instance, suppose that you were generating hash functions and keys
for a cryptographic encoder class, and you had a function
figure_of_merit() [NOT a member of the class] that produces some metric
for how well the encryption works, based on the results of encrypting
each element of an array of sample plain-texts, and analyzing the
cryptexts thus produced.
The encoder class has data members 'internalKey' (a string used to
decode the encrypted text) and 'internalHashDelegate' (a delegate to a
hash-generating function which the class uses to encrypt plaintexts).
The class also has a function generate_improved_hash_and_key() which
potentially modifies either 'internalKey' or 'internalHashDelegate' or
both, and you would like to verify that the function actually does
improve things, or at least not make them worse:
void generate_improved_hash_and_key(string[] plaintexts)
out (float preFOM = figure_of_merit(plaintexts, internalKey,
internalHashDelegate) ) {
assert(preFOM <= figure_of_merit(plaintexts, internalKey,
internalHashDelegate);
}
body { /* ... */ }
I cannot see that the expression
old.figure_of_merit(plaintexts, internalKey, internalHashDelegate)
is an improvement over 'preFOM'.
It's also not easy for the compiler to figure out that, in the
old.expression, the arguments 'internalKey' and 'internalHashDelegate'
are the values of those data at entry-to-function, and somehow need to
be cached out to be used in the post-condition comparison, while the
very same arguments to the figure_of_merit() function in the body of the
post-condition are the values at the END of the function's execution.
With the syntax I proposed, the compiler doesn't have to figure out
either: the expression in the out(...) argument list gets injected at
the very start of the function body, and evaluates based on the
conditions BEFORE the function body gets going, while the body of the
post-condition is conceptually injected at the very end of the function
body [as if in a scope(exit) block] and uses the conditions that hold
AFTER the function body has completed execution.
Here "old" doesn't need to be keyword, it's like the local name of a struct
instance.
As discussed in D.learn there is no need for deep copying of the old variables.
If it's required, then the programmer has to do it manually by herself. This
avoids lot of implementation complexities.
Agreed. As in Eiffel, the programmer has the freedom, the responsibility
AND the power to do any deep-copy work needed. For example,
void foo(A a)
out (auto preA = a) { /* post-condition body using preA */ }
body { /* whatever foo() does */ }
would not work because 'preA' is just an additional reference to the
object that 'a' also refers to. If foo() happened to modify
'a.some_member', by data aliasing it has also modified
'preA.some_member', so the actual prestate is lost.
You would have to do one of the following:
out (auto preA = a.dup)
out (immutable(A) preA = a)
or use a struct for A with postblit constructor as needed (value
semantics rather than reference semantics).
Or drill down into the 'a' object and capture just the internal members,
or expressions built from them, that you need. It's up to you. And you
have the full power of the language to do it with.
-- Davidson
