Writing Bug-Free C/D Code

[Dan]

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