• Marcio (11/11) Sep 05 2006 Spec# http://research.microsoft.com/specsharp/ does extra checks
• pragma (23/38) Sep 05 2006 I was curious, so I went looking for information. I found the following

Marcio <mqmnews321 sglebs.com> writes:

(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

pragma <ericanderton yahoo.com> writes:

Marcio wrote:
 

 (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