Re: Silly and stupid post-condition or not ?

["Randy Brukardt" <randy@rrsoftware.com>]

"BrianG" <me@null.email> wrote in message news:jgq2j2$g67$1@dont-email.me...
...
> It sounds like you don't want SPARK (as it is now, at least), but 
> something like an Ada equivalent to LINT.  (Not an Ada version of lint, 
> but something that does for Ada what lint does for C - covers Ada's needs, 
> rather than C's.)

It's not "Lint" really, it's really something to find errors of omission. 
(Errors of commission are many times easier to find and fix, like using the 
wrong algorithm or subtracting rather than adding.)

And usually this boils down to proving the absence of and/or proper handling 
of exceptions. 90% of the interesting cases have something to do with 
exceptions: either exceptions that are raised when they're not expected or 
not handled when they are expected.

I also want to do this in the context of normal compilation, so that (a) 
there is immediate feedback about problems and (b) there is no temptation to 
skip the step and (c) because I'm not in a position to build another large 
tool. ;-)

OK, the last probably isn't that important, but finding out about the 
problems as early as possible is important.

                                            Randy.