Derek Parnell wrote:
> On Wed, 21 Mar 2007 00:35:46 -0800, David B. Held wrote:
> 
>> Derek Parnell wrote:
>>> [...]
>>> The trouble is that D's typedef does not allow you to extend the semantics
>>> of the base type, but that's what structs and classes are for, no?
>>>
>>> The Euphoria language has a slightly different type construction mechanism
>>> which has its good side and bad side, but maybe something like it could be
>>> used to extend D's typedef mechanism.
>>> [...]
>> My understanding is that Contracts in D allow you to implement Ada-like SubRanges.  This is actually one of the things I really liked about the DbC support.  Is that not the case?
> 
> Contracts are optional. That is, if something is compiled with the -release
> switch, then contract code is not inserted into the executable. You cannot,
> and must not, rely on contract code for 'production' editions of software.
> It is only meant to be used during the development phases of an
> application, thus you should not use contracts to try and detect invalid
> input data for a function. Contract code should be used to detect logic
> errors and not data errors.

I disagree.  That input arguments must be within the proper range, etc, is a precondition, and the purpose of the 'in' clause is to check preconditions.  My interpretation of your statement is that data checking is so important that it may not happen as a part of normal precondition checking.  The thing is, *all* preconditions are important.  Should we just ignore the 'in' clause altogether then?  Or assert()? In my opinion, if the user disables contract checking then he is explicitly stating that he isn't interested in that level of security. My only regret is that the current crop of D compilers don't offer any means of linking a separate library for 'debug' and 'release' builds (a bad choice of words for the associated effects).


Sean

Sean Kelly Wrote:
> My only regret is that the current crop of D compilers don't offer any means of linking a separate library for 'debug' and 'release' builds (a bad choice of words for the associated effects).

I think you actually can link in different modules accordingly, via static ifs, version, debug { import x; } etc.  I think you mean phobos vs. tango etc. though right?

Dan wrote:
> Sean Kelly Wrote:
>> My only regret is that the current crop of D compilers don't offer any means of linking a separate library for 'debug' and 'release' builds (a bad choice of words for the associated effects).
> 
> I think you actually can link in different modules accordingly, via
> static ifs, version, debug { import x; } etc.  I think you mean phobos
> vs. tango etc. though right?

One problem with pragma(lib) is that it only works if the pragma is in a module being compiled into the program.  It has no effect if it is in a 'header' module.  So unless bud/rebuild is being used to construct the application, library developers have no way to automatically link a specific library using static if, version, etc.  And for something fairly fundamental like Phobos or Tango, I'm not sure it's appropriate to expect the user to explicitly link a debug, release, or debug/release build (yes, both flags can be specified simultaneously in D).


Sean

On Wed, 21 Mar 2007 09:44:14 -0400, Dan wrote:

>> It is only meant to be used during the development phases of an
>> application, thus you should not use contracts to try and detect invalid
>> input data for a function. Contract code should be used to detect logic
>> errors and not data errors.
>> Derek
> 
> Actually Derek, contracts as a concept have no such limitation.  Their current implementation only performs logic errors ...

I'm sorry if I may have been a bit vague, but I was actually talking about D's implementation of contracts and not *Contracts* as a general program development concept.

-- 
Derek
(skype: derek.j.parnell)
Melbourne, Australia
"Justice for David Hicks!"
22/03/2007 9:36:55 AM

On Wed, 21 Mar 2007 09:49:20 -0700, Sean Kelly wrote:

> Derek Parnell wrote:
>> On Wed, 21 Mar 2007 00:35:46 -0800, David B. Held wrote:
>> 
>>> Derek Parnell wrote:
>>>> [...]
>>>> The trouble is that D's typedef does not allow you to extend the semantics
>>>> of the base type, but that's what structs and classes are for, no?
>>>>
>>>> The Euphoria language has a slightly different type construction mechanism
>>>> which has its good side and bad side, but maybe something like it could be
>>>> used to extend D's typedef mechanism.
>>>> [...]
>>> My understanding is that Contracts in D allow you to implement Ada-like SubRanges.  This is actually one of the things I really liked about the DbC support.  Is that not the case?
>> 
>> Contracts are optional. That is, if something is compiled with the -release switch, then contract code is not inserted into the executable. You cannot, and must not, rely on contract code for 'production' editions of software. It is only meant to be used during the development phases of an application, thus you should not use contracts to try and detect invalid input data for a function. Contract code should be used to detect logic errors and not data errors.
> 
> I disagree.

