an old topic (pun intended)

[Davidson Corry]

     (continuing a thread from D.learn)

Eiffel supports an 'old' construct in post-conditions. For example, an 
Add method of a Bag class (generic collection container) might verify 
that exactly one element was added to the collection, not zero and not 
more than one:

     Add(newItem : T) is
     do
         -- insert newItem into the Bag
     ensure
         exactly_one_added: count = old count + 1
     end

D2 post-conditions do not provide 'old', and are less useful than they 
could be for its lack.

(Note: D post-conditions appear to be applicable to bare statements, not 
just functions. I don't see the point of statement post-conditions -- 
you can do the same thing with 'assert' -- so I focus here on function 
post-conditions.)

It has been suggested that 'unittest' largely obviates the need for 
'old'. I disagree with this view. A unit test verifies only the 
conditions that it explicitly proposes.  In contrast, a post-condition 
will exercise "real-world data" in production-level runs during testing, 
and is thus likely to trigger on conditions that the unit test never sees.

In the D.learn thread, Jonathan M Davis and Ali Çehreli comment

     JMD> IIRC, old was rejected because it added extra complication for 
little value.
      AÇ> Yes, there were technical difficulties in making the stack 
frame at the call point available to the stack frame at the exit point.

Another difficulty is examining the post-condition code for 'old expr' 
or 'old(expr)' and hoisting those elements out of the middle of an 
expression for prestate capture.

I want to propose a syntax extension that, it seems to me, makes it 
easier for the compiler to do all of this.

In D2, a post-condition is introduced with either 'out(result)' or 
'out(...)' [the latter now elided(??) to merely 'out']. That is, 'out' 
has what appears to be something like an argument list. Let's use it:

     void foo(T param_T, Q param_Q)
     out(result, X preX = exprX, Y preY = exprY) {   // <== prestate 
captures added to out "argument" list HERE
         // various assert()s using the captured prestates
     }
     body {
         // ..actual body of foo()
     }

A lowering of this would look something like

     void foo(T param_T, Q param_Q) {
         X __fresh_symbol_for_preX = exprX;
         Y __fresh_symbol_for_preY = exprY;
         // ..actual body of foo()
         assert(__postcondition_code);
     }

That is, the compiler would hoist the prestate variables (and the code 
that sets their values) out of the "argument" list, and inject them into 
the function body at its very start, much like a template instantiation.

Notes:

     +  "erasing" the actual symbols in the argument list and replacing 
them with compiler-generated fresh symbols hides those symbols from the 
function body code (which should not know of them)
     +  but those captured prestate-values exist at the outermost scope 
of the function body, just as the returned value of the function does. 
If we can pass the magic symbol 'result' to the post-condition, we 
should be able to pass
the captured prestate
     +  the scope and condition-at-time-of-evaluation for exprX and 
exprY are exactly what we want: they have access to anything that the 
function body can access (such as variables in enclosing functions, 
class members etc.) but NOT to
local declarations (which they should not be able to see) because those 
haven't been declared yet; they are part of the function body code that 
follows the injected prestate-capture code
     +  the compiler is relieved of the burden of sniffing out "old" 
sub-elements of expressions in the post-condition body and figuring out 
exactly what bits of frame and scope need to be preserved to compute 
them. The onus is on
the programmer to declare what prestate he wants to verify, and how to 
capture it, to whatever level of complexity he wants or needs to employ
     +  exprX etc. can use any syntax element that is legal within the 
function body (since it is hoisted and injected *into* the function body 
by the compiler), including things like lambda functions, etc. (In 
practice, "old"
expressions in post-conditions tend to be pretty tame.)
     +  the programmer can name the captured prestate values with any 
symbols he wishes. This preserves some of the flavor of Eiffel's 
per-post-condition labels.
     +  capture of prestates is separated from evaluation of 
post-function conditions *using* those prestates. This may make it more 
obvious what's being tested and how.
     +  no new 'old' keyword or magic 'old()' function needs to be added 
to the language, particularly one that is useful only in this isolated 
corner of the syntax

Two weird characteristics of this syntax:

     -  'result' is evaluated AFTER the function body executes, but 
prestate-captures are evaluated BEFORE the function body executes
     -  normal argument lists contain only expressions, not declarations 
of symbols to be assigned from those expressions

I think the syntax is clean and flexible enough to forgive those 
transgressions.



An example ('count' and 'color' here are members of an enclosing class, 
not shown):

     void change_count_and_color(int countIncrement, bool flipColor)
     out (result, auto preCount = count, auto previousColor = color) {
         assert(count == preCount + countIncrement);
         if (flipColor) {
             assert(color == ComplementaryColorOf(previousColor));
         }
         assert(isSensible(result));
     }
     body {
         // ..actual body of the function
     }



   =========

Comments, criticisms, jeers and guffaws cheerfully invited. (Also "if 
you're so smart, there's the source code, YOU implement it!" But then 
*I'll* guffaw.)

-- Davidson