www.digitalmars.com         C & C++   DMDScript  

digitalmars.D - ESC/Modula3 (Extended Static Checking) for D?

reply Marcio <mqmnews321 sglebs.com> writes:
Spec# http://research.microsoft.com/specsharp/ does extra checks 
(basically covers/solves the issues on slide 29 of 
http://www.cs.princeton.edu/~dpw/popl/06/Tim-POPL.ppt ) thanks to 
Simplify http://research.microsoft.com/specsharp/simplify.htm.

Simplify is the beast behind it, from ESC/Modula3 
http://ftp.digital.com/pub/compaq/SRC/research-reports/abstracts/src-rr-159.html

I would like to suggest that it would be great if the D compiler 
incorporated such an idea.

Even Haskell people seem to be doing it 
http://lambda-the-ultimate.org/node/1689


marcio
Sep 05 2006
parent pragma <ericanderton yahoo.com> writes:
Marcio wrote:
 
 Spec# http://research.microsoft.com/specsharp/ does extra checks 
 (basically covers/solves the issues on slide 29 of 
 http://www.cs.princeton.edu/~dpw/popl/06/Tim-POPL.ppt ) thanks to 
 Simplify http://research.microsoft.com/specsharp/simplify.htm.
 
 Simplify is the beast behind it, from ESC/Modula3 
 http://ftp.digital.com/pub/compaq/SRC/research-reports/abstr
cts/src-rr-159.html 
 
 
 I would like to suggest that it would be great if the D compiler 
 incorporated such an idea.
 
 Even Haskell people seem to be doing it 
 http://lambda-the-ultimate.org/node/1689

I was curious, so I went looking for information. I found the following a little more enlightening: (From the digital.com site above) "The paper describes a mechanical checker for software that catches many common programming errors, in particular array index bounds errors, nil dereference errors, and synchronization errors in multi-threaded programs. The checking is performed at compile-time. The checker uses an automatic theorem-prover to reason about the semantics of conditional statements, loops, procedure and method calls, and exceptions. The checker has been implemented for Modula-3. It has been applied to thousands of lines of code, including mature systems code as well as fresh untested code, and it has found a number of errors." My $0.02: In short, I don't think there's any need to wait for Walter to implement this in DMD. It would be one heck of an undertaking, but I honestly don't see why the DMD frontend can't be put to task here. All it would take is someone who really had a firm grasp of the concepts outlined in the paper and used the frontend's parse-tree to perform the analysis. You'd then have a separate tool that can grow and mature, apart from Walter's already burdened schedule. - Eric
Sep 05 2006