Again, please note that the OP was asking about contracts *as implemented by D*, and that is what I restricted my comments to.

> That input arguments must be within the proper range, etc, is a precondition, and the purpose of the 'in' clause is to check preconditions.

However, one can compile it out of the code via a -release so I was saying that one must not rely on such contract code actually executing in a production release edition of the program.

Yes, input data, especially stuff that originates from outside of the application really ought to be validated at some stage, but 'in' blocks are not the best places if one is using the current implementation of D.

> My interpretation of your statement is that data checking is so important that it may not happen as a part of normal precondition checking.  The thing is, *all* preconditions are important.


And yet, DigitalMars has decided that 'in' blocks can be optionally compiled. I agree in principle with the idea that input data ought to be validated, but I would recommend that one does not use 'in' blocks to do that important task.

>   Should we just ignore the 'in' clause altogether then?

No, of course not. But using the current D implementation, one should not rely on it for production editions of your application. Use it only for development editions. Then, armed with this implementation of precondition contracts, one should use them to validate the logic of your algorithms and not the validity of incoming data.

> Or assert()?

No, of course not. But as asserts are not guaranteed to execute in production editions, one should just use them in development editions. Of course, you are quite at liberty to distribute both a 'debugging' edition along with the 'lean&mean' production edition of your application. For example, I do this with Bud.

-- 
Derek
(skype: derek.j.parnell)
Melbourne, Australia
"Justice for David Hicks!"
22/03/2007 9:40:56 AM

Derek Parnell wrote:
> On Wed, 21 Mar 2007 09:49:20 -0700, Sean Kelly wrote:
> 
>> Derek Parnell wrote:
>>> On Wed, 21 Mar 2007 00:35:46 -0800, David B. Held wrote:
>>>
>>>> Derek Parnell wrote:
>>>>> [...]
>>>>> The trouble is that D's typedef does not allow you to extend the semantics
>>>>> of the base type, but that's what structs and classes are for, no?
>>>>>
>>>>> The Euphoria language has a slightly different type construction mechanism
>>>>> which has its good side and bad side, but maybe something like it could be
>>>>> used to extend D's typedef mechanism.
>>>>> [...]
>>>> My understanding is that Contracts in D allow you to implement Ada-like SubRanges.  This is actually one of the things I really liked about the DbC support.  Is that not the case?
>>> Contracts are optional. That is, if something is compiled with the -release
>>> switch, then contract code is not inserted into the executable. You cannot,
>>> and must not, rely on contract code for 'production' editions of software.
>>> It is only meant to be used during the development phases of an
>>> application, thus you should not use contracts to try and detect invalid
>>> input data for a function. Contract code should be used to detect logic
>>> errors and not data errors.
>> I disagree.  
> 
> Again, please note that the OP was asking about contracts *as implemented
> by D*, and that is what I restricted my comments to.
> 
>> That input arguments must be within the proper range, etc, is a precondition, and the purpose of the 'in' clause is to check preconditions.  
> 
> However, one can compile it out of the code via a -release so I was saying
> that one must not rely on such contract code actually executing in a
> production release edition of the program. 
> 
> Yes, input data, especially stuff that originates from outside of the
> application really ought to be validated at some stage, but 'in' blocks are
> not the best places if one is using the current implementation of D.
> 
>> My interpretation of your statement is that data checking is so important that it may not happen as a part of normal precondition checking.  The thing is, *all* preconditions are important. 
> 
> 
> And yet, DigitalMars has decided that 'in' blocks can be optionally
> compiled. I agree in principle with the idea that input data ought to be
> validated, but I would recommend that one does not use 'in' blocks to do
> that important task.
> 
>>   Should we just ignore the 'in' clause altogether then?  
> 
> No, of course not. But using the current D implementation, one should not
> rely on it for production editions of your application. Use it only for
> development editions. Then, armed with this implementation of precondition
> contracts, one should use them to validate the logic of your algorithms and
> not the validity of incoming data.
> 
>> Or assert()? 
> 
> No, of course not. But as asserts are not guaranteed to execute in
> production editions, one should just use them in development editions. Of
> course, you are quite at liberty to distribute both a 'debugging' edition
> along with the 'lean&mean' production edition of your application. For
> example, I do this with Bud.
> 

I often take the same approach, and am quite glad that you do so.  Whenever I find unexpected sorts of building errors, for example, I revert to using bud_d.exe for subsequent builds until I figure out what's going on, just on the off chance Bud's debug code might catch something I'm not, or there may be an error in Bud itself -- hasn't happened for me yet, but I'm cautious.  :)

