Writing Bug-Free C/D Code

[Reiner Pope]

Dan wrote:
> 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.  
Perhaps I'm misunderstanding what you say, but it seems like you are 
saying that the compiler could *always* analyse programs to determine 
whether the assert will ever be triggered. This is impossible for the 
general case as it solves the halting problem (you can reduce all exit 
conditions to x > y things).

> 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) );
> }
...
> 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.
I agree with how you would code it here, although I wouldn't expect the 
compiler to verify all my conditions at compile-time. To me, the point 
about the 'in' contracts is that they will only ever trigger at a bug. 
You hope not to have any of these when you release, so you are spending 
unnecessary processing time checking things which should always be true 
anyway.

If there is a bug, then either way you get a crash for the end user; an 
assert failure isn't really so much more pleasant than a segmentation 
violation for an end user.

> 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.
Such a program would surely be very useful, but I'm not convinced it 
should be done through compile-time programming (automated theorem 
proving takes a long time: you wouldn't want to run it *every time* you 
compile, and you also wouldn't want to run it through CTFE, which is slow).

If anyone is interested, though, Sage (http://sage.soe.ucsc.edu/) and 
Spec# (http://research.microsoft.com/specsharp/) are research languages 
which attempt to statically verify as much in the contracts as possible.

Cheers,

Reiner