www.digitalmars.com         C & C++   DMDScript  

digitalmars.D - an old topic (pun intended)

reply Davidson Corry <davidsoncorry comcast.net> writes:
     (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
Oct 26 2011
parent reply bearophile <bearophileHUGS lycos.com> writes:
Davidson Corry:


      (continuing a thread from D.learn)


I think you have written this post in digitalmars.D in a moment when the
limited brain power is busy with lot of other things :-)

I'd like some form of prestate to be implemented in D2. Usually I use manually
managed ghost variables (inside a debug{}) to solve this problem, but a more
built-in solution is better and more standard.



 Eiffel supports an 'old' construct in post-conditions.


It's often named "prestate".



      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

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.

Bye,
bearophile
Oct 26 2011
next sibling parent reply Davidson Corry <davidsoncorry comcast.net> writes:
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
Oct 26 2011
parent reply Timon Gehr <timon.gehr gmx.ch> writes:
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.
Oct 27 2011
parent reply Davidson Corry <davidsoncorry comcast.net> writes:
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
Oct 27 2011
next sibling parent reply Timon Gehr <timon.gehr gmx.ch> writes:
On 10/27/2011 10:02 PM, Davidson Corry wrote:

 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.


Ok, then I apologize.



 OK, let's try this again.
 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");
 }


 From the compiler's point of view, both approaches should have 
comparable complexity.



 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


Yes, this design has indeed a keyword-issue that your proposal has not. 
I am all for not making it a keyword. The 'body' keyword imho should be 
removed too, there is only one place in the grammar where it is ever 
needed (and there it is completely redundant), therefore it could just 
be lexed as an identifier. That would not break any code.
Oct 27 2011
parent reply Davidson Corry <davidsoncorry comcast.net> writes:
On 10/27/2011 2:12 PM, Timon Gehr wrote:

 Yes, this design has indeed a keyword-issue that your proposal has not.
 I am all for not making it a keyword. The 'body' keyword imho should be
 removed too, there is only one place in the grammar where it is ever
 needed (and there it is completely redundant), therefore it could just
 be lexed as an identifier. That would not break any code.


Agreed. In fact, it occurred to me the other day that we could write 
contracts as

     void foo(T t)
     {
         scope(in) {
              // pre-condition contracts
         }
         scope(out) {
              // post-condition contracts
         }
         // ...body of function...
     }

and eliminate the 'in', 'out' and 'body' keywords/constructs entirely.

Similarly, an invariant could appear in the default constructor of a 
class as

     this()
     {
         scope(invariant) {
             // invariant guarantees...
         }
         // ...body of constructor...
     }

Or *any* constructor, really, although you would probably want the 
compiler to enforce that no more than one constructor defined a 
scope(invariant) block. This notation also suggests (correctly) that the 
invariant doesn't take effect until you have entered the constructor. 
(Exited it, really, but...)

-- Davidson
Oct 27 2011
next sibling parent reply bearophile <bearophileHUGS lycos.com> writes:
Davidson Corry:


 Agreed. In fact, it occurred to me the other day that we could write 
 contracts as
 
      void foo(T t)
      {
          scope(in) {
               // pre-condition contracts
          }
          scope(out) {
               // post-condition contracts
          }
          // ...body of function...
      }


How do you replace out(result) with scope(out) {} ?

Bye,
bearophile
Oct 27 2011
parent reply Davidson Corry <davidsoncorry comcast.net> writes:
On 10/27/2011 9:04 PM, bearophile wrote:

  Agreed. In fact, it occurred to me the other day that we could write
  contracts as

        void foo(T t)
        {
            scope(in) {
                 // pre-condition contracts
            }
            scope(out) {
                 // post-condition contracts
            }
            // ...body of function...
        }




 How do you replace out(result) with scope(out) {} ?


I am not sure that we need to. D2 has two forms of the 'out()' statement 
now: 'out(result)' and 'out(...)' [as it is shown in the DPL book, or 
just 'out' in current practice].

The only reason to have an 'out(result)' form is to declare that we 
intend to use the magic 'result' symbol in the post-condition testing. 
Does this mean that, if we *don't* pre-declare 'out(result)' that the 
symbol 'result' can have some *other* meaning in the post-condition?

That strikes me as a source of subtle bugs, if a programmer might 
accidentally fail to declare 'out(result)' and thereby get different 
semantics in the post-condition code without having changed that code.