-- Chris Nicholson-Sauls

Derek Parnell wrote:
> 
> Yes, input data, especially stuff that originates from outside of the
> application really ought to be validated at some stage, but 'in' blocks are
> not the best places if one is using the current implementation of D.

Okay, this is a valid point.  I just happen to disagree with it :-)  I feel that this is what 'in' contracts are for, and if the user doesn't want that security then it's their prerogative to turn it off.

>> My interpretation of your statement is that data checking is so important that it may not happen as a part of normal precondition checking.  The thing is, *all* preconditions are important.  
> 
> And yet, DigitalMars has decided that 'in' blocks can be optionally
> compiled. I agree in principle with the idea that input data ought to be
> validated, but I would recommend that one does not use 'in' blocks to do
> that important task.

Or assert, I suppose, since it is disabled too.  This leaves D in the same situation as C/C++, and I refuse to do this simply because the user has the option to disable it.

>>   Should we just ignore the 'in' clause altogether then?  
> 
> No, of course not. But using the current D implementation, one should not
> rely on it for production editions of your application. Use it only for
> development editions. Then, armed with this implementation of precondition
> contracts, one should use them to validate the logic of your algorithms and
> not the validity of incoming data.

But this suggests that I should either do parameter checking both in the 'in' clause and in the function body using separate implementations (since assert is not an option).  This complicates maintenance, hurts readability, and reduces the overall utility of the contract programming features IMO.

>> Or assert()? 
> 
> No, of course not. But as asserts are not guaranteed to execute in
> production editions, one should just use them in development editions. Of
> course, you are quite at liberty to distribute both a 'debugging' edition
> along with the 'lean&mean' production edition of your application. For
> example, I do this with Bud.

I'd like to do this with Tango, but it is not an option for the simple install (ie. where the full runtime is bundled in phobos.lib), since that lib is implicitly linked.  By the way, can someone tell me what is included when both -debug and -release are set?


Sean

On Thu, 22 Mar 2007 09:20:01 -0700, Sean Kelly wrote:

> Derek Parnell wrote:

>>>   Should we just ignore the 'in' clause altogether then?
>> 
>> No, of course not. But using the current D implementation, one should not rely on it for production editions of your application. Use it only for development editions. Then, armed with this implementation of precondition contracts, one should use them to validate the logic of your algorithms and not the validity of incoming data.
> 
> But this suggests that I should either do parameter checking both in the 'in' clause and in the function body using separate implementations (since assert is not an option).  This complicates maintenance, hurts readability, and reduces the overall utility of the contract programming features IMO.

Huh? Why would you do it twice? That's crazy talk. Just code the validation once; at the start of the 'body' block. The effect is identical to coding it in the 'in' block only *and* not compiling with -release. No need to code the validation twice at all.

  int doubleit(int x, int y)
  body
  {
      // validate params.
      {
           if (y < 0) y = -y;
           if ((x < -y) || (x > y))
           {
               throw new Exception(ReportErr( RangeErr, x, -y, y));
           }
      }

      // Do the work now everything's okay.
      return x + x;
  }
  out(res)
  {
     assert(res = x*2, format("doubleit(%d): Weird Math Error", x));
  }
  unittest
  {
     assert( doubleit(-10) == -20 );
     assert( doubleit( -1) ==  -2 );
     assert( doubleit(  0) ==   0 );
     assert( doubleit(  1) ==   2 );
     assert( doubleit( 10) ==  20 );
     try{    doubleit(-111); } catch(Exception e) { writefln("%s", e.msg);}
     try{    doubleit(-11);  } catch(Exception e) { writefln("%s", e.msg);}
     try{    doubleit( 11);  } catch(Exception e) { writefln("%s", e.msg);}
     try{    doubleit( 111); } catch(Exception e) { writefln("%s", e.msg);}
  }

With this setup, I don't have to be concerned that -release will ignore my
out block as the function inputs are still validated.

> By the way, can someone tell me what is included when both -debug and -release are set?

-debug compiles *in* anything that is inside a debug block.
  e.g.  debug { writefln("Got here"); }
It has nothing whatsoever to do with -release or -unittest. It is
functionally identical to -version except that it allows 'anonymous'
blocks.

-release does not compile in asserts, 'in' blocks, or 'out' blocks.


-- 
Derek Parnell
Melbourne, Australia
"Justice for David Hicks!"
skype: derek.j.parnell

