On 10/27/2011 07:58 AM, Davidson Corry wrote:
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'.
That is what variables are for. I think that should be kept orthogonal.
void generate_improved_hash_and_key(string[] plaintexts)
out{
auto preFOM = old(figure_of_merit(plaintexts, internalKey,
internalHaskDelegate);
auto nowFOM = figure_of_merit(plaintexts, internalKey,
internalHashDelegate);
assert(preFOM <= nowFOM);
}
body{ /* ... */ }
Furthermore, your example shows an extreme case and from that you
conclude a general statement. That almost never works.
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. 3. write
the name again.