I think the thing to do is to just declare 'out' as we currently do [or 
'scope(out)' as I am proposing], and treat the 'result' symbol magically 
in the post-condition code whether or not it is pre-declared -- that is, 
have the compiler find it and interpret it as the magic returned-value.

-- Davidson
Oct 29 2011
parent reply bearophile <bearophileHUGS lycos.com> writes:
Davidson Corry:


 The only reason to have an 'out(result)' form is to declare that we 
 intend to use the magic 'result' symbol in the post-condition testing.


This is not true. Currently 'result' has nothing magic, it's just a variable
name, you are free to change it:


int result;
int foo(int x, out int result)
    out(y) {
        assert(y > 0);
    }
    body {
        result = 10;
        return -1;
    }
void main() {
    int z;
    auto s = foo(4, z);
}



 I think the thing to do is to just declare 'out' as we currently do [or 
 'scope(out)' as I am proposing], and treat the 'result' symbol magically 
 in the post-condition code whether or not it is pre-declared -- that is, 
 have the compiler find it and interpret it as the magic returned-value.


In some rare situations magic is acceptable, but it's dangerous, and in most
situations it's better to avoid it. Unless "result" becomes a keyword (so you
can't assign something to it by mistake), then the current syntax with
out(someConstVariableName) seems better.

Bye,
bearophile
Oct 29 2011
parent Davidson Corry <davidsoncorry comcast.net> writes:
On 10/29/2011 8:26 PM, bearophile wrote:

 The only reason to have an 'out(result)' form is to declare that we
 intend to use the magic 'result' symbol in the post-condition testing.


 This is not true. Currently 'result' has nothing magic, it's just a variable
name, you are free to change it:


Ah. I did not know that. Thanks for the info.


 I think the thing to do is to just declare 'out' as we currently do [or
 'scope(out)' as I am proposing], and treat the 'result' symbol magically
 in the post-condition code whether or not it is pre-declared -- that is,
 have the compiler find it and interpret it as the magic returned-value.


 In some rare situations magic is acceptable, but it's dangerous, and in most
situations it's better to avoid it.Unless "result" becomes a keyword (so you
can't assign something to it 


by mistake), then the current syntax with out(someConstVariableName) 
seems better.

Ah, again. 'Result' *is* magic in Eiffel (in all functions). I assumed 
that it was equivalently magic in D (in the post-condition context 
only), and named that way *because* of the Eiffel usage. You learn 
something every day.

The notion that you can name exactly zero symbols or exactly one symbol 
in the 'out()' "argument list", and if you name exactly one symbol then 
it gets (a copy of?) the returned value from the function which you can 
then use in your post-condition test strikes me as slightly more 
flexible at the cost of becoming slightly less obvious, and equally 
magical either way. But that's just my opinion, and I don't feel 
strongly about it.

-- Davidson
Oct 30 2011
prev sibling parent reply kennytm <kennytm gmail.com> writes:
Davidson Corry <davidsoncorry comcast.net> wrote:

 On 10/27/2011 2:12 PM, Timon Gehr wrote:

 Yes, this design has indeed a keyword-issue that your proposal has not.
 I am all for not making it a keyword. The 'body' keyword imho should be
 removed too, there is only one place in the grammar where it is ever
 needed (and there it is completely redundant), therefore it could just
 be lexed as an identifier. That would not break any code.


 
 Agreed. In fact, it occurred to me the other day that we could write contracts
as
 
     void foo(T t)
     {
         scope(in) {
              // pre-condition contracts
         }
         scope(out) {
              // post-condition contracts
         }
         // ...body of function...
     }
 
 and eliminate the 'in', 'out' and 'body' keywords/constructs entirely.
 
 Similarly, an invariant could appear in the default constructor of a class as
 
     this()
     {
         scope(invariant) {
             // invariant guarantees...
         }
         // ...body of constructor...
     }
 
 Or *any* constructor, really, although you would probably want the
 compiler to enforce that no more than one constructor defined a
 scope(invariant) block. This notation also suggests (correctly) that the
 invariant doesn't take effect until you have entered the constructor.
 (Exited it, really, but...)
 
 -- Davidson


The contracts are parts of the function's interface, not implementation. If
you put the scope(in/out) inside the '{ ... }' how would a .di file handle
it?