Derek Parnell Wrote:
> Huh? Why would you do it twice? That's crazy talk. Just code the validation once; at the start of the 'body' block. The effect is identical to coding it in the 'in' block only *and* not compiling with -release. No need to code the validation twice at all.
> 
>   int doubleit(int x, int y)
>   body
>   {
>       // validate params.
>       {
>            if (y < 0) y = -y;
>            if ((x < -y) || (x > y))
>            {
>                throw new Exception(ReportErr( RangeErr, x, -y, y));
>            }
>       }
> 
>       // Do the work now everything's okay.
>       return x + x;
>   }
>   out(res)
>   {
>      assert(res = x*2, format("doubleit(%d): Weird Math Error", x));
>   }

IMHO: Yuck.

Here's what I think *ought* to be done to solve the problem of guaranteeing that code is error free for input ranges;

int doubleit(int x, int y)
in {
  // note: you say if y is negative, make it positive twice and test <-y?
  // you then tested the original proposition ALSO!
  assert(x > y);
}
body {
  return x+x;
}
out(result) {
  assert( result == x*2, format("doubleit(%d): Weird Math Error", x) );
}

What should then happen is this:  The compiler should recognize that we only accept values such that x > y.  Knowing that, it should then verify that in all cases where this function can be called, that the input to the function must have this condition.  In cases where this *can* fail, it should raise an error - such as variables that are affected by user input or outside parameters that aren't already bounds checked or adjusted...

Theoretically, one could take any given int (between int.min and int.max) and adjust it such that x > y will be true for all cases.  This can be proven and verified by a proof by induction.

If you don't isolate the in/out tests from the body, a proof by induction couldn't know what needs to be proved to prove the code safe.

For such a system, you also actually do want to simply provide warnings for some cases; such as for example:

int qsort(int x, int y){
  int z = x + y;
}

In most cases, that would be considered bad, because if x + y exceeds int.max, you have an overflow.  That may in fact be the programmers intention however - so refusing to compile would be the wrong way to approach the problem.

Walter, I'm not sure, but I think you were hoping (or did) make the Abstract Symbol Tree accessible?  If so, it may be possible to start a dsource project to accomplish a proof by induction engine based on the current implementation of contract programming.

Sincerely,
Dan

On Thu, 22 Mar 2007 14:54:20 -0400, Dan wrote:

> Derek Parnell Wrote:
> 
> IMHO: Yuck.

I just knew that if I didn't write an off-the-cuff example that wasn't 110%
perfect I'd have some people pooh-poohing the concept I was trying to get
across. Sheesh - it was 3:58AM when I wrote that after having been up since
6:30AM the previous day!

> Here's what I think *ought* to be done to solve the problem of guaranteeing that code is error free for input ranges;

That was not the point of the example!

The point was, using current D, the 'in' block can never be guaranteed to
be executed so don't rely on using the 'in' block for parameter validation
- whatever that validation happens to be.

> int doubleit(int x, int y)
> in {
>   // note: you say if y is negative, make it positive twice and test <-y?
>   // you then tested the original proposition ALSO!

Get a grip, eh? It was a silly example and didn't mean to represent best practice. The actual code used is totally irrelevant to my argument.

>   assert(x > y);
> }

Now, if this is compiled using '-release' then your precious assert test is quietly ignored and the user gets a nasty run time error, as opposed to a nice run time error.

> body {
>   return x+x;
> }
> out(result) {
>   assert( result == x*2, format("doubleit(%d): Weird Math Error", x) );
> }
> 
> What should then happen is this:  The compiler should recognize that we only accept values such that x > y.  Knowing that, it should then verify that in all cases where this function can be called, that the input to the function must have this condition.  In cases where this *can* fail, it should raise an error - such as variables that are affected by user input or outside parameters that aren't already bounds checked or adjusted...

If I was to ask for an improvement in the compiler, with respect to assert() and in{}, it would be to enable us to target exactly which parts of the DbC to excluded in a build. Personally, if I could, I'd never exclude in{} or out{} blocks with the -release switch. Instead I'd like to code them more like ...

  int somefunc( ... )
  in { ...validate inputs ...}
  body { ... }
  debug(logic) out {}

and then when developing I'd compile with -debug=logic and when compiling
the production edition I'd just leave out the -debug switch but use
-release to skip over assert().



-- 
Derek
(skype: derek.j.parnell)
Melbourne, Australia
"Justice for David Hicks!"
23/03/2007 1:02:58 PM