• Dan <murpsoft hotmail.com> Mar 23 2007

Dan <murpsoft hotmail.com> writes:

Reiner Pope Wrote:
 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.


 compiler to verify all my conditions at compile-time.


I agree m8.  It should be a separate feature and/or program that you run when
your program compiles and you want to make it proveably correct (bug-free)

 To me, the point 
 about the 'in' contracts is that they will only ever trigger at a bug. 


To me, bug = failure.  As programmers, we often accept six dozen failures in a
program without realizing it and then find out 7 years down the road (see the
libc quicksort bug).  If we could have a tool to help us completely eliminate
bugs, wouldn't that be awesome?  Contract programming *allows* us to, it
doesn't by default though.

 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.


Not always, sometimes it just gives you no answer, or worse, the wrong one. 
Sometimes it works for all cases but exactly one number, which means you find
it years and years down the road and a 38million dollar system crashes because
of it.  Picture if that was how the libc quicksort bug was found... libc is
thought to be stable.

 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).


It only has to parse and maintain a set of possible min/max pairs.  I'm
suggesting it would be possible to prove by induction for non-constants and
constants alike; by examining how they are modified through possible program
flows, and verifying that by the time they hit an "in" or "out" they are within
acceptable parameters.

This would be done by reverse-tracing the potential flow paths up to the
declaration of the variable, and then doubling back fetching possible ranges
going back down each of those potential flow paths to the result.  This has a
marked similarity to chess algorithms.

Dumping the potential program paths, performing spectral analysis and such
would be well beyond the scope of what most programmers are used to.  However,
I feel with sufficient development it could become almost completely automated.

It would also formalize and automated what most senior programmers already try
to do in their head.

 
 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.


Ooo... sweet.  Something *interesting* to read.

 
 Cheers,
 
 Reiner


On that note, Walter, any chance we can get access to the AST?