And class invariant is also checked outside the constructor. Your syntax
makes it look like it will run only when the constructor is called.
Oct 28 2011
parent Davidson Corry <davidsoncorry comcast.net> writes:
On 10/28/2011 5:10 AM, kennytm wrote:

 Davidson Corry<davidsoncorry comcast.net>  wrote:

  ...it occurred to me the other day that we could write contracts as

       void foo(T t)
       {
           scope(in) {
                // pre-condition contracts
           }
           scope(out) {
                // post-condition contracts
           }
           // ...body of function...
       }

  and eliminate the 'in', 'out' and 'body' keywords/constructs entirely.






Just in passing, I think that 'scope(requires)' and 'scope(ensures)' are 
somewhat more evocative of what these blocks actually do than 
'scope(in)' and 'scope(out)' would be. The words 'in' and 'out' have so 
many other connotations that they could be confusing.


  Similarly, an invariant could appear in the default constructor of a class as

       this()
       {
           scope(invariant) {
               // invariant guarantees...
           }
           // ...body of constructor...
       }

  Or*any*  constructor, really, although you would probably want the
  compiler to enforce that no more than one constructor defined a
  scope(invariant) block. This notation also suggests (correctly) that the
  invariant doesn't take effect until you have entered the constructor.
  (Exited it, really, but...)




 The contracts are parts of the function's interface, not implementation. If
 you put the scope(in/out) inside the '{ ... }' how would a .di file handle
 it?

 And class invariant is also checked outside the constructor. Your syntax
 makes it look like it will run only when the constructor is called.


Good point. A class invariant is special enough that it should be 
declared at class scope, rather than inside any particular method
(including constructors):

     class foo {
         scope(invariant) { /* the invariant checks */ }
         // implementation of the class...
     }

As for .di files, those can declare the contracts inside the braces and 
simply elide the body of the function. This is similar to Eiffel's 
short-flat form. Eiffel doesn't use braces for statement grouping or 
lexical scoping, but its contracts are just as much "inside" the 
function or method or class as the parameter lists of those functions or 
methods are.

Positioning the contract blocks inside the braces is also suggestive of 
the lexical environment (the "scope", although I'm trying not to use 
that word because it's overloaded in this context) within which the 
contract testing code runs -- anything that could be declared or 
referenced at that position in the source code is available to the 
contract code. (As with 'static if', the braces around a contract block 
are for grouping, and do *not* introduce a new lexical scope. You would 
need to {{double-brace}} the block to introduce new lexical scope, as 
you do with 'static if'.)

    ============

I do think that using the 'scope(something)' form for contracts is still 
a good idea.

'scope' is one of the big wins of the D design team. It allows the 
programmer to declare code over *here* where it's close to the resource 
it's going to clean up after, while making that code effective over 
*there* where the clean-up needs to be done -- upon exit from a block, 
upon failure of a block, etc. Or in this proposal, upon entry/exit to a 
class method (invariant) or upon entry into (requires) or exit from 
(ensures) a class method or a bare function... all without requiring the 
user to keep track of a complex scaffolding of try/catch/finally blocks, 
which the compiler manages for you.

It has a bit of the flavor of aspect-oriented programming, but without 
AOP's vagueness about what's going to happen when and where.

-- Davidson
Oct 29 2011
prev sibling parent Davidson Corry <davidsoncorry comcast.net> writes:
I want to point out (quick, before someone else does!) that the 
lowerings I have suggested for old! elsewhere in this thread are naïve. 
In the presence of inheritance, interface contracts, and/or multiple 
subtyping, things can get notably trickier.

That said,
1) I don't think it affects the utility of the old!symbol notation, and
2) old! would be useful even if inherited contracts weren't fully 
handled. (Much more so if they are, of course.)

-- Davidson
Oct 27 2011
prev sibling parent reply bearophile <bearophileHUGS lycos.com> writes:
 out(result, exprX, exprY) {


If you don't need to use the method result too, then you probably write
something like:

out(_, exprX, exprY) {

If the method is void then the _ has no value. Is this possible and good?

Bye,
bearophile
Oct 27 2011
parent Timon Gehr <timon.gehr gmx.ch> writes:
On 10/27/2011 11:34 AM, bearophile wrote:

 out(result, exprX, exprY) {


 If you don't need to use the method result too, then you probably write
something like:

 out(_, exprX, exprY) {

 If the method is void then the _ has no value. Is this possible and good?

 Bye,
 bearophile


This is possible, but I don't like it too much (see my other post).
Oct 27 2011