an old topic (pun intended)

[Davidson Corry]

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